Commit 1d032a37 by Jean-Christophe Filliatre

### number theory moved to library number.why

parent 93cf1d36
 ... ... @@ -4,7 +4,7 @@ module EuclideanAlgorithm use import int.Int use import int.Gcd use import number.Gcd use import int.ComputerDivision let rec gcd u v variant { v } = ... ... @@ -13,12 +13,12 @@ module EuclideanAlgorithm u else gcd v (mod u v) { gcd u v result } { result = gcd u v } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/gcd" compile-command: "unset LANG; make -C ../.. examples/programs/gcd.gui" End: *)
 ... ... @@ -2,8 +2,8 @@ (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Require Import ZOdiv. Definition unit := unit. Parameter mark : Type. ... ... @@ -16,31 +16,108 @@ Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition divides(a:Z) (b:Z): Prop := exists q:Z, (b = (q * a)%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 : 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_x_zero : forall (x:Z), (divides x 0%Z). Axiom divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z). Axiom Divides_one_x : forall (x:Z), (divides 1%Z x). Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z). Definition gcd(a:Z) (b:Z) (g:Z): Prop := (divides g a) /\ ((divides g b) /\ forall (x:Z), (divides x a) -> ((divides x b) -> (divides x g))). Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z). Axiom Gcd_sym : forall (a:Z) (b:Z) (g:Z), (gcd a b g) -> (gcd b a g). Axiom divides1 : forall (x:Z), (divides x 1%Z) -> ((x = 1%Z) \/ (x = (-1%Z)%Z)). Axiom Gcd_0 : forall (a:Z), (gcd a 0%Z a). Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). Axiom Gcd_euclid : forall (a:Z) (b:Z) (q:Z) (g:Z), (gcd a (b - (q * a)%Z)%Z g) -> (gcd a b g). Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) -> ((Zabs a) <= (Zabs b))%Z). Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z). (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z). Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z). ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z). Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z). Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z). Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x). Axiom mod_divides : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((Zmod a b) = 0%Z)). 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 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 : forall (a:Z), ((gcd a 0%Z) = a). Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a (b - (q * a)%Z)%Z)). Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z). Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z). Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z). Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ... ... @@ -58,9 +135,9 @@ Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z. Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x). Axiom Div_11 : forall (x:Z), ((ZOdiv x 1%Z) = x). Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z). Axiom Mod_11 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z). Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOdiv x y) = 0%Z). ... ... @@ -74,38 +151,26 @@ Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)). Axiom Gcd_computer_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b) g) -> (gcd a b g)). Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z). Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z). Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z). Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z). Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x). 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) (g:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b) g) -> (gcd a b g)). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b)) = (gcd a b)). 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)) -> forall (result:Z), (gcd v (ZOmod u v) result) -> (gcd u v result))). ((gcd v (ZOmod u v)) = (gcd u v)))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. apply Gcd_sym. apply Gcd_euclid with (q:=(ZOdiv u v)). symmetry. rewrite Comm. rewrite gcd_euclid with (q:=(ZOdiv u v)). assert (u - (ZOdiv u v) * v = ZOmod u v)%Z. generalize (Div_mod u v); intuition. generalize (Div_mod1 u v); intuition. replace ((ZOdiv u v) * v) with (v * (ZOdiv u v)) by ring. omega. rewrite H7; assumption. rewrite H4; auto. Qed. (* DO NOT EDIT BELOW *) ... ...
 ... ... @@ -3,39 +3,39 @@ ... ...
 module M (* Greatest common divisor, with Bézout coefficients *) module GcdBezout use import int.Int use import int.ComputerDivision use import int.Gcd use import number.Gcd use import module ref.Ref let gcd (x:int) (y:int) = ... ... @@ -13,7 +16,7 @@ module M let c = ref 0 in let d = ref 1 in while (!y > 0) do invariant { !x >= 0 /\ !y >= 0 /\ (forall d:int. gcd !x !y d -> gcd (at !x 'Pre) (at !y 'Pre) d) /\ gcd !x !y = gcd (at !x 'Pre) (at !y 'Pre) /\ !a * (at !x 'Pre) + !b * (at !y 'Pre) = !x /\ !c * (at !x 'Pre) + !d * (at !y 'Pre) = !y } variant { !y } ... ... @@ -24,13 +27,13 @@ module M c := ta - !c * q; d := tb - !d * q done; !x { gcd x y result /\ { result = gcd x y /\ exists a b:int. a*x+b*y = result } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/gcd_bezout" compile-command: "unset LANG; make -C ../.. examples/programs/gcd_bezout.gui" End: *)
 ... ... @@ -58,24 +58,57 @@ Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)). Definition divides(a:Z) (b:Z): Prop := exists q:Z, (b = (q * a)%Z). Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). Axiom Divides_x_zero : forall (x:Z), (divides x 0%Z). Axiom divides_refl : forall (n:Z), (divides n n). Axiom Divides_one_x : forall (x:Z), (divides 1%Z x). Axiom divides_1 : forall (n:Z), (divides 1%Z n). Definition gcd(a:Z) (b:Z) (g:Z): Prop := (divides g a) /\ ((divides g b) /\ forall (x:Z), (divides x a) -> ((divides x b) -> (divides x g))). Axiom divides_0 : forall (n:Z), (divides n 0%Z). Axiom Gcd_sym : forall (a:Z) (b:Z) (g:Z), (gcd a b g) -> (gcd b a g). Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z). Axiom Gcd_0 : forall (a:Z), (gcd a 0%Z a). Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z). Axiom Gcd_euclid : forall (a:Z) (b:Z) (q:Z) (g:Z), (gcd a (b - (q * a)%Z)%Z g) -> (gcd a b g). Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z). Axiom Gcd_computer_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b) g) -> (gcd a b g)). 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 divides1 : forall (x:Z), (divides x 1%Z) -> ((x = 1%Z) \/ (x = (-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 Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z). ... ... @@ -90,8 +123,39 @@ Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z). Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b) g) -> (gcd a b g)). Axiom mod_divides : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((Zmod a b) = 0%Z)). 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 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 : forall (a:Z), ((gcd a 0%Z) = a). 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)). Inductive ref (a:Type) := | mk_ref : a -> ref a. ... ... @@ -105,26 +169,25 @@ Implicit Arguments contents. 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 /\ ((forall (d1:Z), (gcd x1 y1 d1) -> (gcd x y d1)) /\ ((((a * x)%Z + (b * y)%Z)%Z = x1) /\ 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), (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) -> forall (d2:Z), (gcd x2 y2 d2) -> (gcd x y d2)). (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> ((gcd x2 y2) = (gcd x y))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. apply H4. rewrite <- H4. subst x2 y2. apply Gcd_sym. apply Gcd_euclid with (q:=(ZOdiv x1 y1)). symmetry. rewrite Comm. rewrite gcd_euclid with (q:=(ZOdiv x1 y1)). assert (x1 - (ZOdiv x1 y1) * y1 = ZOmod x1 y1)%Z. generalize (Div_mod x1 y1); intuition. replace ((ZOdiv x1 y1) * y1) with (y1 * (ZOdiv x1 y1)) by ring. omega. rewrite H6; assumption. rewrite H6; auto. Qed. (* DO NOT EDIT BELOW *) ... ...
 ... ... @@ -2,60 +2,60 @@ ... ...
 (* Knuth's algorithm for prime numbers. The Art of Computer Programming, vol 1, page 147. The following code computes a table of the first m prime numbers. Though there are more efficient ways of computing prime numbers, the nice thing about this code is that it requires not less than Bertrand's postulate (for n > 1, there is always a prime p such that n < p < 2n) to be proved correct. This program had been proved correct using Coq and an early version of Why back in 2003, by Laurent Théry (INRIA Sophia-Antipolis). Laurent Théry. Proving Pearl: Knuth's Algorithm for Prime Numbers. TPHOLs 2003 A truly tour de force, this proof included the full proof of Bertrand's postulate in Coq. Here, we simply focus on the program verification part, assuming Bertrand's postulate as an axiom. Note: Knuth's code is entering the loop where a new prime number is added, thus resulting into the immediate addition of 3 as prime[1]. It allows subsequent division tests to start at prime[1]=3, thus saving the division by prime[0]=2. We did something similar in the code below, though the use of a while loop looks like we did a special case for 3 as well. *) module PrimeNumbers use import int.Int use import int.ComputerDivision use import number.Prime use import module ref.Refint use import module array.Array use import module array.ArraySorted (* returns an array containing the first m prime numbers *) let prime_numbers (m: int) = { m >= 2 } let prime = make m 0 in prime[0] <- 2; prime[1] <- 3; let n = ref 5 in (* candidate for next prime *) for j = 2 to m - 1 do invariant { sorted_sub prime 0 j /\ !n > prime[j-1] } let rec test (k: int) = { 0 <= k < j } if mod !n prime[k] = 0 then begin n += 2; test 1 end else if div !n prime[k] > prime[k] then test (k + 1) { !n >= old !n } in test 1; prime[j] <- !n; n += 2 done; prime { sorted_sub result 0 m } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/knuth_prime_numbers.gui" End: *)
 ... ... @@ -227,51 +227,6 @@ theory Fact "Factorial" end (* number theory *) theory Divisibility use import Int predicate divides (a b : int) = exists q : int. b = q * a lemma Divides_x_zero: forall x:int. divides x 0 lemma Divides_one_x: forall x:int. divides 1 x (* todo: divides x y <-> if y=0 then true else x mod y = 0 *) end theory Gcd use import Int use import Divisibility predicate gcd (a b g : int) = divides g a /\ divides g b /\ forall x : int. divides x a -> divides x b -> divides x g lemma Gcd_sym : forall a b g : int. gcd a b g -> gcd b a g lemma Gcd_0 : forall a : int. gcd a 0 a lemma Gcd_euclid : forall a b q g : int. gcd a (b - q * a) g -> gcd a b g use ComputerDivision lemma Gcd_computer_mod : forall a b g : int [gcd a (ComputerDivision.mod a b) g]. b <> 0 -> gcd a (ComputerDivision.mod a b) g -> gcd a b g use EuclideanDivision lemma Gcd_euclidean_mod : forall a b g : int [gcd a (EuclideanDivision.mod a b) g]. b <> 0 -> gcd a (EuclideanDivision.mod a b) g -> gcd a b g <