diff options
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/FPDivision64.v | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 6d82ae67..8f0d2fa1 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1014,12 +1014,18 @@ Proof. pose proof (Zgt_cases (b * q) a)%Z as CASE. destruct (_ >? _)%Z. - { admit. } - apply Zdiv_unique with (b := (a - q*b)%Z). - ring. + { unfold b', q', a' in DELTA. + rewrite <- mult_IZR in DELTA. + rewrite <- minus_IZR in DELTA. + rewrite Rabs_Zabs in DELTA. + apply lt_IZR in DELTA. + rewrite Z.abs_eq in DELTA by lia. + + apply Zdiv_unique with (b := (a - (q-1)*b)%Z). + ring. + split; lia. + } - split. - { rewrite Z.mul_comm. lia. } rewrite <- Rabs_Ropp in DELTA. unfold b', q', a' in DELTA. rewrite <- mult_IZR in DELTA. @@ -1028,8 +1034,12 @@ Proof. rewrite Rabs_Zabs in DELTA. apply lt_IZR in DELTA. rewrite Z.abs_eq in DELTA by lia. - lia. -Admitted. + + apply Zdiv_unique with (b := (a - q*b)%Z). + ring. + + split; lia. +Qed. Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (step1_real_inv_longu b). |