Commit 65b2b501 by Jean-Christophe Filliatre

### knuth prime numbers: proof

parent 51b27042
 ... ... @@ -30,33 +30,74 @@ module PrimeNumbers use import int.Int use import int.ComputerDivision use import int.Lex2 use import number.Parity use import number.Divisibility use import number.Prime use import module ref.Refint use import module array.Array use import module array.ArraySorted predicate sorted (p: array int) (u: int) = forall i j: int. 0 <= i < j < u -> p[i] < p[j] predicate only_primes (p: array int) (u: int) = forall i: int. 0 <= i < u -> prime p[i] predicate no_prime_in (l u: int) = forall x: int. l < x < u -> not (prime x) predicate all_primes (p: array int) (u: int) = forall i: int. 0 <= i < u-1 -> no_prime_in p[i] p[i+1] lemma exists_prime: forall p: array int, u: int. 1 <= u -> p[0] = 2 -> sorted p u -> only_primes p u -> all_primes p u -> forall d: int. 2 <= d <= p[u-1] -> prime d -> exists i: int. 0 <= i < u /\ d = p[i] lemma Bertrand_postulate: forall p: int. prime p -> not (no_prime_in p (2*p)) lemma small_divisors: forall p: int. 2 <= p -> (forall d: int. 2 <= d -> prime d -> 1 < d*d <= p -> not (divides d p)) -> prime p (* 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 p = make m 0 in p[0] <- 2; p[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 } invariant { p[0] = 2 /\ sorted p j /\ only_primes p j /\ all_primes p j /\ p[j-1] < !n < 2*p[j-1] /\ odd !n /\ no_prime_in p[j-1] !n } let rec test (k: int) variant { (2*p[j-1] - !n, j - k) } with lex = { 1 <= k < j /\ p[0] = 2 /\ sorted p j /\ only_primes p j /\ all_primes p j /\ p[j-1] < !n < 2*p[j-1] /\ odd !n /\ no_prime_in p[j-1] !n /\ forall i: int. 0 <= i < k -> not (divides p[i] !n) } if mod !n p[k] = 0 then begin assert { not (prime !n) }; n += 2; test 1 end else if div !n p[k] > p[k] then test (k + 1) else assert { prime !n } { p[j-1] < !n /\ prime !n /\ no_prime_in p[j-1] !n } in test 1; prime[j] <- !n; p[j] <- !n; n += 2 done; prime { sorted_sub result 0 m } p { result[0] = 2 /\ sorted result m /\ only_primes result m /\ all_primes result m } end ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod 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). Axiom Mod_bound : 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) -> (0%Z <= (ZOdiv x y))%Z. Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) -> ((ZOdiv x y) <= 0%Z)%Z. Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (ZOmod x y))%Z. Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((ZOmod x y) <= 0%Z)%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 Mod_1 : 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). Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOmod x y) = x). Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%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 lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z. 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 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 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)). Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a). Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a). Definition prime(p:Z): Prop := (2%Z <= p)%Z /\ forall (n:Z), ((1%Z < n)%Z /\ (n < p)%Z) -> ~ (divides n p). Axiom not_prime_1 : ~ (prime 1%Z). Axiom prime_2 : (prime 2%Z). Axiom prime_3 : (prime 3%Z). Axiom prime_divisors : forall (p:Z), (prime p) -> forall (d:Z), (divides d p) -> ((d = 1%Z) \/ ((d = (-1%Z)%Z) \/ ((d = p) \/ (d = (-p)%Z)))). Axiom even_prime : forall (p:Z), (prime p) -> ((even p) -> (p = 2%Z)). Axiom odd_prime : forall (p:Z), (prime p) -> ((3%Z <= p)%Z -> (odd p)). 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 end. Implicit Arguments contents. Parameter map : forall (a:Type) (b:Type), Type. Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Implicit Arguments get. Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Implicit Arguments set. Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). Parameter const: forall (b:Type) (a:Type), b -> (map a b). Set Contextual Implicit. Implicit Arguments const. Unset Contextual Implicit. Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( b1):(map a b)) a1) = b1). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | mk_array _ elts1 => elts1 end. Implicit Arguments elts. Definition length (a:Type)(u:(array a)): Z := match u with | mk_array length1 _ => length1 end. Implicit Arguments length. Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) end. Implicit Arguments set1. Definition sorted(p:(array Z)) (u:Z): Prop := forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i < j)%Z) /\ (j < u)%Z) -> ((get1 p i) < (get1 p j))%Z. Definition only_primes(p:(array Z)) (u:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < u)%Z) -> (prime (get1 p i)). Definition no_prime_in(l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\ (x < u)%Z) -> ~ (prime x). Definition all_primes(p:(array Z)) (u:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < (u - 1%Z)%Z)%Z) -> (no_prime_in (get1 p i) (get1 p (i + 1%Z)%Z)). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z -> ((0%Z <= m)%Z -> (((0%Z <= 0%Z)%Z /\ (0%Z < m)%Z) -> forall (p:(map Z Z)), (p = (set (const(0%Z):(map Z Z)) 0%Z 2%Z)) -> (((0%Z <= 1%Z)%Z /\ (1%Z < m)%Z) -> forall (p1:(map Z Z)), (p1 = (set p 1%Z 3%Z)) -> ((2%Z <= (m - 1%Z)%Z)%Z -> forall (n:Z), forall (p2:(map Z Z)), let p3 := (mk_array m p2) in forall (j:Z), ((2%Z <= j)%Z /\ (j <= (m - 1%Z)%Z)%Z) -> ((((get p2 0%Z) = 2%Z) /\ ((sorted p3 j) /\ ((only_primes p3 j) /\ ((all_primes p3 j) /\ ((((get p2 (j - 1%Z)%Z) < n)%Z /\ (n < (2%Z * (get p2 (j - 1%Z)%Z))%Z)%Z) /\ ((odd n) /\ (no_prime_in (get p2 (j - 1%Z)%Z) n))))))) -> ((((1%Z <= 1%Z)%Z /\ (1%Z < j)%Z) /\ ((((get p2 (j - 1%Z)%Z) < n)%Z /\ (n < (2%Z * (get p2 (j - 1%Z)%Z))%Z)%Z) /\ ((odd n) /\ (no_prime_in (get p2 (j - 1%Z)%Z) n)))) -> forall (n1:Z), (((get p2 (j - 1%Z)%Z) < n1)%Z /\ ((prime n1) /\ (no_prime_in (get p2 (j - 1%Z)%Z) n1))) -> (((0%Z <= j)%Z /\ (j < m)%Z) -> forall (p4:(map Z Z)), (p4 = (set p2 j n1)) -> forall (n2:Z), (n2 = (n1 + 2%Z)%Z) -> (odd n2)))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. intros. subst. apply odd_odd. apply odd_prime. intuition. intuition. unfold sorted in H12. unfold get1 in H12. simpl in H12. assert (2 < get p2 (j - 1))%Z. rewrite <- H8. apply H12. omega. omega. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod 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). Axiom Mod_bound : 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) -> (0%Z <= (ZOdiv x y))%Z. Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) -> ((ZOdiv x y) <= 0%Z)%Z. Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (ZOmod x y))%Z. Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((ZOmod x y) <= 0%Z)%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 Mod_1 : 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). Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOmod x y) = x). Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%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 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 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 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)). Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a). Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a). Definition prime(p:Z): Prop := (2%Z <= p)%Z /\ forall (n:Z), ((1%Z < n)%Z /\ (n < p)%Z) -> ~ (divides n p). Axiom not_prime_1 : ~ (prime 1%Z). Axiom prime_2 : (prime 2%Z). Axiom prime_3 : (prime 3%Z). Axiom prime_divisors : forall (p:Z), (prime p) -> forall (d:Z), (divides d p) -> ((d = 1%Z) \/ ((d = (-1%Z)%Z) \/ ((d = p) \/ (d = (-p)%Z)))). Axiom even_prime : forall (p:Z), (prime p) -> ((even p) -> (p = 2%Z)). Axiom odd_prime : forall (p:Z), (prime p) -> ((3%Z <= p)%Z -> (odd p)). 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 end. Implicit Arguments contents. Parameter map : forall (a:Type) (b:Type), Type. Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Implicit Arguments get. Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Implicit Arguments set. Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). Parameter const: forall (b:Type) (a:Type), b -> (map a b). Set Contextual Implicit. Implicit Arguments const. Unset Contextual Implicit. Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( b1):(map a b)) a1) = b1). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | mk_array _ elts1 => elts1 end.