Commit e4746a0b by Guillaume Melquiond

Fix Coq proofs broken by the qualified-name changes.

parent a620a3e3
 (* This file is generated by Why3's Coq driver *) (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. (* Why3 goal *) Theorem mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\ ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))). (r < y)%Z)))) -> ((q = (ZArith.BinInt.Z.quot x y)) /\ (r = (ZArith.BinInt.Z.rem x y))). (* Why3 intros x y q r (h1,(h2,(h3,(h4,h5)))). *) (* YOU MAY EDIT THE PROOF BELOW *) intros x y q r (H1,(H2,(H3,(H4,H5)))). apply ZOdiv_mod_unique_full. apply Zquot.Zquot_mod_unique_full. 2: rewrite H3; ring. red. left. rewrite Zabs_eq; auto with zarith. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. ... ... @@ -9,28 +8,29 @@ Require int.ComputerDivision. Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\ ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))). (r < y)%Z)))) -> ((q = (ZArith.BinInt.Z.quot x y)) /\ (r = (ZArith.BinInt.Z.rem x y))). Import Zquot. Open Scope Z_scope. (* Why3 goal *) Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) -> ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)). ((~ ((ZArith.BinInt.Z.rem (x + 1%Z)%Z y) = 0%Z)) -> ((ZArith.BinInt.Z.rem (x + 1%Z)%Z y) = ((ZArith.BinInt.Z.rem x y) + 1%Z)%Z)). (* Why3 intros x y (h1,h2) h3. *) intros x y (Hx,Hy) H. assert (h: y>0) by omega. generalize (ZO_div_mod_eq x y); intro h1. generalize (ZO_div_mod_eq (x+1) y); intro h2. assert (h3:x = y * (ZOdiv (x + 1) y) + (ZOmod (x + 1) y - 1)) by omega. generalize (mod_div_unique x y (ZOdiv (x + 1) y) (ZOmod (x + 1) y - 1)). generalize (Z_quot_rem_eq x y); intro h1. generalize (Z_quot_rem_eq (x+1) y); intro h2. assert (h3:x = y * (Z.quot (x + 1) y) + (Z.rem (x + 1) y - 1)) by omega. generalize (mod_div_unique x y (Z.quot (x + 1) y) (Z.rem (x + 1) y - 1)). intuition. destruct H1 ; auto with zarith. rewrite h3 at 1. ring. assert (0 <= ZOmod (x + 1) y < y). apply Zquot.Zrem_lt_pos_pos; omega. assert (0 <= Z.rem (x + 1) y < y). apply Zrem_lt_pos_pos; omega. omega. Qed.
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. ... ... @@ -9,27 +8,30 @@ Require int.ComputerDivision. Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\ ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))). (r < y)%Z)))) -> ((q = (ZArith.BinInt.Z.quot x y)) /\ (r = (ZArith.BinInt.Z.rem x y))). Axiom mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) -> ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)). ((~ ((ZArith.BinInt.Z.rem (x + 1%Z)%Z y) = 0%Z)) -> ((ZArith.BinInt.Z.rem (x + 1%Z)%Z y) = ((ZArith.BinInt.Z.rem x y) + 1%Z)%Z)). Import Zquot. (* Why3 goal *) Theorem mod_succ_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> (((ZOmod (x + 1%Z)%Z y) = 0%Z) -> ((ZOmod x y) = (y - 1%Z)%Z)). (((ZArith.BinInt.Z.rem (x + 1%Z)%Z y) = 0%Z) -> ((ZArith.BinInt.Z.rem x y) = (y - 1%Z)%Z)). (* Why3 intros x y (h1,h2) h3. *) intros x y (Hx,Hy) H. generalize (ZO_div_mod_eq x y); intro h1. generalize (ZO_div_mod_eq (x+1) y); intro h2. assert (h3: (x = y * (ZOdiv (x + 1) y - 1) + (ZOmod (x + 1) y + y - 1))%Z). generalize (Z_quot_rem_eq x y); intro h1. generalize (Z_quot_rem_eq (x+1) y); intro h2. assert (h3: (x = y * (Z.quot (x + 1) y - 1) + (Z.rem (x + 1) y + y - 1))%Z). ring_simplify; omega. rewrite H in h3. generalize (mod_div_unique x y (ZOdiv (x + 1) y - 1) (0 + y - 1)). generalize (mod_div_unique x y (Z.quot (x + 1) y - 1) (0 + y - 1)). intuition. destruct H1; auto with zarith. rewrite h3 at 1. ring. Qed.
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. ... ... @@ -14,18 +13,23 @@ Require number.Gcd. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* Why3 goal *) Theorem WP_parameter_euclid : forall (u:Z) (v:Z), ((0%Z <= u)%Z /\ (0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> let o := (ZOmod u v) in (0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> let o := (ZArith.BinInt.Z.rem u v) in (((0%Z <= v)%Z /\ (0%Z <= o)%Z) -> ((number.Gcd.gcd v o) = (number.Gcd.gcd u v)))). (* Why3 intros u v (h1,h2) h3 o (h4,h5). *) Proof. intuition. symmetry. rewrite Gcd.Comm. rewrite Gcd.gcd_euclid with (q:=(ZOdiv u v)). rewrite Gcd.gcd_euclid with (q := Z.quot u v). apply f_equal. rewrite (ZO_div_mod_eq u v) at 1. rewrite (Zquot.Z_quot_rem_eq u v) at 1. ring. Qed.
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. ... ... @@ -15,6 +14,10 @@ Require map.Map. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* Why3 assumption *) Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. ... ... @@ -69,7 +72,7 @@ Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z) (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) := (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))). (mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))). (* Why3 assumption *) Definition no_prime_in (l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\ ... ... @@ -100,11 +103,13 @@ apply Zge_le in H'. now apply Zmult_le_compat. Qed. Import Zquot. (* Why3 goal *) Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> ((0%Z <= m)%Z -> ((0%Z <= m)%Z -> (((0%Z <= 0%Z)%Z /\ (0%Z < m)%Z) -> forall (p:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\ (p = (map.Map.set (map.Map.const 0%Z:(@map.Map.map Z _ Z _)) 0%Z 2%Z))) -> (p = (map.Map.set (map.Map.const 0%Z: (@map.Map.map Z _ Z _)) 0%Z 2%Z))) -> (((0%Z <= 1%Z)%Z /\ (1%Z < m)%Z) -> forall (p1:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\ (p1 = (map.Map.set p 1%Z 3%Z))) -> let o := (m - 1%Z)%Z in ((2%Z <= o)%Z -> forall (n:Z) (p2:(@map.Map.map Z _ Z _)), forall (j:Z), ... ... @@ -118,10 +123,15 @@ Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> ((number.Parity.odd n1) /\ ((no_prime_in (map.Map.get p3 (j - 1%Z)%Z) n1) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) -> ~ (number.Divisibility.divides (map.Map.get p3 i) n1))))))) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((ZOmod n1 (map.Map.get p3 k)) = 0%Z)) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((map.Map.get p3 k) < (ZOdiv n1 (map.Map.get p3 (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((ZArith.BinInt.Z.rem n1 (map.Map.get p3 k)) = 0%Z)) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((map.Map.get p3 k) < (ZArith.BinInt.Z.quot n1 (map.Map.get p3 k)))%Z) -> (number.Prime.prime n1)))))))))))). (* Why3 intros m h1 h2 h3 (h4,h5) p (h6,h7) (h8,h9) p1 (h10,h11) o h12 n p2 j (h13,h14) (h15,((h16,h17),(h18,h19))) k n1 p3 (h20,((h21,h22),(h23,((h24,h25),(h26,(h27,h28)))))) (h29,h30) h31 (h32,h33) (h34,h35) h36. *) intros m h1 h2 h3 (h4,h5) p (h6,h7) (h8,h9) p1 (h10,h11) o h12 n p2 j (h13,h14) (h15,((h16,h17),(h18,h19))) k n1 p3 (h20,((h21,h22),(h23,((h24,h25),(h26,(h27,h28)))))) (h29,h30) h31 ... ... @@ -133,21 +143,21 @@ rewrite <- p0. apply sorted; omega. apply Prime.small_divisors; auto. omega. intros. generalize (ZO_div_mod_eq n1 (Map.get p3 k)). intro div. generalize (Z_quot_rem_eq n1 (Map.get p3 k)). intro div. assert (ne1: (0 <= n1 /\ Map.get p3 k <> 0)%Z) by omega. assert (mod1: (0 <= ZOmod n1 (Map.get p3 k))%Z). assert (mod1: (0 <= Z.rem n1 (Map.get p3 k))%Z). destruct (not_Zeq_inf _ _ (proj2 ne1)) as [Zm|Zm]. now apply ZOmod_lt_pos_neg. now apply ZOmod_lt_pos_pos. assert (mod2: (ZOmod n1 (Map.get p3 k) < Map.get p3 k)%Z). apply ZOmod_lt_pos_pos ; omega. now apply Zrem_lt_pos_neg. now apply Zrem_lt_pos_pos. assert (mod2: (Z.rem n1 (Map.get p3 k) < Map.get p3 k)%Z). apply Zrem_lt_pos_pos ; omega. assert (d <= Map.get p3 k)%Z. assert (d < Map.get p3 k+1)%Z. 2: omega. apply Zle_sqrt; try omega. assert (2 < Map.get p3 k)%Z. rewrite <- p0. apply sorted; omega. apply Zle_lt_trans with n1; try omega. assert (Map.get p3 k * (ZOdiv n1 (Map.get p3 k)) <= Map.get p3 k * Map.get p3 k)%Z. assert (Map.get p3 k * (Z.quot n1 (Map.get p3 k)) <= Map.get p3 k * Map.get p3 k)%Z. apply Zmult_le_compat_l; try omega. replace ((Map.get p3 k + 1) * (Map.get p3 k + 1))%Z with (Map.get p3 k * Map.get p3 k + 2 * Map.get p3 k + 1)%Z by ring. omega. ... ...
 (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. ... ... @@ -15,6 +14,10 @@ Require map.Map. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* Why3 assumption *) Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. ... ... @@ -69,7 +72,7 @@ Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z) (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) := (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))). (mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))). (* Why3 assumption *) Definition no_prime_in (l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\ ... ... @@ -91,11 +94,13 @@ Axiom exists_prime : forall (p:(@array Z _)) (u:Z), (1%Z <= u)%Z -> Axiom Bertrand_postulate : forall (p:Z), (number.Prime.prime p) -> ~ (no_prime_in p (2%Z * p)%Z). Import Zquot. (* Why3 goal *) Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> ((0%Z <= m)%Z -> ((0%Z <= m)%Z -> (((0%Z <= 0%Z)%Z /\ (0%Z < m)%Z) -> forall (p:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\ (p = (map.Map.set (map.Map.const 0%Z:(@map.Map.map Z _ Z _)) 0%Z 2%Z))) -> (p = (map.Map.set (map.Map.const 0%Z: (@map.Map.map Z _ Z _)) 0%Z 2%Z))) -> (((0%Z <= 1%Z)%Z /\ (1%Z < m)%Z) -> forall (p1:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\ (p1 = (map.Map.set p 1%Z 3%Z))) -> let o := (m - 1%Z)%Z in ((2%Z <= o)%Z -> forall (n:Z) (p2:(@map.Map.map Z _ Z _)), forall (j:Z), ... ... @@ -109,9 +114,10 @@ Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> ((number.Parity.odd n1) /\ ((no_prime_in (map.Map.get p3 (j - 1%Z)%Z) n1) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) -> ~ (number.Divisibility.divides (map.Map.get p3 i) n1))))))) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((ZOmod n1 (map.Map.get p3 k)) = 0%Z)) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((map.Map.get p3 k) < (ZOdiv n1 (map.Map.get p3 k)))%Z -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((ZArith.BinInt.Z.rem n1 (map.Map.get p3 k)) = 0%Z)) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> (((map.Map.get p3 k) < (ZArith.BinInt.Z.quot n1 (map.Map.get p3 k)))%Z -> ((k + 1%Z)%Z < j)%Z))))))))))). (* Why3 intros m h1 h2 h3 (h4,h5) p (h6,h7) (h8,h9) p1 (h10,h11) o h12 n p2 j (h13,h14) (h15,((h16,h17),(h18,h19))) k n1 p3 ... ... @@ -127,14 +133,14 @@ subst k. assert (2 < Map.get p3 (j-1))%Z. red in h23. destruct h23 as (hh1, (hh2, _)). rewrite <- hh1. apply hh2; omega. generalize (ZO_div_mod_eq n1 (Map.get p3 (j-1))%Z). intro div. generalize (Z_quot_rem_eq n1 (Map.get p3 (j-1))%Z). intro div. assert (ne1: (0 <= n1 /\ Map.get p3 (j-1) <> 0)%Z) by omega. assert (mod_: (0 <= ZOmod n1 (Map.get p3 (j-1)))%Z). assert (mod_: (0 <= Z.rem n1 (Map.get p3 (j-1)))%Z). destruct (not_Zeq_inf _ _ (proj2 ne1)) as [Zm|Zm]. now apply ZOmod_lt_pos_neg. now apply ZOmod_lt_pos_pos. now apply Zrem_lt_pos_neg. now apply Zrem_lt_pos_pos. assert (n1 > Map.get p3 (j - 1) * Map.get p3 (j-1))%Z. assert (Map.get p3 (j - 1) * (ZOdiv n1 (Map.get p3 (j - 1))) > Map.get p3 (j - 1) * Map.get p3 (j-1))%Z. assert (Map.get p3 (j - 1) * (Z.quot n1 (Map.get p3 (j - 1))) > Map.get p3 (j - 1) * Map.get p3 (j-1))%Z. apply Zmult_gt_compat_l. omega. apply Zlt_gt. ... ...
 (* This file is generated by Why3's Coq driver *) (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import R_sqrt. Require Reals.R_sqrt. Require BuiltIn. Require real.Real. Require real.Square. ... ... @@ -11,24 +11,26 @@ Definition dot (x1:R) (x2:R) (y1:R) (y2:R): R := ((x1 * y1)%R + (x2 * y2)%R)%R. (* Why3 assumption *) Definition norm2 (x1:R) (x2:R): R := ((Rsqr x1) + (Rsqr x2))%R. Definition norm2 (x1:R) (x2:R): R := ((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R. Axiom norm2_pos : forall (x1:R) (x2:R), (0%R <= (norm2 x1 x2))%R. Axiom Lagrange : forall (a1:R) (a2:R) (b1:R) (b2:R), (((norm2 a1 a2) * (norm2 b1 b2))%R = ((Rsqr (dot a1 a2 b1 b2)) + (Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R). a2) * (norm2 b1 b2))%R = ((Reals.RIneq.Rsqr (dot a1 a2 b1 b2)) + (Reals.RIneq.Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R). Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. (* Why3 assumption *) Definition norm (x1:R) (x2:R): R := (sqrt (norm2 x1 x2)). Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)). Axiom norm_pos : forall (x1:R) (x2:R), (0%R <= (norm x1 x2))%R. Axiom sqr_le_sqrt : forall (x:R) (y:R), ((Rsqr x) <= y)%R -> (x <= (sqrt y))%R. Axiom sqr_le_sqrt : forall (x:R) (y:R), ((Reals.RIneq.Rsqr x) <= y)%R -> (x <= (Reals.R_sqrt.sqrt y))%R. Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. ... ... @@ -36,14 +38,13 @@ Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. (* Why3 goal *) Theorem CauchySchwarz : forall (x1:R) (x2:R) (y1:R) (y2:R), ((dot x1 x2 y1 y2) <= ((norm x1 x2) * (norm y1 y2))%R)%R. (* intros x1 x2 y1 y2. *) (* Why3 intros x1 x2 y1 y2. *) intros x1 x2 y1 y2. unfold norm. rewrite <- sqrt_mult. rewrite <- R_sqrt.sqrt_mult. apply sqr_le_sqrt. ae. ae. ae. Qed.
 (* This file is generated by Why3's Coq driver *) (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import R_sqrt. Require Reals.R_sqrt. Require BuiltIn. Require real.Real. Require real.Square. ... ... @@ -11,30 +11,34 @@ Definition dot (x1:R) (x2:R) (y1:R) (y2:R): R := ((x1 * y1)%R + (x2 * y2)%R)%R. (* Why3 assumption *) Definition norm2 (x1:R) (x2:R): R := ((Rsqr x1) + (Rsqr x2))%R. Definition norm2 (x1:R) (x2:R): R := ((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R. Axiom norm2_pos : forall (x1:R) (x2:R), (0%R <= (norm2 x1 x2))%R. Axiom Lagrange : forall (a1:R) (a2:R) (b1:R) (b2:R), (((norm2 a1 a2) * (norm2 b1 b2))%R = ((Rsqr (dot a1 a2 b1 b2)) + (Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R). a2) * (norm2 b1 b2))%R = ((Reals.RIneq.Rsqr (dot a1 a2 b1 b2)) + (Reals.RIneq.Rsqr ((a1 * b2)%R - (a2 * b1)%R)%R))%R). Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. (* Why3 assumption *) Definition norm (x1:R) (x2:R): R := (sqrt (norm2 x1 x2)). Definition norm (x1:R) (x2:R): R := (Reals.R_sqrt.sqrt (norm2 x1 x2)). Axiom norm_pos : forall (x1:R) (x2:R), (0%R <= (norm x1 x2))%R. Require Import Why3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. Import R_sqrt. Open Scope R_scope. (* Why3 goal *) Theorem sqr_le_sqrt : forall (x:R) (y:R), ((Rsqr x) <= y)%R -> (x <= (sqrt y))%R. Theorem sqr_le_sqrt : forall (x:R) (y:R), ((Reals.RIneq.Rsqr x) <= y)%R -> (x <= (Reals.R_sqrt.sqrt y))%R. (* Why3 intros x y h1. *) intros x y h1. assert (0 <= Rsqr x) by ae. assert (0 <= y) by ae. ... ... @@ -50,4 +54,3 @@ ae. ae. Qed.
 (* This file is generated by Why3's Coq driver *) (* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import R_sqrt. Require Reals.R_sqrt. Require BuiltIn. Require real.Real. Require real.Square. ... ... @@ -11,14 +11,15 @@ Definition dot (x1:R) (x2:R) (y1:R) (y2:R): R := ((x1 * y1)%R + (x2 * y2)%R)%R. (* Why3 assumption *) Definition norm2 (x1:R) (x2:R): R := ((Rsqr x1) + (Rsqr x2))%R. Definition norm2 (x1:R) (x2:R): R := ((Reals.RIneq.Rsqr x1) + (Reals.RIneq.Rsqr x2))%R. Axiom norm2_pos : forall (x1:R) (x2:R), (0%R <= (norm2 x1 x2))%R. (* Why3 assumption *) Definition p (x1:R) (x2:R) (y1:R) (y2:R) (t:R): R := (((norm2 x1 x2) + ((2%R * t)%R * (dot x1 x2 y1 y2))%R)%R + ((Rsqr t) * (norm2 y1 y2))%R)%R. x2) + ((2%R * t)%R * (dot x1 x2 y1 y2))%R)%R + ((Reals.RIneq.Rsqr t) * (norm2 y1 y2))%R)%R. Axiom p_expr : forall (x1:R) (x2:R) (y1:R) (y2:R) (t:R), ((p x1 x2 y1 y2 t) = (norm2 (x1 + (t * y1)%R)%R (x2 + (t * y2)%R)%R)). ... ... @@ -27,47 +28,51 @@ Axiom p_pos : forall (x1:R) (x2:R) (y1:R) (y2:R) (t:R), (0%R <= (p x1 x2 y1 y2 t))%R. Axiom mul_div_simpl : forall (x:R) (y:R), (~ (y = 0%R)) -> (((Rdiv x y)%R * y)%R = x). (((x / y)%R * y)%R = x). Axiom p_val_part : forall (x1:R) (x2:R) (y1:R) (y2:R), (0%R < (norm2 y1 y2))%R -> ((p x1 x2 y1 y2 (-(Rdiv (dot x1 x2 y1 y2) (norm2 y1 y2))%R)%R) = ((norm2 x1 x2) - (Rdiv (Rsqr (dot x1 x2 y1 y2)) (norm2 y1 y2))%R)%R). y2))%R -> ((p x1 x2 y1 y2 (-((dot x1 x2 y1 y2) / (norm2 y1 y2))%R)%R) = ((norm2 x1 x2) - ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) / (norm2 y1 y2))%R)%R). Axiom p_val_part_pos : forall (x1:R) (x2:R) (y1:R) (y2:R), (0%R < (norm2 y1 y2))%R -> (0%R <= ((norm2 x1 x2) - (Rdiv (Rsqr (dot x1 x2 y1 y2)) (norm2 y1 y2))%R)%R)%R. y2))%R -> (0%R <= ((norm2 x1 x2) - ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) / (norm2 y1 y2))%R)%R)%R. Axiom p_val_part_pos_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), (0%R < (norm2 y1 y2))%R -> (0%R <= ((norm2 y1 y2) * (p x1 x2 y1 y2 (Rdiv (-(dot x1 x2 y1 y2))%R (norm2 y1 y2))%R))%R)%R. ((-(dot x1 x2 y1 y2))%R / (norm2 y1 y2))%R))%R)%R. Axiom CauchySchwarz_aux_non_null : forall (x1:R) (x2:R) (y1:R) (y2:R), (0%R < (norm2 y1 y2))%R -> ((Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. (0%R < (norm2 y1 y2))%R -> ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. Axiom norm_null : forall (y1:R) (y2:R), ((norm2 y1 y2) = 0%R) -> ((y1 = 0%R) \/ (y2 = 0%R)). Axiom CauchySchwarz_aux_null : forall (x1:R) (x2:R) (y1:R) (y2:R), ((norm2 y1 y2) = 0%R) -> ((Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. y2) = 0%R) -> ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R. Axiom CauchySchwarz_aux : forall (x1:R) (x2:R) (y1:R) (y2:R), ((Reals.RIneq.Rsqr (dot x1 x2 y1 y2)) <= ((norm2 x1 x2) * (norm2 y1 y2))%R)%R.