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

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

17 18 19 20
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.

21
(* Why3 assumption *)
22
Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
23

24
(* Why3 assumption *)
25 26 27 28 29 30
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)).

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

38
(* Why3 assumption *)
39
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
40 41
  match v with
  | (mk_ref x) => x
42 43
  end.

44
(* Why3 assumption *)
45 46 47
Inductive array
  (a:Type) {a_WT:WhyType a} :=
  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49 50
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
51

52
(* Why3 assumption *)
53 54
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
  Z _ a a_WT) := match v with
55
  | (mk_array x x1) => x1
56 57
  end.

58
(* Why3 assumption *)
59
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
60 61
  match v with
  | (mk_array x x1) => x
62 63
  end.

64
(* Why3 assumption *)
65
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
66
  (map.Map.get (elts a1) i).
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68

(* Why3 assumption *)
69 70 71
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
  (v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
  v)).
72

73
(* Why3 assumption *)
74
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
75
  (mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))).
76

77
(* Why3 assumption *)
78
Definition no_prime_in (l:Z) (u:Z): Prop := forall (x:Z), ((l < x)%Z /\
79
  (x < u)%Z) -> ~ (number.Prime.prime x).
80

81
(* Why3 assumption *)
82
Definition first_primes (p:(@array Z _)) (u:Z): Prop := ((get p
Andrei Paskevich's avatar
Andrei Paskevich committed
83 84
  0%Z) = 2%Z) /\ ((forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ ((i < j)%Z /\
  (j < u)%Z)) -> ((get p i) < (get p j))%Z) /\ ((forall (i:Z),
85 86 87 88 89
  ((0%Z <= i)%Z /\ (i < u)%Z) -> (number.Prime.prime (get p i))) /\
  forall (i:Z), ((0%Z <= i)%Z /\ (i < (u - 1%Z)%Z)%Z) -> (no_prime_in (get p
  i) (get p (i + 1%Z)%Z)))).

Axiom exists_prime : forall (p:(@array Z _)) (u:Z), (1%Z <= u)%Z ->
90
  ((first_primes p u) -> forall (d:Z), ((2%Z <= d)%Z /\ (d <= (get p
91
  (u - 1%Z)%Z))%Z) -> ((number.Prime.prime d) -> exists i:Z, ((0%Z <= i)%Z /\
92
  (i < u)%Z) /\ (d = (get p i)))).
93

94 95
Axiom Bertrand_postulate : forall (p:Z), (number.Prime.prime p) ->
  ~ (no_prime_in p (2%Z * p)%Z).
96

97
Lemma Zle_sqrt: forall x y, (0 <= x -> 0 <= y -> x*x < y*y -> x<y)%Z.
98 99 100 101 102 103
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.
104 105
Qed.

106 107
Import Zquot.

108
(* Why3 goal *)
109
Theorem WP_parameter_prime_numbers : forall (m:Z), (2%Z <= m)%Z ->
Andrei Paskevich's avatar
Andrei Paskevich committed
110
  ((0%Z <= m)%Z -> ((0%Z <= m)%Z -> (((0%Z <= 0%Z)%Z /\ (0%Z < m)%Z) ->
111
  forall (p:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\
112
  (p = (map.Map.set (map.Map.const 0%Z: (@map.Map.map Z _ Z _)) 0%Z 2%Z))) ->
113 114 115
  (((0%Z <= 1%Z)%Z /\ (1%Z < m)%Z) -> forall (p1:(@map.Map.map Z _ Z _)),
  ((0%Z <= m)%Z /\ (p1 = (map.Map.set p 1%Z 3%Z))) -> let o := (m - 1%Z)%Z in
  ((2%Z <= o)%Z -> forall (n:Z) (p2:(@map.Map.map Z _ Z _)), forall (j:Z),
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117 118 119 120 121 122 123 124 125
  ((2%Z <= j)%Z /\ (j <= o)%Z) -> (((first_primes (mk_array m p2) j) /\
  ((((map.Map.get p2 (j - 1%Z)%Z) < n)%Z /\ (n < (2%Z * (map.Map.get p2
  (j - 1%Z)%Z))%Z)%Z) /\ ((number.Parity.odd n) /\ (no_prime_in
  (map.Map.get p2 (j - 1%Z)%Z) n)))) -> forall (k:Z), forall (n1:Z)
  (p3:(@map.Map.map Z _ Z _)), ((0%Z <= m)%Z /\ (((1%Z <= k)%Z /\
  (k < j)%Z) /\ ((first_primes (mk_array m p3) j) /\ ((((map.Map.get p3
  (j - 1%Z)%Z) < n1)%Z /\ (n1 < (2%Z * (map.Map.get p3 (j - 1%Z)%Z))%Z)%Z) /\
  ((number.Parity.odd n1) /\ ((no_prime_in (map.Map.get p3 (j - 1%Z)%Z)
  n1) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) ->
  ~ (number.Divisibility.divides (map.Map.get p3 i) n1))))))) ->
126 127 128 129
  (((0%Z <= k)%Z /\ (k < m)%Z) ->
  ((~ ((ZArith.BinInt.Z.rem n1 (map.Map.get p3 k)) = 0%Z)) ->
  (((0%Z <= k)%Z /\ (k < m)%Z) -> (((0%Z <= k)%Z /\ (k < m)%Z) ->
  ((~ ((map.Map.get p3 k) < (ZArith.BinInt.Z.quot n1 (map.Map.get p3
Andrei Paskevich's avatar
Andrei Paskevich committed
130
  k)))%Z) -> (number.Prime.prime n1)))))))))))).
131 132 133 134
(* Why3 intros m h1 h2 h3 (h4,h5) p (h6,h7) (h8,h9) p1 (h10,h11) o h12 n p2 j
        (h13,h14) (h15,((h16,h17),(h18,h19))) k n1 p3
        (h20,((h21,h22),(h23,((h24,h25),(h26,(h27,h28)))))) (h29,h30) h31
        (h32,h33) (h34,h35) h36. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
135 136 137 138 139 140 141
intros m h1 h2 h3 (h4,h5) p (h6,h7) (h8,h9) p1 (h10,h11) o h12 n p2 j
        (h13,h14) (h15,((h16,h17),(h18,h19))) k n1 p3
        (h20,((h21,h22),(h23,((h24,h25),(h26,(h27,h28)))))) (h29,h30) h31
        (h32,h33) (h34,h35) h36.
intuition.
red in h23. destruct h23 as (p0, (sorted, (only_primes, all_primes))).
assert (H2: (2 < Map.get p3 k)%Z).
142
rewrite <- p0. apply sorted; omega.
143
apply Prime.small_divisors; auto.
144 145
omega.
intros.
146
generalize (Z_quot_rem_eq n1 (Map.get p3 k)). intro div.
147
assert (ne1: (0 <= n1 /\ Map.get p3 k <> 0)%Z) by omega.
148
assert (mod1: (0 <= Z.rem n1 (Map.get p3 k))%Z).
149
destruct (not_Zeq_inf _ _ (proj2 ne1)) as [Zm|Zm].
150 151 152 153
now apply Zrem_lt_pos_neg.
now apply Zrem_lt_pos_pos.
assert (mod2: (Z.rem n1 (Map.get p3 k) < Map.get p3 k)%Z).
apply Zrem_lt_pos_pos ; omega.
154 155
assert (d <= Map.get p3 k)%Z.
assert (d < Map.get p3 k+1)%Z. 2: omega.
156
apply Zle_sqrt; try omega.
157
assert (2 < Map.get p3 k)%Z. 
158
rewrite <- p0. apply sorted; omega.
159
apply Zle_lt_trans with n1; try omega.
160
assert (Map.get p3 k * (Z.quot n1 (Map.get p3 k)) <= Map.get p3 k * Map.get p3 k)%Z.
161
apply Zmult_le_compat_l; try omega.
162
replace ((Map.get p3 k + 1) * (Map.get p3 k + 1))%Z with (Map.get p3 k * Map.get p3 k + 2 * Map.get p3 k + 1)%Z by ring.
163
omega.
164
destruct (exists_prime (mk_array m p3) (k+1))%Z with (d := d) as (i, (hi1, hi2)); auto.
165
omega.
166 167 168 169 170 171 172
red; split; intros.
auto.
split; intros.
apply sorted; omega.
split; intros.
apply only_primes; omega.
apply all_primes; omega.
173
unfold get; simpl.
174 175
replace (k+1-1)%Z with k by omega.
auto.
176
unfold get in hi2; simpl in hi2. subst d.
177
assert (case: (i < k \/i = k)%Z) by omega. destruct case.
Andrei Paskevich's avatar
Andrei Paskevich committed
178
red; intro. apply h28 with i; try omega.
179 180
auto.
subst i.
Andrei Paskevich's avatar
Andrei Paskevich committed
181
intro. apply h31.
182
apply Divisibility.divides_mod_computer; auto; omega.
183 184
Qed.