diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 14:39:51 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 14:39:51 +0100 |
| commit | 3c48c9f0c53ca01cdee579cf1f2ca11879f8874f (patch) | |
| tree | ea16e9d419128dfbfc05381b684830ec488a3c7a /kvx | |
| parent | 8c60bfedbad045a1d60994d46362d3c61e8b20a8 (diff) | |
| download | compcert-kvx-3c48c9f0c53ca01cdee579cf1f2ca11879f8874f.tar.gz compcert-kvx-3c48c9f0c53ca01cdee579cf1f2ca11879f8874f.zip | |
progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index be0fedfd..28c7fe72 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -35,7 +35,7 @@ Definition approx_inv b := let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in Elet b (Elet invb_d x). -Definition approx_inv_thresh := (0.000000000000001)%R. +Definition approx_inv_thresh := (0.1)%R. (* Lemma BofZ_exact_zero: @@ -121,7 +121,7 @@ Proof. fold invb_d in C3. rewrite Rlt_bool_true in C3; cycle 1. { clear C3. admit. } - change (is_finite 24 128 (BofZ 24 128 eq_refl eq_refl 1)) with true in C2F. + change (is_finite 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)) with true in C2F. destruct (C3 C2F) as (C3E & C3F & C3S). unfold Float.fma. assert (is_finite _ _ (Float.neg invb_d) = true) as invb_d_F. @@ -131,7 +131,7 @@ Proof. assumption. } - pose proof (BofZ_correct 53 1024 eq_refl eq_refl b') as C4. + pose proof (BofZ_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C4. rewrite Rlt_bool_true in C4; cycle 1. { clear C4. admit. @@ -155,10 +155,14 @@ Proof. { admit. } destruct C5 as (C5E & C5F & C5S). - pose proof (Bfma_correct 53 1024 eq_refl eq_refl Float.fma_nan mode_NE - (Bfma 53 1024 eq_refl eq_refl Float.fma_nan mode_NE + pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE + (Bfma 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE (Float.neg invb_d) b_d ExtFloat.one) invb_d invb_d C5F C3F C3F) as C6. - + rewrite Rlt_bool_true in C6; cycle 1. + { admit. } + destruct C6 as (C6E & C6F & C6S). + split. + { exact C6F. } Admitted. Definition approx_div a b := |