Commit 94ff3db7 by Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent f2a36c56
 ... ... @@ -437,8 +437,8 @@ Proof. Qed. (* Why3 goal *) Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Proof. apply eq_trans. Qed. ... ... @@ -479,15 +479,15 @@ Proof. Qed. (* Why3 goal *) Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Proof. apply le_lt_trans. Qed. (* Why3 goal *) Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Proof. apply lt_le_trans. Qed. ... ... @@ -1034,7 +1034,7 @@ Proof. Qed. (* Why3 goal *) Definition is_int: t -> Prop. Definition is_int : t -> Prop. Proof. apply is_int. Defined. ... ... @@ -1124,8 +1124,9 @@ Proof. Qed. (* Why3 goal *) Lemma is_int_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> (in_int_range (to_int m x)). Lemma is_int_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> (in_int_range (to_int m x)). Proof. now apply is_int_to_int. Qed. ... ... @@ -1137,15 +1138,17 @@ Proof. Qed. (* Why3 goal *) Lemma int_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((t'real x) = (BuiltIn.IZR (to_int m x))). Lemma int_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((t'real x) = (BuiltIn.IZR (to_int m x))). Proof. apply int_to_real. Qed. (* Why3 goal *) Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int i) -> (eq (roundToIntegral m i) i). Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int i) -> (eq (roundToIntegral m i) i). Proof. now apply truncate_int. Qed. ... ... @@ -1167,8 +1170,9 @@ Proof. Qed. (* Why3 goal *) Lemma ceil_le : forall (x:t), (t'isFinite x) -> (le x (roundToIntegral ieee_float.RoundingMode.RTP x)). Lemma ceil_le : forall (x:t), (t'isFinite x) -> (le x (roundToIntegral ieee_float.RoundingMode.RTP x)). Proof. now apply ceil_le. Qed. ... ...
 ... ... @@ -255,14 +255,14 @@ Proof. Qed. (* Why3 goal *) Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((t'isFinite x) /\ ((t'real x) = 0%R)). Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((t'isFinite x) /\ ((t'real x) = 0%R)). Proof. apply zero_to_real. Qed. (* Why3 goal *) Definition of_int: ieee_float.RoundingMode.mode -> Z -> t. Definition of_int : ieee_float.RoundingMode.mode -> Z -> t. Proof. now apply z_to_fp. Defined. ... ... @@ -313,8 +313,8 @@ Definition in_range (x:R) : Prop := (x <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R. (* Why3 assumption *) Definition in_int_range (i:Z): Prop := ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z. Definition in_int_range (i:Z) : Prop := ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z. (* Why3 goal *) Lemma is_finite : forall (x:t), (t'isFinite x) -> (in_range (t'real x)). ... ... @@ -361,15 +361,15 @@ Proof. Qed. (* Why3 goal *) Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R. Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R. Proof. apply Round_down_le. Qed. (* Why3 goal *) Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R. Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R. Proof. apply Round_up_ge. Qed. ... ... @@ -389,7 +389,7 @@ Proof. Qed. (* Why3 assumption *) Definition in_safe_int_range (i:Z): Prop := Definition in_safe_int_range (i:Z) : Prop := ((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z. (* Why3 goal *) ... ... @@ -436,8 +436,8 @@ Proof. Qed. (* Why3 goal *) Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Proof. apply eq_trans. Qed. ... ... @@ -478,15 +478,15 @@ Proof. Qed. (* Why3 goal *) Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Proof. apply le_lt_trans. Qed. (* Why3 goal *) Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Proof. apply lt_le_trans. Qed. ... ... @@ -620,7 +620,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop := end. (* Why3 assumption *) Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t): Prop := Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop := (is_zero x) -> match m with | ieee_float.RoundingMode.RTN => (is_negative x) ... ... @@ -1033,7 +1033,7 @@ Proof. Qed. (* Why3 goal *) Definition is_int: t -> Prop. Definition is_int : t -> Prop. Proof. apply is_int. Defined. ... ... @@ -1123,8 +1123,9 @@ Proof. Qed. (* Why3 goal *) Lemma is_int_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> (in_int_range (to_int m x)). Lemma is_int_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> (in_int_range (to_int m x)). Proof. now apply is_int_to_int. Qed. ... ... @@ -1136,15 +1137,17 @@ Proof. Qed. (* Why3 goal *) Lemma int_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((t'real x) = (BuiltIn.IZR (to_int m x))). Lemma int_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((t'real x) = (BuiltIn.IZR (to_int m x))). Proof. apply int_to_real. Qed. (* Why3 goal *) Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int i) -> (eq (roundToIntegral m i) i). Lemma truncate_int : forall (m:ieee_float.RoundingMode.mode) (i:t), (is_int i) -> (eq (roundToIntegral m i) i). Proof. now apply truncate_int. Qed. ... ... @@ -1300,8 +1303,9 @@ Proof. Qed. (* Why3 goal *) Lemma neg_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((to_int m (neg x)) = (-(to_int m x))%Z). Lemma neg_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t), (is_int x) -> ((to_int m (neg x)) = (-(to_int m x))%Z). Proof. apply neg_to_int. Qed. ... ...
 ... ... @@ -688,8 +688,8 @@ Proof. Qed. (* Why3 goal *) Lemma is_not_finite : forall (x:t), (~ (is_finite x)) <-> ((is_infinite x) \/ (is_nan x)). Lemma is_not_finite : forall (x:t), (~ (is_finite x)) <-> ((is_infinite x) \/ (is_nan x)). Proof. intros x. destruct x; split; intro h; try easy. ... ... @@ -863,13 +863,13 @@ auto. Qed. (* Why3 goal *) Definition round: ieee_float.RoundingMode.mode -> R -> R. Definition round : ieee_float.RoundingMode.mode -> R -> R. Proof. exact (fun m => round radix2 fexp (round_mode m)). Defined. (* Why3 goal *) Definition max_real: R. Definition max_real : R. Proof. exact ((1 - bpow radix2 (- sb)) * bpow radix2 emax). Defined. ... ... @@ -952,7 +952,7 @@ Proof. Qed. (* Why3 goal *) Definition max_int: Z. Definition max_int : Z. Proof. exact (2 ^ emax - 2 ^ (emax - sb))%Z. Defined. ... ... @@ -975,12 +975,12 @@ Proof. Qed. (* Why3 assumption *) Definition in_range (x:R): Prop := ((-max_real)%R <= x)%R /\ (x <= max_real)%R. Definition in_range (x:R) : Prop := ((-max_real)%R <= x)%R /\ (x <= max_real)%R. (* Why3 assumption *) Definition in_int_range (i:Z): Prop := ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z. Definition in_int_range (i:Z) : Prop := ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z. Lemma in_range_bpow_radix2_emax: forall x, in_range x -> Rabs x < bpow radix2 emax. Proof. ... ... @@ -1029,7 +1029,7 @@ Proof. Qed. (* Why3 assumption *) Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R): Prop := Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop := (in_range (round m x)). Lemma no_overflow_Rabs_round_max_real: forall {m} {x}, no_overflow m x <-> Rabs (round m x) <= max_real. ... ... @@ -1079,8 +1079,9 @@ Proof. Qed. (* Why3 goal *) Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode) (x:R), (in_range x) -> (no_overflow m x). Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode) (x:R), (in_range x) -> (no_overflow m x). Proof. intros m x h1. rewrite no_overflow_Rabs_round_max_real. ... ... @@ -1092,7 +1093,8 @@ rewrite Abs.Abs_le; easy. Qed. (* Why3 goal *) Lemma Round_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R), Lemma Round_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R), (x <= y)%R -> ((round m x) <= (round m y))%R. Proof. intros m x y h1. ... ... @@ -1133,16 +1135,16 @@ apply generic_format_B2R. Qed. (* Why3 goal *) Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R. Lemma Round_down_le : forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R. Proof with auto with typeclass_instances. intros x. apply round_DN_pt... Qed. (* Why3 goal *) Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R. Lemma Round_up_ge : forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R. Proof with auto with typeclass_instances. intros x. apply round_UP_pt... ... ... @@ -1167,7 +1169,7 @@ now rewrite Ropp_involutive. Qed. (* Why3 goal *) Definition pow2sb: Z. Definition pow2sb : Z. Proof. exact (Zpower 2 sb). Defined. ... ... @@ -1179,8 +1181,8 @@ Proof. Qed. (* Why3 assumption *) Definition in_safe_int_range (i:Z): Prop := ((-pow2sb)%Z <= i)%Z /\ (i <= pow2sb)%Z. Definition in_safe_int_range (i:Z) : Prop := ((-pow2sb)%Z <= i)%Z /\ (i <= pow2sb)%Z. Lemma max_rep_int_bounded: bounded sb emax (shift_pos (sb_pos - 1) 1) 1 = true. Proof. ... ... @@ -1300,8 +1302,9 @@ Proof. Qed. (* Why3 assumption *) Definition same_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_positive y)) \/ ((is_negative x) /\ (is_negative y)). Definition same_sign (x:t) (y:t) : Prop := ((is_positive x) /\ (is_positive y)) \/ ((is_negative x) /\ (is_negative y)). Hint Unfold same_sign. ... ... @@ -1314,8 +1317,9 @@ Proof. Qed. (* Why3 assumption *) Definition diff_sign (x:t) (y:t): Prop := ((is_positive x) /\ (is_negative y)) \/ ((is_negative x) /\ (is_positive y)). Definition diff_sign (x:t) (y:t) : Prop := ((is_positive x) /\ (is_negative y)) \/ ((is_negative x) /\ (is_positive y)). Hint Unfold same_sign. ... ... @@ -1403,8 +1407,8 @@ unfold eq; intro h; rewrite Bcompare_swap, h; easy. Qed. (* Why3 goal *) Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)). Proof. intros x y z h1 h2. destruct x, y, z; auto; destruct b, b0, b1; auto; try easy; ... ... @@ -1545,8 +1549,8 @@ Proof. Qed. (* Why3 goal *) Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Lemma le_lt_trans : forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). Proof. intros x y z (h,h1). destruct h as [h|h]. ... ... @@ -1555,8 +1559,8 @@ Proof. Qed. (* Why3 goal *) Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Lemma lt_le_trans : forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). Proof. intros x y z (h1,h2). destruct h2 as [h2|h2]. ... ... @@ -1687,8 +1691,8 @@ Proof. Qed. (* Why3 goal *) Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (is_finite y)). Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (is_finite y)). Proof. intros x y z h1 h2. destruct x, y, z; destruct b, b0, b1; easy. ... ... @@ -1844,11 +1848,12 @@ destruct h3 as [(h3,h4)|(h3,h4)]. Qed. (* Why3 assumption *) Definition product_sign (z:t) (x:t) (y:t): Prop := ((same_sign x y) -> (is_positive z)) /\ ((diff_sign x y) -> (is_negative z)). Definition product_sign (z:t) (x:t) (y:t) : Prop := ((same_sign x y) -> (is_positive z)) /\ ((diff_sign x y) -> (is_negative z)). (* Why3 assumption *) Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop := Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop := match m with | ieee_float.RoundingMode.RTN => ((is_positive x) -> ((is_finite x) /\ ((to_real x) = max_real))) /\ ((~ (is_positive x)) -> (is_infinite x)) ... ... @@ -2237,8 +2242,8 @@ Proof. Qed. (* Why3 assumption *) Definition same_sign_real (x:t) (r:R): Prop := ((is_positive x) /\ (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R). Definition same_sign_real (x:t) (r:R) : Prop := ((is_positive x) /\ (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R). Lemma sign_FF_overflow : forall m b, sign_FF (binary_overflow sb emax m b) = b. ... ...
 ... ... @@ -19,9 +19,10 @@ Require int.Int. (* abs is replaced with (ZArith.BinInt.Z.abs x) by the coq driver *) (* Why3 goal *) Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\ ((~ (0%Z <= x)%Z) -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)). Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\ ((~ (0%Z <= x)%Z) -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)). intros x. split ; intros H. now apply Zabs_eq. ... ...
 ... ... @@ -127,8 +127,9 @@ exact Z.rem_small. Qed. (* Why3 goal *) Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) = (y + (ZArith.BinInt.Z.quot z x))%Z). intros x y z (Hx&Hy&Hz). rewrite (Zplus_comm y). ... ... @@ -143,8 +144,9 @@ now rewrite H in Hx. Qed. (* Why3 goal *) Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZArith.BinInt.Z.rem ((x * y)%Z + z)%Z x) = (ZArith.BinInt.Z.rem z x)). intros x y z (Hx&Hy&Hz). rewrite Zplus_comm, Zmult_comm. ... ...
 ... ... @@ -31,16 +31,19 @@ exact (x - y * div x y)%Z. Defined. (* Why3 goal *) Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). intros x y Zy. unfold mod1, div. case Z_le_dec ; intros H ; ring. Qed. (* Why3 goal *) Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z). Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z). intros x y Zy. zify. assert (H1 := Z_mod_neg x y). ... ... @@ -112,8 +115,8 @@ now rewrite Zmod_1_r, Zdiv_1_r. Qed. (* Why3 goal *) Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z). Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z). intros x y Hxy. unfold div. case Z_le_dec ; intros H. ... ... @@ -170,8 +173,8 @@ rewrite Div_inf; auto with zarith. Qed. (* Why3 goal *) Lemma Div_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z). Lemma Div_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z). intros y Hy. unfold div. assert (h1: (1 mod y = 1)%Z). ... ... @@ -192,8 +195,8 @@ rewrite Div_1_left; auto with zarith. Qed. (* Why3 goal *) Lemma Mod_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z). Lemma Mod_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z). intros y Hy. unfold mod1. rewrite Div_minus1_left; auto with zarith. ... ...
 ... ... @@ -19,9 +19,10 @@ Require int.Int. (* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *) (* Why3 goal *) Lemma min_def : forall (x:Z) (y:Z), ((x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x)) /\ ((~ (x <= y)%Z) -> ((ZArith.BinInt.Z.min x y) = y)). Lemma min_def : forall (x:Z) (y:Z), ((x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = x)) /\ ((~ (x <= y)%Z) -> ((ZArith.BinInt.Z.min x y) = y)). Proof. intros x y. split ; intros H. ... ... @@ -34,9 +35,10 @@ Qed. (* max is replaced with (ZArith.BinInt.Z.max x x1) by the coq driver *) (* Why3 goal *) Lemma max_def : forall (x:Z) (y:Z), ((x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y)) /\ ((~ (x <= y)%Z) -> ((ZArith.BinInt.Z.max x y) = x)). Lemma max_def : forall (x:Z) (y:Z), ((x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = y)) /\ ((~ (x <= y)%Z) -> ((ZArith.BinInt.Z.max x y) = x)). Proof. intros x y. split ; intros H. ... ... @@ -46,31 +48,32 @@ omega. Qed. (* Why3 goal *) Lemma Min_r : forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.min x y) = y). Lemma Min_r : forall (x:Z) (y:Z), (y <= x)%Z -> ((ZArith.BinInt.Z.min x y) = y). exact Zmin_r. Qed. (* Why3 goal *) Lemma Max_l : forall (x:Z) (y:Z), (y <= x)%Z ->