From ff28b8ca5249e8c4ff0ec519673f71a382e816ad Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 13 Jan 2022 00:07:39 +0100 Subject: moved functions to a more logical place --- kvx/FPDivision32.v | 27 +-------------------------- 1 file changed, 1 insertion(+), 26 deletions(-) (limited to 'kvx/FPDivision32.v') 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. - -- cgit