Commit 9ef42e17 by Guillaume Melquiond

### Update parts of Coq realizations whose printing looks sane.

parent 5a92d21d
 ... ... @@ -212,8 +212,8 @@ omega. Qed. (* Why3 goal *) Lemma nth_out_of_bound : forall (x:t) (n:Z), ((n < 0%Z)%Z \/ (size <= n)%Z) -> ((nth x n) = false). Lemma nth_out_of_bound : forall (x:t) (n:Z), ((n < 0%Z)%Z \/ (size <= n)%Z) -> ((nth x n) = false). intros. unfold nth. rewrite nth_aux_out_of_bound; auto with zarith. ... ... @@ -1202,8 +1202,8 @@ Lemma to_int_def : forall (x:t), ((is_signed_positive x) -> Qed. (* Why3 goal *) Lemma to_uint_extensionality : forall (v:t) (v':t), ((to_uint v) = (to_uint v')) -> (v = v'). Lemma to_uint_extensionality : forall (v:t) (v':t), ((to_uint v) = (to_uint v')) -> (v = v'). unfold to_uint. intros v v'. rewrite Nat2Z.inj_iff. ... ... @@ -1211,8 +1211,8 @@ Lemma to_uint_extensionality : forall (v:t) (v':t), Qed. (* Why3 goal *) Lemma to_int_extensionality : forall (v:t) (v':t), ((to_int v) = (to_int v')) -> (v = v'). Lemma to_int_extensionality : forall (v:t) (v':t), ((to_int v) = (to_int v')) -> (v = v'). apply twos_complement_extensionality. Qed. ... ... @@ -1220,8 +1220,8 @@ Qed. Definition uint_in_range (i:Z) : Prop := (0%Z <= i)%Z /\ (i <= max_int)%Z. (* Why3 goal *) Lemma to_uint_bounds : forall (v:t), (0%Z <= (to_uint v))%Z /\ ((to_uint v) < two_power_size)%Z. Lemma to_uint_bounds : forall (v:t), (0%Z <= (to_uint v))%Z /\ ((to_uint v) < two_power_size)%Z. intros v. unfold to_uint, uint_in_range. split. ... ... @@ -1430,8 +1430,8 @@ Lemma zeros_sign_false: Bsign last_bit zeros = false. Qed. (* Why3 goal *) Lemma positive_is_ge_zeros : forall (x:t), (is_signed_positive x) <-> (sge x zeros). Lemma positive_is_ge_zeros : forall (x:t), (is_signed_positive x) <-> (sge x zeros). intros. unfold is_signed_positive, sge, to_int, twos_complement, size_nat. rewrite zeros_sign_false. destruct Bsign. ... ... @@ -1586,8 +1586,8 @@ Definition lsr_bv : t -> t -> t. Defined. (* Why3 goal *) Lemma lsr_bv_is_lsr : forall (x:t) (n:t), ((lsr_bv x n) = (lsr x (to_uint n))). Lemma lsr_bv_is_lsr : forall (x:t) (n:t), ((lsr_bv x n) = (lsr x (to_uint n))). easy. Qed. ... ... @@ -1616,8 +1616,8 @@ Definition lsl_bv : t -> t -> t. Defined. (* Why3 goal *) Lemma lsl_bv_is_lsl : forall (x:t) (n:t), ((lsl_bv x n) = (lsl x (to_uint n))). Lemma lsl_bv_is_lsl : forall (x:t) (n:t), ((lsl_bv x n) = (lsl x (to_uint n))). easy. Qed. ... ... @@ -1640,14 +1640,14 @@ Definition rotate_left_bv : t -> t -> t. Defined. (* Why3 goal *) Lemma rotate_left_bv_is_rotate_left : forall (v:t) (n:t), ((rotate_left_bv v n) = (rotate_left v (to_uint n))). Lemma rotate_left_bv_is_rotate_left : forall (v:t) (n:t), ((rotate_left_bv v n) = (rotate_left v (to_uint n))). trivial. Qed. (* Why3 goal *) Lemma rotate_right_bv_is_rotate_right : forall (v:t) (n:t), ((rotate_right_bv v n) = (rotate_right v (to_uint n))). Lemma rotate_right_bv_is_rotate_right : forall (v:t) (n:t), ((rotate_right_bv v n) = (rotate_right v (to_uint n))). trivial. Qed. ... ...
 ... ... @@ -255,8 +255,8 @@ 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. ... ... @@ -274,8 +274,8 @@ Proof. Defined. (* Why3 goal *) Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Proof. apply zero_of_int. Qed. ... ... @@ -302,7 +302,8 @@ Proof. Defined. (* Why3 goal *) Lemma max_real_int : ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)). Lemma max_real_int : ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)). Proof. unfold max_int. now rewrite mult_IZR, <- !Z2R_IZR. ... ... @@ -314,8 +315,8 @@ Definition in_range (x:R) : Prop := (x <= (33554430 * 10141204801825835211973625643008)%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)). ... ... @@ -362,15 +363,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. ... ... @@ -390,8 +391,8 @@ Proof. Qed. (* Why3 assumption *) Definition in_safe_int_range (i:Z): Prop := ((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z. Definition in_safe_int_range (i:Z) : Prop := ((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z. (* Why3 goal *) Lemma Exact_rounding_for_integers : forall (m:ieee_float.RoundingMode.mode) ... ... @@ -403,12 +404,14 @@ 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)). (* 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)). (* Why3 goal *) Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) -> ... ... @@ -530,50 +533,50 @@ Proof. Qed. (* Why3 goal *) Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)). Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)). Proof. apply lt_lt_finite. Qed. (* Why3 goal *) Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R). Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R). Proof. apply positive_to_real. Qed. (* Why3 goal *) Lemma to_real_positive : forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)). Lemma to_real_positive : forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)). Proof. apply to_real_positive. Qed. (* Why3 goal *) Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R). Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R). Proof. apply negative_to_real. Qed. (* Why3 goal *) Lemma to_real_negative : forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)). Lemma to_real_negative : forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)). Proof. apply to_real_negative. Qed. (* Why3 goal *) Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Proof. apply negative_xor_positive. Qed. (* Why3 goal *) Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Proof. apply negative_or_positive. Qed. ... ... @@ -600,8 +603,9 @@ Proof. 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 := ... ... @@ -621,7 +625,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) ... ...
 ... ... @@ -274,8 +274,8 @@ Proof. Defined. (* Why3 goal *) Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Proof. apply zero_of_int. Qed. ... ... @@ -402,12 +402,14 @@ 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)). (* 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)). (* Why3 goal *) Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) -> ... ... @@ -529,50 +531,50 @@ Proof. Qed. (* Why3 goal *) Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)). Lemma lt_lt_finite : forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)). Proof. apply lt_lt_finite. Qed. (* Why3 goal *) Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R). Lemma positive_to_real : forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R). Proof. apply positive_to_real. Qed. (* Why3 goal *) Lemma to_real_positive : forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)). Lemma to_real_positive : forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)). Proof. apply to_real_positive. Qed. (* Why3 goal *) Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R). Lemma negative_to_real : forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R). Proof. apply negative_to_real. Qed. (* Why3 goal *) Lemma to_real_negative : forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)). Lemma to_real_negative : forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)). Proof. apply to_real_negative. Qed. (* Why3 goal *) Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Proof. apply negative_xor_positive. Qed. (* Why3 goal *) Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Proof. apply negative_or_positive. Qed. ... ... @@ -599,8 +601,9 @@ Proof. 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 := ... ...
 ... ... @@ -782,8 +782,8 @@ Proof. Qed. (* Why3 goal *) Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((is_finite x) /\ ((to_real x) = 0%R)). Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((is_finite x) /\ ((to_real x) = 0%R)). Proof. unfold is_zero. assert (is_finite zeroF) by easy. ... ... @@ -856,8 +856,8 @@ Proof. Qed. (* Why3 goal *) Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)). Proof. auto. Qed. ... ... @@ -1699,8 +1699,8 @@ destruct x, y, z; destruct b, b0, b1; easy. Qed. (* Why3 goal *) Lemma positive_to_real : forall (x:t), (is_finite x) -> ((is_positive x) -> (0%R <= (to_real x))%R). Lemma positive_to_real : forall (x:t), (is_finite x) -> ((is_positive x) -> (0%R <= (to_real x))%R). Proof. intros x h1 h2. assert (is_finite zeroF) as zero_is_finite by easy. ... ... @@ -1731,8 +1731,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_real_positive : forall (x:t), (is_finite x) -> ((0%R < (to_real x))%R -> (is_positive x)). Lemma to_real_positive : forall (x:t), (is_finite x) -> ((0%R < (to_real x))%R -> (is_positive x)). Proof. intros x h1 h2. assert (is_finite zeroF) as zero_is_finite by easy. ... ... @@ -1741,8 +1741,8 @@ Proof. Qed. (* Why3 goal *) Lemma negative_to_real : forall (x:t), (is_finite x) -> ((is_negative x) -> ((to_real x) <= 0%R)%R). Lemma negative_to_real : forall (x:t), (is_finite x) -> ((is_negative x) -> ((to_real x) <= 0%R)%R). Proof. intros x h1 h2. assert (is_finite zeroF) as zero_is_finite by easy. ... ... @@ -1773,8 +1773,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_real_negative : forall (x:t), (is_finite x) -> (((to_real x) < 0%R)%R -> (is_negative x)). Lemma to_real_negative : forall (x:t), (is_finite x) -> (((to_real x) < 0%R)%R -> (is_negative x)). Proof. intros x h1 h2. assert (is_finite zeroF) as zero_is_finite by easy. ... ... @@ -1783,16 +1783,16 @@ Proof. Qed. (* Why3 goal *) Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Lemma negative_xor_positive : forall (x:t), ~ ((is_positive x) /\ (is_negative x)). Proof. intros x. destruct x ; destruct b; easy. Qed. (* Why3 goal *) Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Lemma negative_or_positive : forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). Proof. intros x h1. destruct x ; destruct b; simpl; auto; now elim h1. ... ... @@ -1868,7 +1868,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) ... ... @@ -3507,7 +3507,7 @@ Proof. Qed. (* Why3 goal *) Definition is_int: t -> Prop. Definition is_int : t -> Prop. Proof. exact (fun x => is_finite x /\ is_intR (to_real x)). Defined. ... ...
 ... ... @@ -52,8 +52,9 @@ easy. Qed. (* Why3 goal *) Lemma Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x (n + 1%Z)%Z) = (infix_as x (power x n))). Lemma Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x (n + 1%Z)%Z) = (infix_as x (power x n))). Proof. intros x n h1. unfold power. ... ... @@ -62,8 +63,9 @@ now rewrite Zabs_nat_Zsucc. Qed. (* Why3 goal *) Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (infix_as x (power x (n - 1%Z)%Z))). Lemma Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (infix_as x (power x (n - 1%Z)%Z))). Proof. intros x n h1. rewrite <- Power_s; auto with zarith. ... ...
 ... ... @@ -38,8 +38,8 @@ exact Zle_lt_or_eq_iff. Qed. (* Why3 goal *) Lemma Assoc : forall (x:Z) (y:Z) (z:Z), (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z). Lemma Assoc : forall (x:Z) (y:Z) (z:Z), (((x + y)%Z + z)%Z = (x + (y + z)%Z)%Z). Proof. intros x y z. apply sym_eq. ... ... @@ -77,8 +77,8 @@ exact Zplus_comm. Qed. (* Why3 goal *) Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z), (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z). Lemma Assoc1 : forall (x:Z) (y:Z) (z:Z), (((x * y)%Z * z)%Z = (x * (y * z)%Z)%Z). Proof. intros x y z. apply sym_eq. ... ... @@ -86,16 +86,16 @@ apply Zmult_assoc. Qed. (* Why3 goal *) Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z), ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z). Lemma Mul_distr_l : forall (x:Z) (y:Z) (z:Z), ((x * (y + z)%Z)%Z = ((x * y)%Z + (x * z)%Z)%Z). Proof. intros x y z. apply Zmult_plus_distr_r. Qed. (* Why3 goal *) Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z), (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z). Lemma Mul_distr_r : forall (x:Z) (y:Z) (z:Z), (((y + z)%Z * x)%Z = ((y * x)%Z + (z * x)%Z)%Z). Proof. intros x y z. apply Zmult_plus_distr_l. ... ... @@ -127,8 +127,8 @@ apply Zle_refl. Qed. (* Why3 goal *) Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z -> (x <= z)%Z). Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z -> (x <= z)%Z). Proof. exact Zle_trans. Qed. ... ... @@ -158,8 +158,8 @@ now left. Qed. (* Why3 goal *) Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((x + z)%Z <= (y + z)%Z)%Z. Lemma CompatOrderAdd : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((x + z)%Z <= (y + z)%Z)%Z. Proof. exact Zplus_le_compat_r. Qed. ... ...
 ... ... @@ -22,7 +22,8 @@ Require number.Parity. (* Hack so that Why3 does not override the notation below. (* Why3 assumption *) Definition divides (d:Z) (n:Z): Prop := ((d = 0%Z) -> (n = 0%Z)) /\ Definition divides (d:Z) (n:Z) : Prop := ((d = 0%Z) -> (n = 0%Z)) /\ ((~ (d = 0%Z)) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)). *) ... ... @@ -31,8 +32,8 @@ Require Import Znumtheory. Notation divides := Zdivide (only parsing).