diff options
| -rw-r--r-- | kvx/FPDivision32.v | 27 | ||||
| -rw-r--r-- | lib/IEEE754_extra.v | 344 |
2 files changed, 180 insertions, 191 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. - diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 7e0e7260..636ea1ff 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -28,6 +28,184 @@ Require Import Coq.Logic.FunctionalExtensionality. Local Open Scope Z_scope. + +Lemma Znearest_IZR : + forall choice n, (Znearest choice (IZR n)) = n. +Proof. + intros. + unfold Znearest. + case Rcompare_spec ; intro ORDER. + - apply Zfloor_IZR. + - destruct choice. + + apply Zceil_IZR. + + apply Zfloor_IZR. + - apply Zceil_IZR. +Qed. + +Lemma ZnearestE_IZR: + forall n, (ZnearestE (IZR n)) = n. +Proof. + apply Znearest_IZR. +Qed. + +Lemma Zfloor_opp : + forall x : R, (Zfloor (- x)) = - (Zceil x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Z.opp_involutive. + reflexivity. +Qed. + +Lemma Zceil_opp : + forall x : R, (Zceil (- x)) = - (Zfloor x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Ropp_involutive. + reflexivity. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro. + rewrite Znearest_opp. + f_equal. + f_equal. + apply functional_extensionality. + intro. + rewrite Z.even_opp. + fold (Z.succ x0). + rewrite Z.even_succ. + f_equal. + apply Z.negb_odd. +Qed. + +Lemma Zceil_non_floor: + forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + apply Zceil_imp. + split. + { rewrite minus_IZR. + rewrite plus_IZR. + lra. + } + rewrite plus_IZR. + pose proof (Zfloor_ub x). + lra. +Qed. + +(** more complicated way of proving +Lemma Zceil_non_ceil: + forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + cut (Zfloor x = (Zceil x) - 1). { intros; lia. } + apply Zfloor_imp. + split. + { rewrite minus_IZR. + pose proof (Zceil_lb x). + lra. + } + rewrite plus_IZR. + rewrite minus_IZR. + lra. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro x. + unfold ZnearestE. + case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP. + - pose proof (Zfloor_lb x) as LB. + destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT]. + lra. + { set (n := Zfloor x) in *. + rewrite EXACT. + rewrite <- opp_IZR. + rewrite Zfloor_IZR. + rewrite opp_IZR. + rewrite Rcompare_Lt by lra. + reflexivity. + } + rewrite Rcompare_Gt. + { apply Zceil_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by assumption. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Eq. + { rewrite Zceil_opp. + rewrite Zfloor_opp. + rewrite Z.even_opp. + rewrite Zceil_non_floor by lra. + rewrite Z.even_succ. + rewrite Z.negb_odd. + destruct (Z.even (Zfloor x)); reflexivity. + } + rewrite Zfloor_opp. + rewrite opp_IZR. + ring_simplify. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Lt. + { apply Zfloor_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. +Qed. + *) + +Lemma Znearest_imp2: + forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R. +Proof. + intros. + unfold Znearest. + pose proof (Zfloor_lb x) as FL. + pose proof (Zceil_ub x) as CU. + pose proof (Zceil_non_floor x) as NF. + case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra. + - destruct choice; lra. + - destruct choice. 2: lra. + rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. + - rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. +Qed. + +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_le_inv in Rx. + apply Rabs_le_inv in Ry. + assert (x = y) by lra. + subst y. + lia. +Qed. + Section Extra_ops. (** [prec] is the number of bits of the mantissa including the implicit one. @@ -901,145 +1079,6 @@ Definition ZofB_ne (f: binary_float): option Z := | _ => None end. -Lemma Znearest_IZR : - forall choice n, (Znearest choice (IZR n)) = n. -Proof. - intros. - unfold Znearest. - case Rcompare_spec ; intro ORDER. - - apply Zfloor_IZR. - - destruct choice. - + apply Zceil_IZR. - + apply Zfloor_IZR. - - apply Zceil_IZR. -Qed. - -Lemma ZnearestE_IZR: - forall n, (ZnearestE (IZR n)) = n. -Proof. - apply Znearest_IZR. -Qed. - -Lemma Zfloor_opp : - forall x : R, (Zfloor (- x)) = - (Zceil x). -Proof. - unfold Zceil, Zfloor. - intro x. - rewrite Z.opp_involutive. - reflexivity. -Qed. - -Lemma Zceil_opp : - forall x : R, (Zceil (- x)) = - (Zfloor x). -Proof. - unfold Zceil, Zfloor. - intro x. - rewrite Ropp_involutive. - reflexivity. -Qed. - -Lemma ZnearestE_opp - : forall x : R, ZnearestE (- x) = - ZnearestE x. -Proof. - intro. - rewrite Znearest_opp. - f_equal. - f_equal. - apply functional_extensionality. - intro. - rewrite Z.even_opp. - fold (Z.succ x0). - rewrite Z.even_succ. - f_equal. - apply Z.negb_odd. -Qed. - -Lemma Zceil_non_floor: - forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). -Proof. - intros x BETWEEN. - unfold Z.succ. - apply Zceil_imp. - split. - { rewrite minus_IZR. - rewrite plus_IZR. - lra. - } - rewrite plus_IZR. - pose proof (Zfloor_ub x). - lra. -Qed. - -(** more complicated way of proving -Lemma Zceil_non_ceil: - forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). -Proof. - intros x BETWEEN. - unfold Z.succ. - cut (Zfloor x = (Zceil x) - 1). { intros; lia. } - apply Zfloor_imp. - split. - { rewrite minus_IZR. - pose proof (Zceil_lb x). - lra. - } - rewrite plus_IZR. - rewrite minus_IZR. - lra. -Qed. - -Lemma ZnearestE_opp - : forall x : R, ZnearestE (- x) = - ZnearestE x. -Proof. - intro x. - unfold ZnearestE. - case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP. - - pose proof (Zfloor_lb x) as LB. - destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT]. - lra. - { set (n := Zfloor x) in *. - rewrite EXACT. - rewrite <- opp_IZR. - rewrite Zfloor_IZR. - rewrite opp_IZR. - rewrite Rcompare_Lt by lra. - reflexivity. - } - rewrite Rcompare_Gt. - { apply Zceil_opp. } - rewrite Zfloor_opp. - rewrite opp_IZR. - rewrite Zceil_non_floor by assumption. - unfold Z.succ. - rewrite plus_IZR. - lra. - - rewrite Rcompare_Eq. - { rewrite Zceil_opp. - rewrite Zfloor_opp. - rewrite Z.even_opp. - rewrite Zceil_non_floor by lra. - rewrite Z.even_succ. - rewrite Z.negb_odd. - destruct (Z.even (Zfloor x)); reflexivity. - } - rewrite Zfloor_opp. - rewrite opp_IZR. - ring_simplify. - rewrite Zceil_non_floor by lra. - unfold Z.succ. - rewrite plus_IZR. - lra. - - rewrite Rcompare_Lt. - { apply Zfloor_opp. } - rewrite Zfloor_opp. - rewrite opp_IZR. - rewrite Zceil_non_floor by lra. - unfold Z.succ. - rewrite plus_IZR. - lra. -Qed. - *) - Ltac field_simplify_den := field_simplify ; [idtac | lra]. Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. @@ -1149,37 +1188,12 @@ Proof. lia. Qed. - -Lemma Znearest_imp2: - forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R. -Proof. - intros. - unfold Znearest. - pose proof (Zfloor_lb x) as FL. - pose proof (Zceil_ub x) as CU. - pose proof (Zceil_non_floor x) as NF. - case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra. - - destruct choice; lra. - - destruct choice. 2: lra. - rewrite NF. 2: lra. - unfold Z.succ. rewrite plus_IZR. lra. - - rewrite NF. 2: lra. - unfold Z.succ. rewrite plus_IZR. lra. -Qed. - -Lemma Rabs_le_rev : forall a b, (Rabs a <= b -> -b <= a <= b)%R. -Proof. - intros a b ABS. - unfold Rabs in ABS. - destruct Rcase_abs in ABS; lra. -Qed. - Theorem ZofB_ne_ball: forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R. Proof. intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H. pose proof (Znearest_imp2 (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS. - pose proof (Rabs_le_rev _ _ ABS). + pose proof (Rabs_le_inv _ _ ABS). lra. Qed. |