diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:10:38 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:10:38 +0100 |
| commit | 1e3340be6913b8988cde998c165e77eea480783c (patch) | |
| tree | 3452e3fd79f64f8d3889e464abe998ec2d8a1590 /kvx | |
| parent | 54cf78c0d3579dced79d846ee111b8c5edfee615 (diff) | |
| download | compcert-kvx-1e3340be6913b8988cde998c165e77eea480783c.tar.gz compcert-kvx-1e3340be6913b8988cde998c165e77eea480783c.zip | |
reorganize proof
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index f22387d6..db44c30a 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -538,7 +538,8 @@ Proof. pose proof (Rabs_triang (prod' - IZR a' * inv_b_r) (IZR a' * delta))%R. lra. } - rewrite <- div_approx_reals_correct with (x := B2R _ _ prod); cycle 1. lia. exact NEAR. + pose proof (div_approx_reals_correct (Int.unsigned a) (Int.unsigned b) prod') as DIV_CORRECT. + rewrite <- DIV_CORRECT; cycle 1. lia. exact NEAR. unfold div_approx_reals. fold a' b' prod' prod_r. @@ -586,6 +587,18 @@ Proof. } cbn. f_equal. + rewrite Int64.add_signed. + rewrite (Int64.signed_repr prod_r) by (cbn ; lia). + rewrite Int64.signed_repr by (cbn ; lia). + unfold Int64.loword. + rewrite Int64.unsigned_repr. reflexivity. + fold prod' in NEAR. + fold a' in NEAR. + fold b' in NEAR. + split. + 2: cbn; lia. + apply le_IZR. + rewrite plus_IZR. admit. - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1. { unfold Int64.lt. |