diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 14:48:59 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 14:48:59 +0100 |
| commit | 74dec8e174e1a49facaf68d45b3c920c5547123d (patch) | |
| tree | 9c58efd45bb0c9683a0dc4fcee1a1c2659771662 /kvx/FPDivision64.v | |
| parent | c61b77be54b4696e5c5d5ed2a60f00fbc3dedb56 (diff) | |
| download | compcert-kvx-74dec8e174e1a49facaf68d45b3c920c5547123d.tar.gz compcert-kvx-74dec8e174e1a49facaf68d45b3c920c5547123d.zip | |
progress
Diffstat (limited to 'kvx/FPDivision64.v')
| -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 766ff80f..23cf73e3 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1045,8 +1045,7 @@ Qed. Lemma find_quotient: forall (a b : Z) - (b_POS : (b > 0)%Z) - (invb : R) + (b_POS : (0 < b)%Z) (qr : R) (GAP : (Rabs (IZR a / IZR b - qr) < /2)%R), (a / b)%Z = @@ -1345,9 +1344,20 @@ Proof. fold a'. rewrite signed_repr_sub. - - - Check Int64.signed_repr. + rewrite Int64.signed_repr; cycle 1. + { admit. } + + assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF. + { replace (IZR a' / IZR b' - q')%R with + (-(q' - IZR a' / IZR b'))%R by ring. + rewrite Rabs_Ropp. + lra. + } + rewrite (find_quotient a' b' b_NOT0 q' HALF). + fold q''. + unfold zlt. - rewrite find_quotient with (qr := q'). - cbn. + destruct (Z_lt_dec 0). + - replace ( _ >? _ )%Z with true by lia. reflexivity. + - replace ( _ >? _ )%Z with false by lia. reflexivity. +Admitted. |