Commit 6e34c53e by Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent 24165c3e
 ... ... @@ -270,9 +270,10 @@ Definition bw_and : t -> t -> t. Defined. (* Why3 goal *) Lemma Nth_bw_and : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 n) (nth v2 n))). Lemma Nth_bw_and : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 n) (nth v2 n))). symmetry. apply nth_aux_map2 with (f := fun x y => x && y); easy. Qed. ... ... @@ -283,9 +284,10 @@ Definition bw_or : t -> t -> t. Defined. (* Why3 goal *) Lemma Nth_bw_or : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 n) (nth v2 n))). Lemma Nth_bw_or : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 n) (nth v2 n))). symmetry. apply nth_aux_map2; easy. Qed. ... ... @@ -296,9 +298,10 @@ Definition bw_xor : t -> t -> t. Defined. (* Why3 goal *) Lemma Nth_bw_xor : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 n) (nth v2 n))). Lemma Nth_bw_xor : forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 n) (nth v2 n))). symmetry. apply nth_aux_map2; easy. Qed. ... ... @@ -525,8 +528,10 @@ Lemma bshiftL_iter_nth_high : forall {l} v s m, (0 <= Z.of_nat s)%Z -> (Z.of_nat Qed. (* Why3 goal *) Lemma Lsl_nth_high : forall (b:t) (n:Z) (s:Z), ((0%Z <= s)%Z /\ ((s <= n)%Z /\ (n < size)%Z)) -> ((nth (lsl b s) n) = (nth b (n - s)%Z)). Lemma Lsl_nth_high : forall (b:t) (n:Z) (s:Z), ((0%Z <= s)%Z /\ ((s <= n)%Z /\ (n < size)%Z)) -> ((nth (lsl b s) n) = (nth b (n - s)%Z)). intros. unfold lsl, nth. rewrite <-Z2Nat.id with (n := s) at 2 by omega. ... ... @@ -554,8 +559,9 @@ Lemma Lsl_nth_low_aux : forall {l} x b (n : int), Qed. (* Why3 goal *) Lemma Lsl_nth_low : forall (b:t) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < s)%Z) -> ((nth (lsl b s) n) = false). Lemma Lsl_nth_low : forall (b:t) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < s)%Z) -> ((nth (lsl b s) n) = false). intros. apply Lsl_nth_low_aux. rewrite Z2Nat.id; omega. ... ... @@ -1721,8 +1727,10 @@ Lemma Nth_bv_is_nth : Qed. (* Why3 goal *) Lemma Nth_bv_is_nth2 : forall (x:t) (i:Z), ((0%Z <= i)%Z /\ (i < two_power_size)%Z) -> ((nth_bv x (of_int i)) = (nth x i)). Lemma Nth_bv_is_nth2 : forall (x:t) (i:Z), ((0%Z <= i)%Z /\ (i < two_power_size)%Z) -> ((nth_bv x (of_int i)) = (nth x i)). intros x i h1. rewrite <-Nth_bv_is_nth. rewrite to_uint_of_int by auto. ... ... @@ -1737,9 +1745,10 @@ Definition eq_sub_bv : t -> t -> t -> t -> Prop. Defined. (* Why3 goal *) Lemma eq_sub_bv_def : forall (a:t) (b:t) (i:t) (n:t), let mask := (lsl_bv (sub (lsl_bv one n) one) i) in ((eq_sub_bv a b i n) <-> ((bw_and b mask) = (bw_and a mask))). Lemma eq_sub_bv_def : forall (a:t) (b:t) (i:t) (n:t), let mask := (lsl_bv (sub (lsl_bv one n) one) i) in ((eq_sub_bv a b i n) <-> ((bw_and b mask) = (bw_and a mask))). rewrite Of_int_one. easy. Qed. ... ...
 ... ... @@ -1279,7 +1279,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_int_roundToIntegral : forall (m:ieee_float.RoundingMode.mode) (x:t), Lemma to_int_roundToIntegral : forall (m:ieee_float.RoundingMode.mode) (x:t), ((to_int m x) = (to_int m (roundToIntegral m x))). Proof. now apply to_int_roundToIntegral. ... ... @@ -1294,7 +1295,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z), Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z), (in_safe_int_range i) -> ((to_int m (of_int m i)) = i). Proof. intros m i h1. ... ... @@ -1302,22 +1304,25 @@ Proof. Qed. (* Why3 goal *) Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) -> ((eq x y) -> ((to_int m x) = (to_int m y))). Proof. apply eq_to_int. 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. (* Why3 goal *) Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) -> (t'isFinite (roundToIntegral m x)). Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) -> (t'isFinite (roundToIntegral m x)). Proof. now apply roundToIntegral_is_finite. Qed. ... ...
 ... ... @@ -1172,8 +1172,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. ... ... @@ -1276,7 +1277,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_int_roundToIntegral : forall (m:ieee_float.RoundingMode.mode) (x:t), Lemma to_int_roundToIntegral : forall (m:ieee_float.RoundingMode.mode) (x:t), ((to_int m x) = (to_int m (roundToIntegral m x))). Proof. now apply to_int_roundToIntegral. ... ... @@ -1291,7 +1293,8 @@ Proof. Qed. (* Why3 goal *) Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z), Lemma to_int_of_int : forall (m:ieee_float.RoundingMode.mode) (i:Z), (in_safe_int_range i) -> ((to_int m (of_int m i)) = i). Proof. intros m i h1. ... ... @@ -1299,7 +1302,8 @@ Proof. Qed. (* Why3 goal *) Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), Lemma eq_to_int : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) -> ((eq x y) -> ((to_int m x) = (to_int m y))). Proof. apply eq_to_int. ... ... @@ -1314,8 +1318,9 @@ Proof. Qed. (* Why3 goal *) Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) -> (t'isFinite (roundToIntegral m x)). Lemma roundToIntegral_is_finite : forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) -> (t'isFinite (roundToIntegral m x)). Proof. now apply roundToIntegral_is_finite. Qed. ... ...
 ... ... @@ -64,15 +64,17 @@ now apply Zlt_le_weak. Qed. (* Why3 goal *) Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> (0%Z <= (ZArith.BinInt.Z.quot x y))%Z. Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> (0%Z <= (ZArith.BinInt.Z.quot x y))%Z. intros x y (Hx, Hy). now apply Z.quot_pos. Qed. (* Why3 goal *) Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) -> ((ZArith.BinInt.Z.quot x y) <= 0%Z)%Z. Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) -> ((ZArith.BinInt.Z.quot x y) <= 0%Z)%Z. intros x y (Hx, Hy). generalize (Z.quot_pos (-x) y). rewrite Zquot_opp_l. ... ... @@ -80,15 +82,17 @@ omega. Qed. (* Why3 goal *) Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (ZArith.BinInt.Z.rem x y))%Z. Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (ZArith.BinInt.Z.rem x y))%Z. intros x y (Hx, Zy). now apply Zrem_lt_pos. Qed. (* Why3 goal *) Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((ZArith.BinInt.Z.rem x y) <= 0%Z)%Z. Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((ZArith.BinInt.Z.rem x y) <= 0%Z)%Z. intros x y (Hx, Zy). now apply Zrem_lt_neg. Qed. ... ... @@ -115,14 +119,16 @@ exact Z.rem_1_r. Qed. (* Why3 goal *) Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZArith.BinInt.Z.quot x y) = 0%Z). Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZArith.BinInt.Z.quot x y) = 0%Z). exact Z.quot_small. Qed. (* Why3 goal *) Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZArith.BinInt.Z.rem x y) = x). Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZArith.BinInt.Z.rem x y) = x). exact Z.rem_small. Qed. ... ...
 ... ... @@ -80,7 +80,9 @@ omega. Qed. (* Why3 goal *) Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z). intros x y (Hx,Hy). unfold div. ... ... @@ -126,8 +128,9 @@ now rewrite Zmod_small. Qed. (* Why3 goal *) Lemma Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((div (-x)%Z y) = (-1%Z)%Z). Lemma Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((div (-x)%Z y) = (-1%Z)%Z). intros x y Hxy. assert (h: (x < y \/ x = y)%Z) by omega. destruct h. ... ... @@ -205,8 +208,9 @@ Qed. Open Scope Z_scope. (* Why3 goal *) Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z). Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z). intros x y z h. unfold div. destruct (Z_le_dec 0 (z mod x)). ... ... @@ -218,8 +222,9 @@ generalize (Z_mod_lt z x); auto with zarith. Qed. (* Why3 goal *) Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)). Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)). intros x y z h. unfold mod1. rewrite Div_mult. ... ...
 ... ... @@ -165,8 +165,9 @@ exact Zplus_le_compat_r. Qed. (* Why3 goal *) Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z). Lemma CompatOrderMult : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z). Proof. exact Zmult_le_compat_r. Qed. ... ...
 ... ... @@ -215,7 +215,8 @@ Proof. Qed. (* Why3 goal *) Lemma numof_increasing : forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z), Lemma numof_increasing : forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((numof p i j) <= (numof p i k))%Z. Proof. intros p i j k (h1,h2). ... ...
 ... ... @@ -102,8 +102,9 @@ apply Power_comm2 ; auto with zarith. Qed. (* Why3 goal *) Lemma Power_non_neg : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) -> (0%Z <= (power x y))%Z. Lemma Power_non_neg : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) -> (0%Z <= (power x y))%Z. intros x y (h1,h2). now apply Z.pow_nonneg. Qed. ... ... @@ -111,8 +112,10 @@ Qed. Open Scope Z_scope. (* Why3 goal *) Lemma Power_monotonic : forall (x:Z) (n:Z) (m:Z), ((0%Z < x)%Z /\ ((0%Z <= n)%Z /\ (n <= m)%Z)) -> ((power x n) <= (power x m))%Z. Lemma Power_monotonic : forall (x:Z) (n:Z) (m:Z), ((0%Z < x)%Z /\ ((0%Z <= n)%Z /\ (n <= m)%Z)) -> ((power x n) <= (power x m))%Z. intros. apply Z.pow_le_mono_r; auto with zarith. Qed. ... ...
 ... ... @@ -31,13 +31,14 @@ exact (fix num_occ (l : list a) : int := Defined. (* Why3 goal *) Lemma num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), Lemma num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), match l with | Init.Datatypes.nil => ((num_occ x l) = 0%Z) | (Init.Datatypes.cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\ ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z)) | (Init.Datatypes.cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\ ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z)) end. Proof. intros a a_WT x [|y r]. ... ... @@ -82,9 +83,10 @@ now apply IHl. Qed. (* Why3 goal *) Lemma Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), ((num_occ x (Init.Datatypes.app l1 l2)) = ((num_occ x l1) + (num_occ x l2))%Z). Lemma Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), ((num_occ x (Init.Datatypes.app l1 l2)) = ((num_occ x l1) + (num_occ x l2))%Z). Proof. intros a a_WT x l1 l2. induction l1 as [|l1h l1t IHl1]. ... ...
 ... ... @@ -27,8 +27,8 @@ Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) l1) = (list.NumOcc.num_occ x l2)). (* Why3 goal *) Lemma Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (permut l l). Lemma Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (permut l l). Proof. now intros a a_WT l. Qed. ... ... @@ -41,9 +41,10 @@ now intros a a_WT l1 l2 h1. Qed. (* Why3 goal *) Lemma Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)). Lemma Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)). Proof. intros a a_WT l1 l2 l3 h1 h2 x. now rewrite h1. ... ... @@ -104,9 +105,10 @@ now apply f_equal2. Qed. (* Why3 goal *) Lemma Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), (permut (Init.Datatypes.app l1 l2) (Init.Datatypes.app l2 l1)). Lemma Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), (permut (Init.Datatypes.app l1 l2) (Init.Datatypes.app l2 l1)). Proof. intros a a_WT l1 l2 y. rewrite 2!NumOcc.Append_Num_Occ. ... ... @@ -114,9 +116,10 @@ apply Zplus_comm. Qed. (* Why3 goal *) Lemma Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) -> (list.Mem.mem x l2)). Lemma Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Mem.mem x l1) -> (list.Mem.mem x l2)). Proof. intros a a_WT x l1 l2 h1 h2. apply NumOcc.Mem_Num_Occ. ... ... @@ -125,9 +128,10 @@ now apply NumOcc.Mem_Num_Occ. Qed. (* Why3 goal *) Lemma Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Length.length l1) = (list.Length.length l2)). Lemma Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), (permut l1 l2) -> ((list.Length.length l1) = (list.Length.length l2)). Proof. intros a a_WT l1 l2 h1. revert l2 h1. ... ...
 ... ... @@ -30,7 +30,8 @@ apply excluded_middle_informative. Qed. (* Why3 goal *) Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, Definition set : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (a -> b) -> a -> b -> (a -> b). Proof. intros a a_WT b b_WT m x y. ... ... @@ -41,9 +42,11 @@ exact (m x'). Defined. (* Why3 goal *) Lemma set_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (f:(a -> b)) (x:a) (v:b) (y:a), ((y = x) -> (((set f x v) y) = v)) /\ ((~ (y = x)) -> (((set f x v) y) = (f y))). Lemma set_def : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (f:(a -> b)) (x:a) (v:b) (y:a), ((y = x) -> (((set f x v) y) = v)) /\ ((~ (y = x)) -> (((set f x v) y) = (f y))). Proof. intros a a_WT b b_WT f x v y. unfold set. ... ...
 ... ... @@ -22,9 +22,10 @@ Import Rbasic_fun. (* abs is replaced with (Reals.Rbasic_fun.Rabs x) by the coq driver *) (* Why3 goal *) Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((Reals.Rbasic_fun.Rabs x) = x)) /\ ((~ (0%R <= x)%R) -> ((Reals.Rbasic_fun.Rabs x) = (-x)%R)). Lemma abs_def : forall (x:R), ((0%R <= x)%R -> ((Reals.Rbasic_fun.Rabs x) = x)) /\ ((~ (0%R <= x)%R) -> ((Reals.Rbasic_fun.Rabs x) = (-x)%R)). split ; intros H. apply Rabs_right. now apply Rle_ge. ... ... @@ -33,8 +34,9 @@ now apply Rnot_le_lt. Qed. (* Why3 goal *) Lemma Abs_le : forall (x:R) (y:R), ((Reals.Rbasic_fun.Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\ (x <= y)%R). Lemma Abs_le : forall (x:R) (y:R), ((Reals.Rbasic_fun.Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\ (x <= y)%R). intros x y. unfold Rabs. case Rcase_abs ; intros H ; (split ; [intros H0;split | intros (H0,H1)]). ... ... @@ -64,19 +66,22 @@ exact Rabs_pos. Qed. (* Why3 goal *) Lemma Abs_sum : forall (x:R) (y:R), Lemma Abs_sum : forall (x:R) (y:R), ((Reals.Rbasic_fun.Rabs (x + y)%R) <= ((Reals.Rbasic_fun.Rabs x) + (Reals.Rbasic_fun.Rabs y))%R)%R. exact Rabs_triang. Qed. (* Why3 goal *) Lemma Abs_prod : forall (x:R) (y:R), Lemma Abs_prod : forall (x:R) (y:R), ((Reals.Rbasic_fun.Rabs (x * y)%R) = ((Reals.Rbasic_fun.Rabs x) * (Reals.Rbasic_fun.Rabs y))%R). exact Rabs_mult. Qed. (* Why3 goal *) Lemma triangular_inequality : forall (x:R) (y:R) (z:R), Lemma triangular_inequality : forall (x:R) (y:R) (z:R), ((Reals.Rbasic_fun.Rabs (x - z)%R) <= ((Reals.Rbasic_fun.Rabs (x - y)%R) + (Reals.Rbasic_fun.Rabs (y - z)%R))%R)%R. intros x y z. replace (x - z)%R with ((x - y) + (y - z))%R by ring. ... ...
 ... ... @@ -52,8 +52,8 @@ now apply ln_mult. Qed. (* Why3 goal *) Lemma Log_exp : forall (x:R), ((Reals.Rpower.ln (Reals.Rtrigo_def.exp x)) = x). Lemma Log_exp : forall (x:R), ((Reals.Rpower.ln (Reals.Rtrigo_def.exp x)) = x). exact ln_exp. Qed. ... ...
 ... ... @@ -83,8 +83,9 @@ now apply Rtrigo_def.exp_0. Qed. (* Why3 goal *) Lemma Pow_x_two : forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 2%R) = (Reals.RIneq.Rsqr x)). Lemma Pow_x_two : forall (x:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x 2%R) = (Reals.RIneq.Rsqr x)). Proof. intros x h1. rewrite (Rpower_pow 2) by easy. ... ...
 ... ... @@ -136,8 +136,9 @@ reflexivity. Qed. (* Why3 goal *) Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x + y)%R / z)%R = ((x / z)%R + (y / z)%R)%R). Lemma add_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x + y)%R / z)%R = ((x / z)%R + (y / z)%R)%R). Proof. intros. field. ... ... @@ -145,8 +146,9 @@ assumption. Qed. (* Why3 goal *) Lemma sub_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x - y)%R / z)%R = ((x / z)%R - (y / z)%R)%R). Lemma sub_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x - y)%R / z)%R = ((x / z)%R - (y / z)%R)%R). Proof. intros. field. ... ... @@ -154,8 +156,8 @@ assumption. Qed. (* Why3 goal *) Lemma neg_div : forall (x:R) (y:R), (~ (y = 0%R)) -> (((-x)%R / y)%R = (-(x / y)%R)%R). Lemma neg_div : forall (x:R) (y:R), (~ (y = 0%R)) -> (((-x)%R / y)%R = (-(x / y)%R)%R). Proof. intros. field. ... ... @@ -163,16 +165,18 @@ assumption. Qed. (* Why3 goal *) Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x * y)%R / z)%R = (x * (y / z)%R)%R). Lemma assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = 0%R)) -> (((x * y)%R / z)%R = (x * (y / z)%R)%R). Proof. intros x y z _. apply Rmult_assoc. Qed. (* Why3 goal *) Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ ~ (z = 0%R)) -> (((x / y)%R / z)%R = (x / (y * z)%R)%R). Lemma assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ ~ (z = 0%R)) -> (((x / y)%R / z)%R = (x / (y * z)%R)%R). Proof. intros x y z (Zy, Zz). unfold Rdiv. ... ... @@ -181,8 +185,9 @@ now rewrite Rinv_mult_distr. Qed. (* Why3 goal *) Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ ~ (z = 0%R)) -> ((x / (y / z)%R)%R = ((x * z)%R / y)%R). Lemma assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = 0%R)) /\ ~ (z = 0%R)) -> ((x / (y / z)%R)%R = ((x * z)%R / y)%R). Proof. intros x y z (Zy, Zz). field. ... ... @@ -233,8 +238,9 @@ exact (Rplus_le_compat_r z x y). Qed. (* Why3 goal *) Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (x <= y)%R -> ((0%R <= z)%R -> ((x * z)%R <= (y * z)%R)%R). Lemma CompatOrderMult : forall (x:R) (y:R) (z:R), (x <= y)%R -> ((0%R <= z)%R -> ((x * z)%R <= (y * z)%R)%R). Proof. intros x y z H Zz. now apply Rmult_le_compat_r. ... ...
 ... ... @@ -91,8 +91,9 @@ Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)) : Prop := forall (x:a), ~ (mem x s). (* Why3 goal *) Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, (is_empty (map.Const.const false: (a -> bool))). Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, (is_empty (map.Const.const false: (a -> bool))). Proof. now intros a a_WT x. Qed. ... ... @@ -118,8 +119,10 @@ destruct why_decidable_eq ; intuition. Qed. (* Why3 goal *) Lemma add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> bool)), (mem x s) -> ((map.Map.set (map.Map.set s x false) x true) = s). Lemma add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> bool)), (mem x s) -> ((map.Map.set (map.Map.set s x false) x true) = s). Proof. intros a a_WT x s h1. apply extensionality; intro y. ... ... @@ -129,9 +132,10 @@ destruct (why_decidable_eq y x) as [->|H] ; intuition. Qed. (* Why3 goal *) Lemma remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a -> bool)), ((map.Map.set (map.Map.set s x true) x false) = (map.Map.set s x false)). Lemma remove_add : forall {a:Type} {a_WT:WhyType a}