knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_6.v 5.44 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Andrei Paskevich's avatar
Andrei Paskevich committed
3
Require Import BuiltIn.
4
Require Import ZOdiv.
Andrei Paskevich's avatar
Andrei Paskevich committed
5
Require BuiltIn.
6 7 8 9 10 11 12 13 14
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require number.Parity.
Require number.Divisibility.
Require number.Prime.

(* Why3 assumption *)
15 16
Definition unit  := unit.

17 18
(* Why3 assumption *)
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
19

20
(* Why3 assumption *)
21 22 23 24 25 26
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)).

27
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
28
Inductive ref (a:Type) {a_WT:WhyType a} :=
29
  | mk_ref : a -> ref a.
Andrei Paskevich's avatar
Andrei Paskevich committed
30 31 32
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
33

34
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
35
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
36 37
  match v with
  | (mk_ref x) => x
38 39
  end.

Andrei Paskevich's avatar
Andrei Paskevich committed
40 41 42 43
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
  (b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45 46
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b.
47

Andrei Paskevich's avatar
Andrei Paskevich committed
48 49
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  (map a b) -> a -> b -> (map a b).
50

Andrei Paskevich's avatar
Andrei Paskevich committed
51 52 53
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
  ((get (set m a1 b1) a2) = b1).
54

Andrei Paskevich's avatar
Andrei Paskevich committed
55 56 57
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
  {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
  forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
58

Andrei Paskevich's avatar
Andrei Paskevich committed
59 60
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  b -> (map a b).
61

Andrei Paskevich's avatar
Andrei Paskevich committed
62 63
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
  forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
64

65
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
66
Inductive array (a:Type) {a_WT:WhyType a} :=
67
  | mk_array : Z -> (map Z a) -> array a.
Andrei Paskevich's avatar
Andrei Paskevich committed
68 69 70
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
71

72
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
73
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) :=
74 75
  match v with
  | (mk_array x x1) => x1
76 77
  end.

78
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
79
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
80 81
  match v with
  | (mk_array x x1) => x
82 83
  end.

84
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
85 86 87 88 89 90
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a :=
  (get (elts a1) i).

(* Why3 assumption *)
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array
  a) := (mk_array (length a1) (set (elts a1) i v)).
91

92
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
93 94
Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) :=
  (mk_array n (const v:(map Z a))).
95

96 97 98
(* Why3 assumption *)
Definition no_prime_in(l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\
  (x < u)%Z) -> ~ (number.Prime.prime x).
99

100
(* Why3 assumption *)
101
Definition first_primes(p:(array Z)) (u:Z): Prop := ((get1 p 0%Z) = 2%Z) /\
102 103 104 105 106
  ((forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i < j)%Z) /\ (j < u)%Z) ->
  ((get1 p i) < (get1 p j))%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\
  (i < u)%Z) -> (number.Prime.prime (get1 p i))) /\ 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)))).
107 108 109

Axiom exists_prime : forall (p:(array Z)) (u:Z), (1%Z <= u)%Z ->
  ((first_primes p u) -> forall (d:Z), ((2%Z <= d)%Z /\ (d <= (get1 p
110 111
  (u - 1%Z)%Z))%Z) -> ((number.Prime.prime d) -> exists i:Z, ((0%Z <= i)%Z /\
  (i < u)%Z) /\ (d = (get1 p i)))).
112

113 114
Axiom Bertrand_postulate : forall (p:Z), (number.Prime.prime p) ->
  ~ (no_prime_in p (2%Z * p)%Z).
115

116
(* Why3 goal *)
117
Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z ->
118 119 120
  ((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)) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
121 122 123 124 125 126 127 128 129 130 131
  ((2%Z <= (m - 1%Z)%Z)%Z -> forall (n:Z) (p2:(map Z Z)), forall (j:Z),
  ((2%Z <= j)%Z /\ (j <= (m - 1%Z)%Z)%Z) -> (((((first_primes (mk_array m p2)
  j) /\ (((get p2 (j - 1%Z)%Z) < n)%Z /\ (n < (2%Z * (get p2
  (j - 1%Z)%Z))%Z)%Z)) /\ (number.Parity.odd n)) /\ (no_prime_in (get p2
  (j - 1%Z)%Z) n)) -> forall (k:Z), forall (n1:Z) (p3:(map Z Z)),
  (((((((1%Z <= k)%Z /\ (k < j)%Z) /\ (first_primes (mk_array m p3) j)) /\
  (((get p3 (j - 1%Z)%Z) < n1)%Z /\ (n1 < (2%Z * (get p3
  (j - 1%Z)%Z))%Z)%Z)) /\ (number.Parity.odd n1)) /\ (no_prime_in (get p3
  (j - 1%Z)%Z) n1)) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) ->
  ~ (number.Divisibility.divides (get p3 i) n1)) -> (((0%Z <= k)%Z /\
  (k < m)%Z) -> (((ZOmod n1 (get p3 k)) = 0%Z) ->
132 133 134
  ((~ (number.Prime.prime n1)) -> forall (n2:Z), (n2 = (n1 + 2%Z)%Z) ->
  (n2 < (2%Z * (get p3 (j - 1%Z)%Z))%Z)%Z)))))))).
Proof.
135
intros.
136
assert (case: (n2 < 2 * get p3 (j-1) \/ n2 >= 2 * get p3 (j-1))%Z) by omega.
137 138 139
destruct case.
auto.
apply False_ind.
140
apply Bertrand_postulate with (get p3 (j-1)%Z); intuition.
Andrei Paskevich's avatar
Andrei Paskevich committed
141
red in H27; decompose [and] H27; clear H27.
142
apply H30; omega.
143 144
red; intros.
assert (case: (x < n1 \/ x = n1 \/ x = n1+1)%Z) by omega. destruct case.
Andrei Paskevich's avatar
Andrei Paskevich committed
145
apply H22; omega.
146
destruct H30; subst x.
147
intuition.
148 149
intro K.
apply Prime.even_prime in K.
150
omega.
151
now apply Parity.odd_even.
152 153 154
Qed.