diff options
-rw-r--r-- | kvx/FPDivision64.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 76e21e54..d16417fb 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -582,7 +582,9 @@ Proof. econstructor. split. reflexivity. rewrite C3R. rewrite C2R. - rewrite C3S. + rewrite C3S; cycle 1. + { apply is_finite_not_is_nan. + assumption. } rewrite C2S. rewrite C1S. rewrite C3F. @@ -597,4 +599,12 @@ Proof. ((rd (rd (IZR a') * f_r) - (rd (IZR a') * f_r)) + ((rd (IZR a') - IZR a') * f_r) + (IZR a') * (f_r - 1 / IZR b'))%R by (field ; lra). + + assert (Rabs (rd (IZR a') - IZR a') <= 1024)%R as DELTA1. + { unfold rd. gappa. } + set (delta1 := (rd (IZR a') - IZR a')%R) in *. + + assert (Rabs (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r) <= 1024)%R as DELTA2. + { unfold rd. gappa. } + set (delta2 := (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r)%R) in *. Admitted. |