diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:27:15 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 12:27:15 +0100 |
| commit | cae3d77b314778bd6b0dcc679ac7833c38ce7aeb (patch) | |
| tree | 7e8c702415bd7c720b948063c4c075d06a15ba1a | |
| parent | 1e3340be6913b8988cde998c165e77eea480783c (diff) | |
| download | compcert-kvx-cae3d77b314778bd6b0dcc679ac7833c38ce7aeb.tar.gz compcert-kvx-cae3d77b314778bd6b0dcc679ac7833c38ce7aeb.zip | |
no more admitted
| -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 db44c30a..d9c108a7 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -541,7 +541,7 @@ Proof. 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. + unfold div_approx_reals in *. fold a' b' prod' prod_r. unfold Int64.mul. rewrite Int64.unsigned_repr by (cbn; lia). @@ -577,7 +577,10 @@ Proof. apply Rabs_def2b in R4. split; nra. } - case Z.ltb_spec; intro CMP. + fold a' b' prod_r in DIV_CORRECT. + + pose proof (Zlt_cases (a' - prod_r * b') 0) as CMP. + destruct (Z.ltb (a' - prod_r * b') 0). - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true; cycle 1. { unfold Int64.lt. change (Int64.signed Int64.zero) with 0. @@ -597,9 +600,10 @@ Proof. fold b' in NEAR. split. 2: cbn; lia. - apply le_IZR. - rewrite plus_IZR. - admit. + replace (prod_r + (-1)) with (prod_r - 1) by lia. + rewrite (DIV_CORRECT b_nz NEAR). + apply Z.div_pos; lia. + - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1. { unfold Int64.lt. change (Int64.signed Int64.zero) with 0. @@ -611,6 +615,6 @@ Proof. unfold Int64.loword. rewrite Int64.unsigned_repr by (cbn; lia). reflexivity. -Admitted. +Qed. |