diff options
| -rw-r--r-- | kvx/FPDivision64.v | 23 |
1 files changed, 20 insertions, 3 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 424dfc77..a44de06e 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -184,9 +184,26 @@ Proof. fold b_d. set (r_invb_d := B2R 53 1024 invb_d) in *. set (r_b_d := B2R 53 1024 b_d) in *. - - unfold invb_d. - unfold invb_s. gappa. } + fold b_d in C6. + destruct C6 as (C6R & C6F & _). + + pose proof (Bfma_correct 53 1024 re re Float.fma_nan mode_NE + (Bfma 53 1024 re re Float.fma_nan mode_NE + (Bopp 53 1024 Float.neg_nan invb_d) b_d (BofZ 53 1024 re re 1)) + invb_d invb_d C6F C3F C3F) as C7. + rewrite Rlt_bool_true in C7; cycle 1. + { clear C7. + rewrite C6R. + rewrite B2R_Bopp. + eapply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + rewrite C4R. + cbn. + set (r_invb_d := B2R 53 1024 invb_d) in *. + set (r_b_d := B2R 53 1024 b_d) in *. + gappa. + } + Admitted. |