knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v 6.65 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

Lemma Zle_sqrt: forall x y, (0 <= x)%Z -> (0 <= y)%Z ->  x*x < y*y -> x<y.
117 118 119 120 121 122
intros x y Hx Hy H.
apply Znot_ge_lt.
intros H'.
apply (Zlt_not_le _ _ H).
apply Zge_le in H'.
now apply Zmult_le_compat.
123 124
Qed.

125
(* Why3 goal *)
126
Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z ->
127 128 129
  ((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
130 131 132 133 134 135 136 137 138 139 140 141 142
  ((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)) -> (((0%Z <= k)%Z /\
  (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) -> ((~ ((get p3
  k) < (ZOdiv n1 (get p3 k)))%Z) -> (number.Prime.prime n1))))))))))).
143
Proof.
Andrei Paskevich's avatar
Andrei Paskevich committed
144 145
intros. intuition.
red in H29. destruct H29 as (p0, (sorted, (only_primes, all_primes))).
146 147
assert (h2: 2 < get p3 k%Z).
rewrite <- p0. apply sorted; omega.
148
apply Prime.small_divisors; auto.
149 150
omega.
intros.
151
generalize (ZO_div_mod_eq n1 (get p3 k)). intro div.
152
assert (ne1: (0 <= n1 /\ get p3 k <> 0)%Z) by omega.
153 154 155 156 157 158
assert (mod1: (0 <= ZOmod n1 (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 (get p3 k) < get p3 k)%Z).
apply ZOmod_lt_pos_pos ; omega.
159 160
assert (d <= get p3 k)%Z.
assert (d < get p3 k+1)%Z. 2: omega.
161
apply Zle_sqrt; try omega.
162 163
assert (2 < get p3 k)%Z. 
rewrite <- p0. apply sorted; omega.
164
apply Zle_lt_trans with n1; try omega.
165
assert (get p3 k * (ZOdiv n1 (get p3 k)) <= get p3 k * get p3 k)%Z.
166
apply Zmult_le_compat_l; try omega.
167
replace ((get p3 k + 1) * (get p3 k + 1))%Z with (get p3 k * get p3 k + 2 * get p3 k + 1)%Z by ring.
168
omega.
169
destruct (exists_prime (mk_array m p3) (k+1))%Z with (d := d) as (i, (hi1, hi2)); auto.
170
omega.
171 172 173 174 175 176 177
red; split; intros.
auto.
split; intros.
apply sorted; omega.
split; intros.
apply only_primes; omega.
apply all_primes; omega.
178 179 180 181 182
unfold get1; simpl.
replace (k+1-1)%Z with k by omega.
auto.
unfold get1 in hi2; simpl in hi2. subst d.
assert (case: (i < k \/i = k)%Z) by omega. destruct case.
Andrei Paskevich's avatar
Andrei Paskevich committed
183
red; intro. apply H19 with i; try omega.
184 185 186
auto.
subst i.
intro. apply H10.
187
apply Divisibility.divides_mod_computer; auto; omega.
188 189 190
Qed.