Require Arith.
Require Wf_nat.

Require lemmas.
Require dec.
Require divides.
Require mod.

(* Defines Primality *)

Definition Prime: nat -> Prop :=
   [n:nat](gt n (1)) /\ (q:nat)(Divides q n) -> q=(1) \/ q=n.

(* prime with bounded all quantifier *)

Definition bPrime :=
   [n:nat](gt n (1))/\((q:nat)(lt q (S n)) -> (Divides q n) -> q=(1)\/q=n).

Lemma primebprime: (n:nat)(Prime n) <-> (bPrime n).
Proof.
   Unfold Prime bPrime.
   Split.
   Intro. Elim H.
   Split.
   Assumption.
   Intros.
   Apply H1.
   Assumption.
   Intro. Elim H.
   Split.
   Assumption.
   Intros.
   Apply H1.
   Unfold lt.
   Apply le_n_S.
   Apply div_le.
   Apply lt_trans with (1). Apply lt_O_Sn. Assumption.
   Assumption.
   Assumption.
Qed.

(* prime is decidable *)

Lemma bprimedec: (n:nat) (bPrime n) \/ ~(bPrime n).
Proof.
   Unfold bPrime. Intros.
   Apply anddec.
   Apply gtdec.
   Apply (alldec [q:nat](Divides q n)->q=(1)\/q=n (S n)).
   Intros.
   Apply impdec.
   Apply divdec.
   Apply ordec.
   Apply eqdec.
   Apply eqdec.
Qed.

Lemma primedec: (n:nat) (Prime n) \/ ~(Prime n).
Proof.
   Intro. Elim (primebprime n).
   Intros. Elim (bprimedec n).
   Left. Apply (H0 H1).
   Right. Intro. Apply H1. Apply (H H2).
Qed.

(* non-primes n>1 have non-trivial divisors *)

Lemma nonprime_witness:
   (n:nat)
      (gt n (1)) ->
          ~(Prime n) ->
             (EX d:nat | (lt (1) d) /\ (lt d n) /\ (Divides d n)).
Proof.
   Intro n. Case n.
   Intro. Elim (lt_n_O (1)). Assumption.
   Intro n1. Case n1. Intro. Elim (lt_n_n (1)). Assumption.
   Intro n2. Intros.
   Elim (decDeMorgan (S (S n2)) [d:nat](lt (1) d)/\(Divides d (S (S n2)))).
   Intros. Elim H2. Intros.
   Split with x.
   Elim H3. Intros.
   Elim H5. Intros.
   Split.
   Assumption.
   Split.
   Assumption.
   Assumption.
   Intro. Apply H0. Unfold Prime. Split. Assumption.
   Intro q. Case q.
   Intro. Unfold Divides in H4. Elim H4. Simpl. Intros. Discriminate H5.
   Intro q1. Case q1. Left. Reflexivity.
   Intro q2. Intros. Right.
   Elim (le_lt_or_eq (S (S q2)) (S (S n2))).
   Intros. Elim (H3 (S (S q2))). Assumption.
   Split. Apply lt_n_S. Apply lt_O_Sn. Assumption.
   Intros. Assumption.
   Apply div_le1. Assumption.
   Intros. Apply anddec. Apply ltdec. Apply divdec.
Qed.

Lemma nonprime_sqrwitness:
   (n:nat)
      (gt n (1)) ->
          ~(Prime n) ->
             (EX d:nat | (lt (1) d) /\ (le (mult d d) n) /\ (Divides d n)).
Proof.
   Intros. Elim (nonprime_witness n).
   Intro d. Intros.
   Elim (sqrdivbound n d). Intro d'. Intros.
   Elim H2. Intros.
   Elim H4. Intros.
   Elim H6.
   Intro. Split with d'.
   Split. Rewrite H7. Elim H1. Tauto.
   Split. Assumption.
   Rewrite H7. Elim H1. Tauto.
   Intro. Split with d'. Split. Apply (lt_n_nm_m_gt_1 d d').
   Rewrite H7. Elim H1. Tauto.
   Split. Assumption.
   Assumption.
   Elim H1. Tauto.
   Assumption.
   Assumption.
Qed.

(* non-primes n>1 have prime-divisors *)

Theorem nonprime_primewitness:
   (n:nat)
      (gt n (1)) ->
          ~(Prime n) ->
             (EX d:nat | (lt (1) d) /\ (le (mult d d) n) /\
                         (Divides d n) /\ (Prime d)).
Proof.
   Intro. Apply (lt_wf_ind n).
   Intros N IH. Intros.
   Elim (nonprime_sqrwitness N). Intro x. Intros.
   Elim H1. Intros.
   Elim H3. Intros.
   Elim (primedec x).
   Intros.
   Split with x.
   Split. Assumption.
   Split. Assumption.
   Split. Assumption.
   Assumption.
   Intros. Elim (IH x). Intros.
   Elim H7. Intros.
   Elim H9. Intros.
   Elim H11.
   Intros.
   Split with x0.
   Split. Assumption.
   Split. Apply le_trans with (mult x x).
   Apply le_trans with x. Assumption. Apply le_n_nn. Assumption.
   Split. Apply div_trans with x. Assumption. Assumption.
   Assumption.
   Unfold lt. Apply le_trans with (mult x x).
   Change (lt x (mult x x)). Apply sqr_ascend. Assumption.
   Assumption. Assumption. Assumption. Assumption. Assumption.
Qed.


(* prime(n) if all prime divisors > sqrt(n) *)

Theorem primepropdiv: (n:nat)(gt n (1)) ->
                       ((q:nat)(Prime q)->(Divides q n)->(gt (mult q q) n)) ->
                           (Prime n).
Proof.
   Intros. Elim (primedec n).
   Intro. Assumption.
   Intros. Elim (nonprime_primewitness n).
   Intros.
   Elim H2. Intros.
   Elim H4. Intros.
   Elim H6. Intros.
   Elim (le_not_lt (mult x x) n).
   Assumption.
   Unfold gt in H0. Apply H0. Assumption. Assumption.
   Assumption.
   Assumption.
Qed.

Lemma primediv1p: (p,n:nat)(Prime p)->(Divides n p)->n=(1)\/n=p.
Proof.
   Intros.
   Unfold Prime in H.Elim H.Intros.
   Apply (H2 n). Assumption.
Qed.

(* two is a prime *)

Lemma prime2: (Prime (2)).
Proof.
   Apply primepropdiv.
   Auto.
   Intro q. Case q.
   Intros. Elim H. Intro.
   Elim (lt_n_O (1)). Assumption.
   Intro q1. Case q1.
   Intros. Elim H. Intro.
   Elim (lt_n_n (1)). Assumption.
   Intro q2. Case q2.
   Simpl. Intros. Auto.
   Intro q3. Simpl. Intros.
   Repeat Apply gt_n_S. Apply gt_Sn_O.
Qed.