(** * prime. * The primality predicate. * * @author Olga Caprotti and Martijn Oostdijk * @version $Revision$ *) Require ZArith. Require Wf_nat. Require lemmas. Require natZ. Require dec. Require divides. Require mod. Require list. 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. (* ZPrime, just like Prime but uses only Z. *) Definition ZPrime: Z -> Prop := [n:Z]`n>1` /\ (q:Z)`q>=0` -> (ZDivides q n) -> q=`1` \/ q=n. Lemma primezprime: (n:nat)(Prime n)->(ZPrime (inject_nat n)). Proof. Unfold Prime ZPrime. Intros. Elim H. Intros. Split. Change `(inject_nat n) > (inject_nat (S O))`. Apply inj_gt. Assumption. Intros. Elim (H1 (absolu q)). Left. Rewrite <- (inj_abs_pos q). Rewrite H4. Simpl. Reflexivity. Assumption. Right. Rewrite <- (inj_abs_pos q). Rewrite H4. Reflexivity. Assumption. Rewrite <- (abs_inj n). Apply zdivdiv. Assumption. Qed. Lemma zprimeprime: (n:Z)(ZPrime n)->(Prime (absolu n)). Proof. Unfold ZPrime Prime. Intros. Elim H. Intros. Split. Change (gt (absolu n) (absolu `1`)). Apply gtzgt. Apply Zle_trans with `1`. Unfold Zle. Simpl. Discriminate. Apply Zlt_le_weak. Apply Zgt_lt. Assumption. Unfold Zle. Simpl. Discriminate. Assumption. Intros. Elim (H1 (inject_nat q)). Left. Rewrite <- (abs_inj q). Rewrite H3. Simpl. Reflexivity. Right. Rewrite <- (abs_inj q). Rewrite H3. Reflexivity. Apply nat_ge_0. Apply divzdiv. Rewrite abs_inj. Assumption. Qed. Lemma zprime2: (ZPrime `2`). Proof. Change (ZPrime (inject_nat (2))). Apply primezprime. Exact prime2. Qed. (* All numbers in natlist are prime. *) Definition allPrime := (alllist nat Prime): natlist->Prop. Definition allZPrime := (alllist Z ZPrime): Zlist->Prop. Lemma allzprimeallpos: (l:Zlist)(allZPrime l)->(allPos l). Proof. Unfold allZPrime allPos. Induction l. Simpl. Intro. Assumption. Simpl. Intros h t IH H. Elim H. Intros. Elim H0. Intros. Split. Apply Zle_ge. Apply Zle_trans with `1`. Unfold Zle. Simpl. Discriminate. Apply Zlt_le_weak. Apply Zgt_lt. Assumption. Apply IH. Assumption. Qed. Lemma allprimeallzprime: (l:natlist)(allPrime l)->(allZPrime (Map inject_nat l)). Proof. Unfold allPrime allZPrime. Induction l. Simpl. Intro. Assumption. Simpl. Intros h t IH H. Elim H. Intros. Split. Apply primezprime. Assumption. Apply IH. Assumption. Qed. Lemma allzprimeallprime: (l:Zlist)(allZPrime l)->(allPrime (Map absolu l)). Proof. Unfold allPrime allZPrime. Induction l. Simpl. Intro. Assumption. Simpl. Intros h t IH H. Elim H. Intros. Split. Apply zprimeprime. Assumption. Apply IH. Assumption. Qed.