Commit f945cbf6 by Guillaume Melquiond

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

parent ecb58b34
 ... ... @@ -22,7 +22,7 @@ Require int.Int. 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)). (~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)). intros x. split ; intros H. now apply Zabs_eq. ... ...
 ... ... @@ -35,8 +35,8 @@ Qed. Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\ ((ZArith.BinInt.Z.quot x y) <= x)%Z). (0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\ ((ZArith.BinInt.Z.quot x y) <= x)%Z. intros x y (Hx,Hy). split. now apply Z.quot_pos. ... ... @@ -53,9 +53,9 @@ Qed. (* Why3 goal *) Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\ ((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z). ~ (y = 0%Z) -> ((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\ ((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z. intros x y Zy. destruct (Zle_or_lt 0 x) as [Hx|Hx]. refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _). ... ... @@ -103,7 +103,8 @@ Qed. (* Why3 goal *) Lemma Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((ZArith.BinInt.Z.abs ((ZArith.BinInt.Z.quot x y) * y)%Z) <= (ZArith.BinInt.Z.abs x))%Z. ((ZArith.BinInt.Z.abs ((ZArith.BinInt.Z.quot x y) * y)%Z) <= (ZArith.BinInt.Z.abs x))%Z. intros x y Zy. rewrite Zmult_comm. zify. ... ...
 ... ... @@ -32,8 +32,7 @@ Defined. (* Why3 goal *) Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). 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. ... ... @@ -42,8 +41,8 @@ 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). ~ (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). ... ... @@ -59,7 +58,7 @@ Qed. (* Why3 goal *) Lemma Div_unique : forall (x:Z) (y:Z) (q:Z), (0%Z < y)%Z -> ((((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q)). (((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q). intros x y q h1 (h2,h3). assert (h:(~(y=0))%Z) by omega. generalize (Mod_bound x y h); intro h0. ... ... @@ -82,8 +81,7 @@ Qed. (* Why3 goal *) 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). ((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. case Z_le_dec ; intros H. ... ... @@ -161,7 +159,7 @@ rewrite Z_div_same_full; auto with zarith. Qed. (* Why3 goal *) Lemma Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((mod1 0%Z y) = 0%Z). Lemma Mod_0 : forall (y:Z), ~ (y = 0%Z) -> ((mod1 0%Z y) = 0%Z). intros y Hy. unfold mod1, div. rewrite Zmod_0_l. ... ...
 ... ... @@ -128,13 +128,13 @@ Qed. (* Why3 goal *) Lemma Trans : forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> ((y <= z)%Z -> (x <= z)%Z). forall (x:Z) (y:Z) (z:Z), (x <= y)%Z -> (y <= z)%Z -> (x <= z)%Z. Proof. exact Zle_trans. Qed. (* Why3 goal *) Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> ((y <= x)%Z -> (x = y)). Lemma Antisymm : forall (x:Z) (y:Z), (x <= y)%Z -> (y <= x)%Z -> (x = y). Proof. exact Zle_antisym. Qed. ... ... @@ -167,7 +167,7 @@ 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). (x <= y)%Z -> (0%Z <= z)%Z -> ((x * z)%Z <= (y * z)%Z)%Z. Proof. exact Zmult_le_compat_r. Qed. ... ...
 ... ... @@ -22,7 +22,7 @@ Require int.Int. 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)). (~ (x <= y)%Z -> ((ZArith.BinInt.Z.min x y) = y)). Proof. intros x y. split ; intros H. ... ... @@ -38,7 +38,7 @@ Qed. 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)). (~ (x <= y)%Z -> ((ZArith.BinInt.Z.max x y) = x)). Proof. intros x y. split ; intros H. ... ...
 ... ... @@ -67,7 +67,7 @@ Qed. (* Why3 goal *) Lemma Numof_bounds : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z -> ((0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z). (a < b)%Z -> (0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z. Proof. intros p a b h1. unfold numof. ... ... @@ -125,8 +125,9 @@ Proof. Qed. (* Why3 goal *) Lemma Numof_left_no_add : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z -> ((~ ((p a) = true)) -> ((numof p a b) = (numof p (a + 1%Z)%Z b))). Lemma Numof_left_no_add : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z -> ~ ((p a) = true) -> ((numof p a b) = (numof p (a + 1%Z)%Z b)). Proof. intros p a b h1 h2. rewrite Numof_append with (b := (a+1)%Z) by omega. ... ... @@ -169,8 +170,8 @@ Qed. (* Why3 goal *) Lemma Full : forall (p:(Z -> bool)) (a:Z) (b:Z), (a <= b)%Z -> ((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ((p n) = true)) -> ((numof p a b) = (b - a)%Z)). (forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ((p n) = true)) -> ((numof p a b) = (b - a)%Z). Proof. intros p a b h1. pattern b. ... ... @@ -234,7 +235,7 @@ Qed. Lemma numof_strictly_increasing : forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z) (l:Z), ((i <= j)%Z /\ ((j <= k)%Z /\ (k < l)%Z)) -> (((p k) = true) -> ((numof p i j) < (numof p i l))%Z). ((p k) = true) -> ((numof p i j) < (numof p i l))%Z. Proof. intros p i j k l (h1,(h2,h3)) h4. rewrite (Numof_append p i j l) by omega. ... ... @@ -243,9 +244,11 @@ apply numof_pos with (k := k); auto with zarith. Qed. (* Why3 goal *) Lemma numof_change_any : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> (((p1 j) = true) -> ((p2 j) = true))) -> ((numof p1 a b) <= (numof p2 a b))%Z. Lemma numof_change_any : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) -> ((p2 j) = true)) -> ((numof p1 a b) <= (numof p2 a b))%Z. Proof. intros p1 p2 a b. case (Z_lt_le_dec a b); intro; [|rewrite Numof_empty, Numof_empty; omega]. ... ... @@ -265,10 +268,12 @@ Proof. Qed. (* Why3 goal *) Lemma numof_change_some : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z) (i:Z), ((a <= i)%Z /\ (i < b)%Z) -> ((forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> (((p1 j) = true) -> ((p2 j) = true))) -> ((~ ((p1 i) = true)) -> (((p2 i) = true) -> ((numof p1 a b) < (numof p2 a b))%Z))). Lemma numof_change_some : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z) (i:Z), ((a <= i)%Z /\ (i < b)%Z) -> (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) -> ((p2 j) = true)) -> ~ ((p1 i) = true) -> ((p2 i) = true) -> ((numof p1 a b) < (numof p2 a b))%Z. Proof. intros p1 p2 a b i (h1,h2) h3 h4 h5. generalize (Z_le_lt_eq_dec _ _ (numof_change_any p1 p2 a b h3)). ... ... @@ -293,7 +298,7 @@ Qed. Lemma numof_change_equiv : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> (((p1 j) = true) <-> ((p2 j) = true))) -> ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) <-> ((p2 j) = true)) -> ((numof p2 a b) = (numof p1 a b)). Proof. intros p1 p2 a b h1. ... ...
 ... ... @@ -32,7 +32,7 @@ Lemma nth_def : | Init.Datatypes.nil => ((nth n l) = Init.Datatypes.None) | (Init.Datatypes.cons x r) => ((n = 0%Z) -> ((nth n l) = (Init.Datatypes.Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) (~ (n = 0%Z) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. Proof. intros a a_WT n l. ... ...
 ... ... @@ -38,7 +38,7 @@ Lemma num_occ_def : | 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)) (~ (x = y) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z)) end. Proof. intros a a_WT x [|y r]. ... ...
 ... ... @@ -44,7 +44,7 @@ Qed. 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)). (permut l1 l2) -> (permut l2 l3) -> (permut l1 l3). Proof. intros a a_WT l1 l2 l3 h1 h2 x. now rewrite h1. ... ... @@ -119,7 +119,7 @@ Qed. 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)). (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. ... ...
 ... ... @@ -46,7 +46,7 @@ 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))). (~ (y = x) -> (((set f x v) y) = (f y))). Proof. intros a a_WT b b_WT f x v y. unfold set. ... ...
 ... ... @@ -233,12 +233,12 @@ Definition surjective (a:(Z -> Z)) (n:Z) : Prop := (* Why3 assumption *) Definition range (a:(Z -> Z)) (n:Z) : Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (a i))%Z /\ ((a i) < n)%Z). ((0%Z <= i)%Z /\ (i < n)%Z) -> (0%Z <= (a i))%Z /\ ((a i) < n)%Z. (* Why3 goal *) Lemma injective_surjective : forall (a:(Z -> Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). (injective a n) -> (range a n) -> (surjective a n). Proof. unfold injective, range, surjective. intros a n h1 h2. ... ...
 ... ... @@ -135,7 +135,7 @@ Qed. Lemma occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z -> a)) (l:Z) (u:Z), (l <= u)%Z -> ((0%Z <= (occ v m l u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z). (l <= u)%Z -> (0%Z <= (occ v m l u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z. Proof. intros a a_WT v m l u h1. cut (0 <= u - l)%Z. 2: omega. ... ...
 ... ... @@ -76,7 +76,7 @@ Qed. Lemma Euclid : forall (p:Z) (a:Z) (b:Z), ((number.Prime.prime p) /\ (number.Divisibility.divides p (a * b)%Z)) -> ((number.Divisibility.divides p a) \/ (number.Divisibility.divides p b)). (number.Divisibility.divides p a) \/ (number.Divisibility.divides p b). intros p a b (h1,h2). apply Znumtheory.prime_mult; auto. now rewrite <- Prime.prime_is_Zprime. ... ...
 ... ... @@ -24,7 +24,7 @@ Require number.Parity. (* Why3 assumption *) Definition divides (d:Z) (n:Z) : Prop := ((d = 0%Z) -> (n = 0%Z)) /\ ((~ (d = 0%Z)) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)). (~ (d = 0%Z) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)). *) ... ... @@ -100,7 +100,7 @@ Qed. (* Why3 goal *) Lemma divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b + c)%Z)). (divides a b) -> (divides a c) -> (divides a (b + c)%Z). Proof. exact Zdivide_plus_r. Qed. ... ... @@ -108,7 +108,7 @@ Qed. (* Why3 goal *) Lemma divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b - c)%Z)). (divides a b) -> (divides a c) -> (divides a (b - c)%Z). Proof. exact Zdivide_minus_l. Qed. ... ... @@ -142,7 +142,7 @@ Qed. (* Why3 goal *) Lemma divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)). forall (n:Z), (divides n 1%Z) -> (n = 1%Z) \/ (n = (-1%Z)%Z). Proof. exact Zdivide_1. Qed. ... ... @@ -150,14 +150,14 @@ Qed. (* Why3 goal *) Lemma divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). (divides a b) -> (divides b a) -> (a = b) \/ (a = (-b)%Z). Proof. exact Zdivide_antisym. Qed. (* Why3 goal *) Lemma divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides b c) -> (divides a c). Proof. exact Zdivide_trans. Qed. ... ... @@ -172,8 +172,9 @@ Qed. Import EuclideanDivision. (* Why3 goal *) Lemma mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((int.EuclideanDivision.mod1 a b) = 0%Z) -> (divides b a)). Lemma mod_divides_euclidean : forall (a:Z) (b:Z), ~ (b = 0%Z) -> ((int.EuclideanDivision.mod1 a b) = 0%Z) -> (divides b a). Proof. intros a b Zb H. exists (div a b). ... ... @@ -183,8 +184,9 @@ ring. Qed. (* Why3 goal *) Lemma divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z)). Lemma divides_mod_euclidean : forall (a:Z) (b:Z), ~ (b = 0%Z) -> (divides b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z). Proof. intros a b Zb H. assert (Zmod a b = Z0). ... ... @@ -200,7 +202,7 @@ Qed. (* Why3 goal *) Lemma mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((ZArith.BinInt.Z.rem a b) = 0%Z) -> (divides b a)). ~ (b = 0%Z) -> ((ZArith.BinInt.Z.rem a b) = 0%Z) -> (divides b a). Proof. intros a b Zb H. exists (Z.quot a b). ... ... @@ -211,7 +213,7 @@ Qed. (* Why3 goal *) Lemma divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((ZArith.BinInt.Z.rem a b) = 0%Z)). ~ (b = 0%Z) -> (divides b a) -> ((ZArith.BinInt.Z.rem a b) = 0%Z). Proof. intros a b Zb (q,H). rewrite H. ... ...
 ... ... @@ -48,9 +48,11 @@ apply Zgcd_is_gcd. Qed. (* Why3 goal *) Lemma gcd_def3 : forall (a:Z) (b:Z) (x:Z), (number.Divisibility.divides x a) -> ((number.Divisibility.divides x b) -> (number.Divisibility.divides x (gcd a b))). Lemma gcd_def3 : forall (a:Z) (b:Z) (x:Z), (number.Divisibility.divides x a) -> (number.Divisibility.divides x b) -> (number.Divisibility.divides x (gcd a b)). Proof. intros a b x. apply Zgcd_is_gcd. ... ... @@ -124,8 +126,9 @@ apply Zgcd_is_gcd. Qed. (* Why3 goal *) Lemma Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd b (ZArith.BinInt.Z.rem a b)) = (gcd a b)). Lemma Gcd_computer_mod : forall (a:Z) (b:Z), ~ (b = 0%Z) -> ((gcd b (ZArith.BinInt.Z.rem a b)) = (gcd a b)). Proof. intros a b _. rewrite (Zgcd_comm a b). ... ... @@ -138,7 +141,7 @@ Qed. (* Why3 goal *) Lemma Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd b (int.EuclideanDivision.mod1 a b)) = (gcd a b)). ~ (b = 0%Z) -> ((gcd b (int.EuclideanDivision.mod1 a b)) = (gcd a b)). Proof. intros a b Zb. rewrite (Zgcd_comm a b). ... ... @@ -149,8 +152,9 @@ ring. Qed. (* Why3 goal *) Lemma gcd_mult : forall (a:Z) (b:Z) (c:Z), (0%Z <= c)%Z -> ((gcd (c * a)%Z (c * b)%Z) = (c * (gcd a b))%Z). Lemma gcd_mult : forall (a:Z) (b:Z) (c:Z), (0%Z <= c)%Z -> ((gcd (c * a)%Z (c * b)%Z) = (c * (gcd a b))%Z). Proof. intros a b c H. apply Zis_gcd_gcd. ... ...
 ... ... @@ -164,7 +164,7 @@ Qed. (* Why3 goal *) Lemma even_prime : forall (p:Z), (prime p) -> ((number.Parity.even p) -> (p = 2%Z)). forall (p:Z), (prime p) -> (number.Parity.even p) -> (p = 2%Z). Proof. intros p Pp (q,Hq). generalize (proj2 Pp q). ... ... @@ -183,7 +183,7 @@ Qed. (* Why3 goal *) Lemma odd_prime : forall (p:Z), (prime p) -> ((3%Z <= p)%Z -> (number.Parity.odd p)). forall (p:Z), (prime p) -> (3%Z <= p)%Z -> (number.Parity.odd p). Proof. intros p Pp Hp. apply <- Divisibility.odd_divides. ... ...
 ... ... @@ -25,7 +25,7 @@ Import Rbasic_fun. 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)). (~ (0%R <= x)%R -> ((Reals.Rbasic_fun.Rabs x) = (-x)%R)). split ; intros H. apply Rabs_right. now apply Rle_ge. ... ...
 ... ... @@ -24,7 +24,7 @@ Require Import Rbasic_fun. Lemma min_def : forall (x:R) (y:R), ((x <= y)%R -> ((Reals.Rbasic_fun.Rmin x y) = x)) /\ ((~ (x <= y)%R) -> ((Reals.Rbasic_fun.Rmin x y) = y)). (~ (x <= y)%R -> ((Reals.Rbasic_fun.Rmin x y) = y)). Proof. intros x y. split ; intros H. ... ... @@ -40,7 +40,7 @@ Qed. Lemma max_def : forall (x:R) (y:R), ((x <= y)%R -> ((Reals.Rbasic_fun.Rmax x y) = y)) /\ ((~ (x <= y)%R) -> ((Reals.Rbasic_fun.Rmax x y) = x)). (~ (x <= y)%R -> ((Reals.Rbasic_fun.Rmax x y) = x)). Proof. intros x y. split ; intros H. ... ...
 ... ... @@ -47,7 +47,8 @@ Qed. (* Why3 goal *) Lemma Power_s : forall (x:R) (n:Z), (0%Z <= n)%Z -> ((Reals.Rfunctions.powerRZ x (n + 1%Z)%Z) = (x * (Reals.Rfunctions.powerRZ x n))%R). ((Reals.Rfunctions.powerRZ x (n + 1%Z)%Z) = (x * (Reals.Rfunctions.powerRZ x n))%R). Proof. intros x n h1. rewrite 2!power_is_exponentiation by auto with zarith. ... ... @@ -56,7 +57,8 @@ Qed. (* Why3 goal *) Lemma Power_s_alt : forall (x:R) (n:Z), (0%Z < n)%Z -> ((Reals.Rfunctions.powerRZ x n) = (x * (Reals.Rfunctions.powerRZ x (n - 1%Z)%Z))%R). ((Reals.Rfunctions.powerRZ x n) = (x * (Reals.Rfunctions.powerRZ x (n - 1%Z)%Z))%R). intros x n h1. rewrite <- Power_s. f_equal; omega. ... ... @@ -70,8 +72,9 @@ exact Rmult_1_r. Qed. (* Why3 goal *) Lemma Power_sum : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z -> ((Reals.Rfunctions.powerRZ x (n + m)%Z) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ x m))%R)). Lemma Power_sum : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z -> ((Reals.Rfunctions.powerRZ x (n + m)%Z) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ x m))%R). Proof. intros x n m h1 h2. rewrite 3!power_is_exponentiation by auto with zarith. ... ... @@ -79,8 +82,9 @@ apply Power_sum ; auto with real. Qed. (* Why3 goal *) Lemma Power_mult : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z -> ((Reals.Rfunctions.powerRZ x (n * m)%Z) = (Reals.Rfunctions.powerRZ (Reals.Rfunctions.powerRZ x n) m))). Lemma Power_mult : forall (x:R) (n:Z) (m:Z), (0%Z <= n)%Z -> (0%Z <= m)%Z -> ((Reals.Rfunctions.powerRZ x (n * m)%Z) = (Reals.Rfunctions.powerRZ (Reals.Rfunctions.powerRZ x n) m)). Proof. intros x n m h1 h2. rewrite 3!power_is_exponentiation by auto with zarith. ... ... @@ -90,7 +94,8 @@ Qed. (* Why3 goal *) Lemma Power_comm1 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> forall (n:Z), (0%Z <= n)%Z -> (((Reals.Rfunctions.powerRZ x n) * y)%R = (y * (Reals.Rfunctions.powerRZ x n))%R). (((Reals.Rfunctions.powerRZ x n) * y)%R = (y * (Reals.Rfunctions.powerRZ x n))%R). intros x y h1 n h2. apply Rmult_comm. Qed. ... ... @@ -98,7 +103,8 @@ Qed. (* Why3 goal *) Lemma Power_comm2 : forall (x:R) (y:R), ((x * y)%R = (y * x)%R) -> forall (n:Z), (0%Z <= n)%Z -> ((Reals.Rfunctions.powerRZ (x * y)%R n) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ y n))%R). ((Reals.Rfunctions.powerRZ (x * y)%R n) = ((Reals.Rfunctions.powerRZ x n) * (Reals.Rfunctions.powerRZ y n))%R). Proof. intros x y h1 n h2. rewrite 3!power_is_exponentiation by auto with zarith. ... ...
 ... ... @@ -27,7 +27,8 @@ Import Rpower. (* Why3 goal *) Lemma Pow_def : forall (x:R) (y:R), (0%R < x)%R -> ((Reals.Rpower.Rpower x y) = (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)). ((Reals.Rpower.Rpower x y) = (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)). Proof.