diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-14 11:47:58 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-14 11:47:58 +0100 |
| commit | 0ca71551f9d47dcc04e7a97bb294a0379732bc04 (patch) | |
| tree | 56f31d6584ec3ddd2f87fccbe65424da80fdf3c3 /kvx | |
| parent | a5df0e05f97f5ce4ee35723089cbd4a83435d37f (diff) | |
| download | compcert-kvx-0ca71551f9d47dcc04e7a97bb294a0379732bc04.tar.gz compcert-kvx-0ca71551f9d47dcc04e7a97bb294a0379732bc04.zip | |
find_quotient
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). |