diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 09:24:14 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-17 09:24:14 +0100 |
| commit | 94dff310377cf75e9457dbf67fbc39fc2ab82c7b (patch) | |
| tree | 688edfbeffa225d9bf8c959ba3cf0cb5a52a3655 /kvx | |
| parent | 449165cb8b108e15c60ccb76821f0208adac8056 (diff) | |
| download | compcert-kvx-94dff310377cf75e9457dbf67fbc39fc2ab82c7b.tar.gz compcert-kvx-94dff310377cf75e9457dbf67fbc39fc2ab82c7b.zip | |
one admit less
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 72c2c8ca..573a8e18 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -423,7 +423,16 @@ Proof. pose proof (Bmult_correct 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt)a') inv_b) as C1. set (inv_b_r := B2R 53 1024 inv_b) in *. - assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R) by admit. + assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R). + { split; unfold Rdiv. + - apply Rmult_le_compat_l. lra. + apply Rinv_le. apply IZR_lt. lia. + apply IZR_le. lia. + - replace 1%R with (1 / 1)%R at 2 by field. + apply Rmult_le_compat_l. lra. + apply Rinv_le. apply IZR_lt. lia. + apply IZR_le. lia. + } apply Rabs_def2b in inv_b_correct. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. |