From cd444fa2200427a1e792716ad5cbac9c1eac872e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 7 Jan 2022 19:12:03 +0100 Subject: progress in proofs --- kvx/FPDivision64.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 851a6cc4..f61cc48c 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -208,5 +208,39 @@ Proof. destruct C7 as (C7R & C7F & _). split. assumption. + rewrite C7R. + rewrite C6R. + rewrite C5R. + rewrite C4R. + rewrite B2R_Bopp. + rewrite C3R. + rewrite C2R. + rewrite C1R. + rewrite C0R. + cbn. + set(b1 := IZR b') in *. + replace (round radix2 (FLT_exp (-1074) 53) ZnearestE 1) with 1%R by gappa. + set (bd := round radix2 (FLT_exp (-1074) 53) ZnearestE b1). + set (x0 := round radix2 (FLT_exp (-1074) 53) ZnearestE + (round radix2 (FLT_exp (-149) 24) ZnearestE + (1 / round radix2 (FLT_exp (-149) 24) ZnearestE b1))). + set (alpha0 := (- x0 * bd + 1)%R). + set (y1 := (round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0 * x0 + x0)%R). + set (x1 := round radix2 (FLT_exp (-1074) 53) ZnearestE y1). + replace (x1 - 1/b1)%R with ((y1-1/b1)+(x1-y1))%R by ring. + + assert(alpha0 = -((x0-1/bd)/(1/bd)))%R as alpha0_EQ. + { unfold alpha0. + field. + unfold bd. + gappa. + } + assert(y1-1/b1 = ((round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0) + - alpha0) * x0 + + alpha0*(x0-1/b1) - ((bd-b1)/b1) * x0)%R as y1_EQ. + { unfold y1, alpha0. + field. + lra. + } Admitted. -- cgit