From e4746a0b32f759c43414082be2824b46a70fb67e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 5 Mar 2014 17:59:41 +0100 Subject: [PATCH] Fix Coq proofs broken by the qualified-name changes. --- .../euler001_DivModHints_mod_div_unique_1.v | 27 +++++------ .../euler001_DivModHints_mod_succ_1_1.v | 22 ++++----- .../euler001_DivModHints_mod_succ_2_1.v | 22 +++++---- ...WP_EuclideanAlgorithm_WP_parameter_gcd_1.v | 12 +++-- ...rimeNumbers_WP_parameter_prime_numbers_4.v | 36 +++++++++----- ...rimeNumbers_WP_parameter_prime_numbers_7.v | 28 ++++++----- ..._CauchySchwarzInequality_CauchySchwarz_1.v | 27 ++++++----- ...ty_CauchySchwarzInequality_sqr_le_sqrt_1.v | 25 +++++----- ..._CauchySchwarzInequality_CauchySchwarz_1.v | 48 ++++++++++--------- ...wer_M_WP_parameter_fast_exp_imperative_1.v | 17 ++++--- ..._WP_M_WP_parameter_fast_exp_imperative_3.v | 25 +++++----- 11 files changed, 160 insertions(+), 129 deletions(-) diff --git a/examples/euler001/euler001_DivModHints_mod_div_unique_1.v b/examples/euler001/euler001_DivModHints_mod_div_unique_1.v index 35f7cbb57..31cf762f3 100644 --- a/examples/euler001/euler001_DivModHints_mod_div_unique_1.v +++ b/examples/euler001/euler001_DivModHints_mod_div_unique_1.v @@ -1,26 +1,23 @@ -(* 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))). + ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ + (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 *) - diff --git a/examples/euler001/euler001_DivModHints_mod_succ_1_1.v b/examples/euler001/euler001_DivModHints_mod_succ_1_1.v index d106a0fbc..a22ab0970 100644 --- a/examples/euler001/euler001_DivModHints_mod_succ_1_1.v +++ b/examples/euler001/euler001_DivModHints_mod_succ_1_1.v @@ -1,7 +1,6 @@ (* 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. - diff --git a/examples/euler001/euler001_DivModHints_mod_succ_2_1.v b/examples/euler001/euler001_DivModHints_mod_succ_2_1.v index fef7f89cd..319d4278f 100644 --- a/examples/euler001/euler001_DivModHints_mod_succ_2_1.v +++ b/examples/euler001/euler001_DivModHints_mod_succ_2_1.v @@ -1,7 +1,6 @@ (* 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. - diff --git a/examples/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v b/examples/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v index a85c792ce..2a50bb193 100644 --- a/examples/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v +++ b/examples/gcd/gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v @@ -1,7 +1,6 @@ (* 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. diff --git a/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v b/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v index d61df5b45..5d461c442 100644 --- a/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v +++ b/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v @@ -1,7 +1,6 @@ (* 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. diff --git a/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_7.v b/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_7.v index 5e385a7d2..53984732f 100644 --- a/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_7.v +++ b/examples/knuth_prime_numbers/knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_7.v @@ -1,7 +1,6 @@ (* 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. diff --git a/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v b/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v index b1b7f735d..3ff058b92 100644 --- a/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v +++ b/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v @@ -1,7 +1,7 @@ -(* 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. - diff --git a/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v b/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v index 64e278b01..7cc5df6df 100644 --- a/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v +++ b/examples/logic/lagrange_inequality/lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v @@ -1,7 +1,7 @@ -(* 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. - diff --git a/examples/logic/triangle_inequality/triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v b/examples/logic/triangle_inequality/triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v index 02e3fa55c..6538ea295 100644 --- a/examples/logic/triangle_inequality/triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v +++ b/examples/logic/triangle_inequality/triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v @@ -1,7 +1,7 @@ -(* 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. (* 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), ((0%R <= x)%R /\ - ((0%R <= (Rsqr x))%R /\ ((Rsqr x) <= y)%R)) -> (x <= (sqrt y))%R. + ((0%R <= (Reals.RIneq.Rsqr x))%R /\ ((Reals.RIneq.Rsqr x) <= y)%R)) -> + (x <= (Reals.R_sqrt.sqrt y))%R. + +Import R_sqrt. (* 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. @@ -87,4 +92,3 @@ apply norm2_pos. apply norm2_pos. Qed. - diff --git a/examples/power/power_M_WP_parameter_fast_exp_imperative_1.v b/examples/power/power_M_WP_parameter_fast_exp_imperative_1.v index b3016b603..89b7bb12c 100644 --- a/examples/power/power_M_WP_parameter_fast_exp_imperative_1.v +++ b/examples/power/power_M_WP_parameter_fast_exp_imperative_1.v @@ -1,7 +1,6 @@ (* 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. @@ -11,6 +10,10 @@ Require int.Power. (* Why3 assumption *) Definition unit := unit. +Axiom qtmark : Type. +Parameter qtmark_WhyType : WhyType qtmark. +Existing Instance qtmark_WhyType. + (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. @@ -19,7 +22,7 @@ Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) -Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a := +Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a := match v with | (mk_ref x) => x end. @@ -31,9 +34,10 @@ Import Power. Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z), (0%Z <= n)%Z -> forall (e:Z) (p:Z) (r:Z), ((0%Z <= e)%Z /\ ((r * (int.Power.power p e))%Z = (int.Power.power x n))) -> ((0%Z < e)%Z -> - (((ZOmod e 2%Z) = 1%Z) -> forall (r1:Z), (r1 = (r * p)%Z) -> forall (p1:Z), - (p1 = (p * p)%Z) -> forall (e1:Z), (e1 = (ZOdiv e 2%Z)) -> - ((r1 * (int.Power.power p1 e1))%Z = (int.Power.power x n)))). + (((ZArith.BinInt.Z.rem e 2%Z) = 1%Z) -> forall (r1:Z), (r1 = (r * p)%Z) -> + forall (p1:Z), (p1 = (p * p)%Z) -> forall (e1:Z), + (e1 = (ZArith.BinInt.Z.quot e 2%Z)) -> ((r1 * (int.Power.power p1 + e1))%Z = (int.Power.power x n)))). (* Why3 intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8. *) intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8. subst. @@ -46,11 +50,10 @@ intros. rewrite <- h3; clear h3. rewrite H0 at 2. clear H0. rewrite Power_sum by omega. -replace (2 * (ZOdiv e 2))%Z with (ZOdiv e 2 + ZOdiv e 2)%Z by ring. +replace (2 * (Z.quot e 2))%Z with (Z.quot e 2 + Z.quot e 2)%Z by ring. rewrite Power_sum by apply H. rewrite Power_mult2 by apply H. rewrite Power_1. ring. Qed. - diff --git a/examples/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v b/examples/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v index 9afd54195..4a1a11bfd 100644 --- a/examples/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v +++ b/examples/power/power_WP_M_WP_parameter_fast_exp_imperative_3.v @@ -1,7 +1,6 @@ (* 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. @@ -11,6 +10,10 @@ Require int.Power. (* Why3 assumption *) Definition unit := unit. +Axiom qtmark : Type. +Parameter qtmark_WhyType : WhyType qtmark. +Existing Instance qtmark_WhyType. + (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. @@ -19,36 +22,34 @@ Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) -Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a := +Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a := match v with | (mk_ref x) => x end. -Import Power. +Import Power Zquot. Open Scope Z_scope. (* Why3 goal *) Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z), (0%Z <= n)%Z -> forall (e:Z) (p:Z) (r:Z), ((0%Z <= e)%Z /\ ((r * (int.Power.power p e))%Z = (int.Power.power x n))) -> ((0%Z < e)%Z -> - ((~ ((ZOmod e 2%Z) = 1%Z)) -> forall (p1:Z), (p1 = (p * p)%Z) -> - forall (e1:Z), (e1 = (ZOdiv e 2%Z)) -> ((r * (int.Power.power p1 - e1))%Z = (int.Power.power x n)))). + ((~ ((ZArith.BinInt.Z.rem e 2%Z) = 1%Z)) -> forall (p1:Z), + (p1 = (p * p)%Z) -> forall (e1:Z), (e1 = (ZArith.BinInt.Z.quot e 2%Z)) -> + ((r * (int.Power.power p1 e1))%Z = (int.Power.power x n)))). (* Why3 intros x n h1 e p r (h2,h3) h4 h5 p1 h6 e1 h7. *) -(* YOU MAY EDIT THE PROOF BELOW *) intros x n Hn e0 p0 r0 (He0,Hind). intros He0' Hmod p1 Hp e1 He. rewrite <- Hind. apply f_equal. subst. -assert (h: (e0 = ZOdiv e0 2 + ZOdiv e0 2)). -assert (ZOmod e0 2 = 0). -generalize (ZOmod_lt_pos e0 2). +assert (h: (e0 = Z.quot e0 2 + Z.quot e0 2)). +assert (Z.rem e0 2 = 0). +generalize (Zrem_lt_pos e0 2). unfold Zabs; omega. -rewrite (ZO_div_mod_eq e0 2) at 1; omega. +rewrite (Z_quot_rem_eq e0 2) at 1; omega. rewrite Power_mult2; auto with zarith. rewrite h at 3. rewrite Power_sum; omega. Qed. - -- GitLab