diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-11 15:31:02 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-11 15:31:02 +0100 |
| commit | aa8f655361670b593f805b1e57a1089b8f924938 (patch) | |
| tree | 52b0b6076c502a7c02a5799b5fcf7654746f9458 /kvx | |
| parent | 76917c124e7c7de216acd99555209f18c1ecd16b (diff) | |
| download | compcert-kvx-aa8f655361670b593f805b1e57a1089b8f924938.tar.gz compcert-kvx-aa8f655361670b593f805b1e57a1089b8f924938.zip | |
progress in proofs
Diffstat (limited to 'kvx')
| -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. |