diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-13 00:07:39 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-13 00:07:39 +0100 |
| commit | ff28b8ca5249e8c4ff0ec519673f71a382e816ad (patch) | |
| tree | 38e50ad47dde420e967ac98b591876b8a1f321b1 /kvx/FPDivision32.v | |
| parent | 5354fea25dd1537a9ce36fbebcc190f5dda241c1 (diff) | |
| download | compcert-kvx-ff28b8ca5249e8c4ff0ec519673f71a382e816ad.tar.gz compcert-kvx-ff28b8ca5249e8c4ff0ec519673f71a382e816ad.zip | |
moved functions to a more logical place
Diffstat (limited to 'kvx/FPDivision32.v')
| -rw-r--r-- | kvx/FPDivision32.v | 27 |
1 files changed, 1 insertions, 26 deletions
diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v index 7c37c619..5cda1077 100644 --- a/kvx/FPDivision32.v +++ b/kvx/FPDivision32.v @@ -21,10 +21,7 @@ Require Import IEEE754_extra. From Gappa Require Import Gappa_tactic. Local Open Scope cminorsel_scope. - -Local Open Scope string_scope. -Local Open Scope error_monad_scope. - + Definition approx_inv b := let invb_s := Eop Oinvfs ((Eop Osingleofintu ((Eletvar 0%nat):::Enil)):::Enil) in let invb_d := Eop Ofloatofsingle (invb_s ::: Enil) in @@ -358,27 +355,6 @@ Qed. Opaque approx_inv. -Theorem Znearest_le - : forall choice (x y : R), (x <= y)%R -> Znearest choice x <= Znearest choice y. -Proof. - intros. - destruct (Z_le_gt_dec (Znearest choice x) (Znearest choice y)) as [LE | GT]. - assumption. - exfalso. - assert (1 <= IZR (Znearest choice x) - IZR(Znearest choice y))%R as GAP. - { rewrite <- minus_IZR. - apply IZR_le. - lia. - } - pose proof (Znearest_imp2 choice x) as Rx. - pose proof (Znearest_imp2 choice y) as Ry. - apply Rabs_def2b in Rx. - apply Rabs_def2b in Ry. - assert (x = y) by lra. - subst y. - lia. -Qed. - Theorem fp_divu32_correct : forall (ge : genv) (sp: val) cmenv memenv (le : letenv) (expr_a expr_b : expr) (a b : int) @@ -610,4 +586,3 @@ Proof. reflexivity. Qed. - |