diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 22:14:44 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 22:14:44 +0100 |
| commit | 3fb606b155f0ed443bb99b0a94b2b32ca3ad4276 (patch) | |
| tree | 64b9b82fe27bdeed1e9119029ad21e4a15d47def | |
| parent | b0f18b3de1c530a03a90c0618c39a3d26704f49e (diff) | |
| download | compcert-kvx-3fb606b155f0ed443bb99b0a94b2b32ca3ad4276.tar.gz compcert-kvx-3fb606b155f0ed443bb99b0a94b2b32ca3ad4276.zip | |
Qed
| -rw-r--r-- | kvx/FPDivision.v | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 5d1ce1ac..a5be3d0a 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -209,7 +209,29 @@ Proof. (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. } + { clear C6. + rewrite C3E. + rewrite C2E. + rewrite C1E. + rewrite C0E. + rewrite C5E. + unfold Float.neg. + rewrite B2R_Bopp. + rewrite C3E. + rewrite C2E. + rewrite C0E. + rewrite C1E. + unfold b_d. + rewrite Int64.unsigned_repr by lia. + rewrite C4E. + unfold ExtFloat.one. + change (Float.of_int (Int.repr 1)) with (BofZ 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1). + rewrite C9E. + apply (Rabs_relax (bpow radix2 10)). + { apply bpow_lt; lia. } + cbn. + gappa. + } destruct C6 as (C6E & C6F & _). split. { exact C6F. } @@ -267,7 +289,7 @@ Proof. unfold invb0, rd, rs, approx_inv_thresh. apply Rabs_le. gappa. -Admitted. +Qed. Definition approx_div a b := let a_var := Eletvar (1%nat) in |