Commit 02f803a7 by Guillaume Melquiond

### Update Coq proofs for number theory examples and prove admitted lemma along the way.

parent 5c3182d2
 ... ... @@ -2,166 +2,46 @@ (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import Zdiv. Require Import ZOdiv. Require int.Int. Require int.Abs. Require int.EuclideanDivision. Require int.ComputerDivision. Require number.Parity. Require number.Divisibility. Require number.Gcd. (* Why3 assumption *) Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). Axiom divides_refl : forall (n:Z), (divides n n). Axiom divides_1_n : forall (n:Z), (divides 1%Z n). Axiom divides_0 : forall (n:Z), (divides n 0%Z). Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z). Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z). Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z). Axiom divides_oppl : forall (a:Z) (b:Z), (divides a b) -> (divides (-a)%Z b). Axiom divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a b). Axiom divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a b). Axiom divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b + c)%Z)). Axiom divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b - c)%Z)). Axiom divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (c * b)%Z). Axiom divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z). Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z). Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z). Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)). Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) -> ((Zabs a) <= (Zabs b))%Z). Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((Zmod a b) = 0%Z)). Axiom mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((ZOmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((ZOmod a b) = 0%Z)). Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z). Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z). Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n). Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n). Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n). Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z). Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z). Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z). Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z). Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z). Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z). Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a). Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a). Parameter gcd: Z -> Z -> Z. Axiom gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z. Axiom gcd_def1 : forall (a:Z) (b:Z), (divides (gcd a b) a). Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b). Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) -> (divides x (gcd a b))). Axiom gcd_unique : forall (a:Z) (b:Z) (d:Z), (0%Z <= d)%Z -> ((divides d a) -> ((divides d b) -> ((forall (x:Z), (divides x a) -> ((divides x b) -> (divides x d))) -> (d = (gcd a b))))). Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y z))). Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)). Axiom gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a). Axiom gcd_0_neg : forall (a:Z), (a < 0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z). Axiom gcd_opp : forall (a:Z) (b:Z), ((gcd a b) = (gcd (-a)%Z b)). Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a (b - (q * a)%Z)%Z)). Axiom Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b)) = (gcd a b)). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b)) = (gcd a b)). Axiom 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). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 goal *) Theorem WP_parameter_gcd : forall (u:Z), forall (v:Z), ((0%Z <= u)%Z /\ (0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> ((((0%Z <= v)%Z /\ ((ZOmod u v) < v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z)) -> ((gcd v (ZOmod u v)) = (gcd u v)))). (* YOU MAY EDIT THE PROOF BELOW *) ((ZOmod u v) < v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z)) -> ((number.Gcd.gcd v (ZOmod u v)) = (number.Gcd.gcd u v)))). Proof. intuition. symmetry. rewrite Comm. rewrite gcd_euclid with (q:=(ZOdiv u v)). rewrite Gcd.Comm. rewrite Gcd.gcd_euclid with (q:=(ZOdiv u v)). apply f_equal. rewrite (ZO_div_mod_eq u v) at 1. ring. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -3,182 +3,66 @@ Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Require int.Int. Require int.Abs. Require int.EuclideanDivision. Require int.ComputerDivision. Require number.Parity. Require number.Divisibility. Require number.Gcd. (* Why3 assumption *) Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). Axiom divides_refl : forall (n:Z), (divides n n). Axiom divides_1_n : forall (n:Z), (divides 1%Z n). Axiom divides_0 : forall (n:Z), (divides n 0%Z). Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z). Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z). Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z). Axiom divides_oppl : forall (a:Z) (b:Z), (divides a b) -> (divides (-a)%Z b). Axiom divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a b). Axiom divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a b). Axiom divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b + c)%Z)). Axiom divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b - c)%Z)). Axiom divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (c * b)%Z). Axiom divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z). Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z). Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z). Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)). Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) -> ((Zabs a) <= (Zabs b))%Z). Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((Zmod a b) = 0%Z)). Axiom mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((ZOmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((ZOmod a b) = 0%Z)). Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z). Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z). Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n). Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n). Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n). Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z). Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z). Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z). Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z). Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z). Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z). Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a). Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a). Parameter gcd: Z -> Z -> Z. Axiom gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z. Axiom gcd_def1 : forall (a:Z) (b:Z), (divides (gcd a b) a). Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b). Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) -> (divides x (gcd a b))). Axiom gcd_unique : forall (a:Z) (b:Z) (d:Z), (0%Z <= d)%Z -> ((divides d a) -> ((divides d b) -> ((forall (x:Z), (divides x a) -> ((divides x b) -> (divides x d))) -> (d = (gcd a b))))). Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y z))). Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)). Axiom gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a). Axiom gcd_0_neg : forall (a:Z), (a < 0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z). Axiom gcd_opp : forall (a:Z) (b:Z), ((gcd a b) = (gcd (-a)%Z b)). Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a (b - (q * a)%Z)%Z)). Axiom Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b)) = (gcd a b)). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b)) = (gcd a b)). Axiom 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). (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 (* Why3 assumption *) Definition contents (a:Type)(v:(ref a)): a := match v with | (mk_ref x) => x end. Implicit Arguments contents. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) (* Why3 goal *) Theorem WP_parameter_gcd : forall (x:Z), forall (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) -> forall (d:Z), forall (c:Z), forall (b:Z), forall (a:Z), forall (y1:Z), forall (x1:Z), ((0%Z <= x1)%Z /\ ((0%Z <= y1)%Z /\ (((gcd x1 y1) = (gcd x y)) /\ ((((a * x)%Z + (b * y)%Z)%Z = x1) /\ (((c * x)%Z + (d * y)%Z)%Z = y1))))) -> ((0%Z < y1)%Z -> forall (x2:Z), forall (y1:Z), forall (x1:Z), ((0%Z <= x1)%Z /\ ((0%Z <= y1)%Z /\ (((number.Gcd.gcd x1 y1) = (number.Gcd.gcd x y)) /\ ((((a * x)%Z + (b * y)%Z)%Z = x1) /\ (((c * x)%Z + (d * y)%Z)%Z = y1))))) -> ((0%Z < y1)%Z -> forall (x2:Z), (x2 = y1) -> forall (y2:Z), (y2 = (ZOmod x1 y1)) -> forall (a1:Z), (a1 = c) -> forall (b1:Z), (b1 = d) -> forall (c1:Z), (c1 = (a - (c * (ZOdiv x1 y1))%Z)%Z) -> forall (d1:Z), (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> ((gcd x2 y2) = (gcd x y))). (* YOU MAY EDIT THE PROOF BELOW *) (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> ((number.Gcd.gcd x2 y2) = (number.Gcd.gcd x y))). Proof. intuition. rewrite <- H4. subst x2 y2. symmetry. rewrite Comm. rewrite gcd_euclid with (q:=(ZOdiv x1 y1)). rewrite Gcd.Comm. rewrite Gcd.gcd_euclid with (q:=(ZOdiv x1 y1)). apply f_equal. rewrite (ZO_div_mod_eq x1 y1) at 1. ring. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -3,155 +3,60 @@ Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Require int.Int. Require int.Abs. Require int.EuclideanDivision. Require int.ComputerDivision. Require number.Parity. Require number.Divisibility. Require number.Prime. (* Why3 assumption *) Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. (* Why3 assumption *) Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop := | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1, y1) (x2, y2)) | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x, y2)). Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z). Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z). Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n). Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n). Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n). Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z). Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z). Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z). Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z). Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z). Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z). Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). Axiom divides_refl : forall (n:Z), (divides n n). Axiom divides_1_n : forall (n:Z), (divides 1%Z n). Axiom divides_0 : forall (n:Z), (divides n 0%Z). Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z). Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z). Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z). Axiom divides_oppl : forall (a:Z) (b:Z), (divides a b) -> (divides (-a)%Z b). Axiom divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a b). Axiom divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a b). Axiom divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b + c)%Z)). Axiom divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b - c)%Z)). Axiom divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (c * b)%Z). Axiom divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z). Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z). Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z). Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)). Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) -> ((Zabs a) <= (Zabs b))%Z). Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b</