Prime.v 3.97 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3
Require Import BuiltIn.
4
Require Import ZOdiv.
5
Require BuiltIn.
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require number.Parity.
Require number.Divisibility.

Import Znumtheory.

(* Why3 assumption *)
Definition prime(p:Z): Prop := (2%Z <= p)%Z /\ forall (n:Z), ((1%Z < n)%Z /\
  (n < p)%Z) -> ~ (number.Divisibility.divides n p).

Lemma prime_is_Zprime :
  forall p, prime p <-> Znumtheory.prime p.
Proof.
intros p.
apply iff_trans with (2 := prime_alt p).
unfold prime, prime'.
intuition.
Qed.

(* Why3 goal *)
Lemma not_prime_1 : ~ (prime 1%Z).
intros (H1,_).
now elim H1.
Qed.

(* Why3 goal *)
Lemma prime_2 : (prime 2%Z).
Proof.
apply <- prime_is_Zprime.
apply prime_2.
Qed.

(* Why3 goal *)
Lemma prime_3 : (prime 3%Z).
Proof.
apply <- prime_is_Zprime.
apply prime_3.
Qed.

(* Why3 goal *)
Lemma prime_divisors : forall (p:Z), (prime p) -> forall (d:Z),
  (number.Divisibility.divides d p) -> ((d = 1%Z) \/ ((d = (-1%Z)%Z) \/
  ((d = p) \/ (d = (-p)%Z)))).
Proof.
intros p Hp d Hd.
apply -> prime_is_Zprime in Hp.
destruct (prime_divisors p Hp d Hd) ; intuition.
Qed.

(* Why3 goal *)
Lemma small_divisors : forall (p:Z), (2%Z <= p)%Z -> ((forall (d:Z),
  (2%Z <= d)%Z -> ((prime d) -> (((1%Z < (d * d)%Z)%Z /\
  ((d * d)%Z <= p)%Z) -> ~ (number.Divisibility.divides d p)))) ->
  (prime p)).
Proof.
intros p Hp H.
apply <- prime_is_Zprime.
destruct (prime_dec p) as [Pp|Pp].
exact Pp.
elimtype False.
(* *)
assert (exists d, (2 <= d)%Z /\ (d * d <= p)%Z /\ prime d /\ Zdivide d p).
clear H.
assert (Hp' : (0 <= p)%Z) by omega.
revert p Hp' Hp Pp.
apply (Zlt_0_ind (fun p => 2 <= p -> ~ Znumtheory.prime p -> (exists d : Z, 2 <= d /\ d * d <= p /\ prime d /\ (d | p)))%Z).
intros p IH _ Hp Pp.
destruct (not_prime_divide p) as (x,(Hx1,Hx2)).
clear -Hp ; omega.
exact Pp.
destruct (Zle_or_lt (x * x) p) as [Hx|Hx].
destruct (prime_dec x) as [Px|Px].
exists x.
split.
clear -Hx1 ; omega.
split.
exact Hx.
split.
now apply <- prime_is_Zprime.
exact Hx2.
destruct (IH x) as (y&Hy1&Hy2&Hy3&Hy4).
clear -Hx1 ; omega.
clear -Hx1 ; omega.
exact Px.
exists y.
refine (conj Hy1 (conj _ (conj Hy3 _))).
apply Zle_trans with (1 := Hy2).
apply Zle_trans with (2 := Hx).
rewrite <- (Zmult_1_r x) at 1.
apply Zmult_le_compat_l.
now apply Zlt_le_weak.
clear -Hx1 ; omega.
now apply Zdivide_trans with x.
case Hx2.
intros q Hq1.
assert (Hq2 : (2 <= q)%Z).
apply (Zlt_le_succ 1).
apply Zmult_lt_reg_r with x.
clear -Hx1 ; omega.
now rewrite Zmult_1_l, <- Hq1.
destruct (prime_dec q) as [Pq|Pq].
exists q.
split.
exact Hq2.
split.
rewrite Hq1.
apply Zmult_le_compat_l.
apply Zlt_le_weak.
apply Zmult_lt_reg_r with x.
clear -Hx1 ; omega.
now rewrite <- Hq1.
clear -Hq2 ; omega.
split.
now apply <- prime_is_Zprime.
exists x.
now rewrite Zmult_comm.
destruct (IH q) as (y&Hy1&Hy2&Hy3&Hy4).
split.
clear -Hq2 ; omega.
rewrite <- (Zmult_1_r q), Hq1.
apply Zmult_lt_compat_l.
clear -Hq2 ; omega.
clear -Hx1 ; omega.
exact Hq2.
exact Pq.
exists y.
refine (conj Hy1 (conj _ (conj Hy3 _))).
apply Zle_trans with (1 := Hy2).
rewrite <- (Zmult_1_r q), Hq1.
apply Zmult_le_compat_l.
clear -Hx1 ; omega.
clear -Hq2 ; omega.
apply Zdivide_trans with (1 := Hy4).
exists x.
now rewrite Zmult_comm.
destruct H0 as (y&Hy1&Hy2&Hy3&Hy4).
apply (H y) ; try easy.
split.
apply Zlt_le_trans with (2 * 2)%Z.
easy.
now apply Zmult_le_compat.
exact Hy2.
Qed.

(* Why3 goal *)
Lemma even_prime : forall (p:Z), (prime p) -> ((number.Parity.even p) ->
  (p = 2%Z)).
Proof.
intros p Pp (q,Hq).
generalize (proj2 Pp q).
assert (Zdivide q p).
now exists 2%Z.
intros.
refine (_ (fun H1 => H0 H1 H) (proj1 Pp)).
(* ??? omega fails to solve this goal ??? *)
clear -Hq.
intros H Hp.
destruct (Zle_lt_or_eq 2 p Hp) as [Hp'|Hp'].
elim H.
omega.
easy.
Qed.

(* Why3 goal *)
Lemma odd_prime : forall (p:Z), (prime p) -> ((3%Z <= p)%Z ->
  (number.Parity.odd p)).
Proof.
intros p Pp Hp.
apply <- Divisibility.odd_divides.
apply proj2 in Pp.
apply Pp.
omega.
Qed.