diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-14 11:39:22 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-14 11:39:22 +0100 |
| commit | a5df0e05f97f5ce4ee35723089cbd4a83435d37f (patch) | |
| tree | 834f62bebec1e79091ad8f00abbf7c6defafcd59 /kvx | |
| parent | 0742df3a567f98445e95669f92a291fda733d286 (diff) | |
| download | compcert-kvx-a5df0e05f97f5ce4ee35723089cbd4a83435d37f.tar.gz compcert-kvx-a5df0e05f97f5ce4ee35723089cbd4a83435d37f.zip | |
some more proof
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 767e7ae0..6d82ae67 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -953,6 +953,7 @@ Proof. gappa. Qed. +(* Lemma range_up_le : forall a x b, (IZR a <= IZR x <= (IZR b) - 1)%R -> @@ -965,6 +966,7 @@ Proof. { apply le_IZR. rewrite minus_IZR. lra. } lia. Qed. + *) Lemma find_quotient: forall (a b : Z) @@ -1015,13 +1017,20 @@ Proof. { admit. } apply Zdiv_unique with (b := (a - q*b)%Z). ring. - apply range_up_le. - rewrite minus_IZR. - rewrite mult_IZR. - fold a' b' q'. - - Search (Rabs _ * Rabs _)%R. + split. + { rewrite Z.mul_comm. lia. } + rewrite <- Rabs_Ropp in DELTA. + unfold b', q', a' in DELTA. + rewrite <- mult_IZR in DELTA. + rewrite <- minus_IZR in DELTA. + rewrite <- opp_IZR in DELTA. + rewrite Rabs_Zabs in DELTA. + apply lt_IZR in DELTA. + rewrite Z.abs_eq in DELTA by lia. + lia. +Admitted. + Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (step1_real_inv_longu b). |