Require Arith.
Require ZArith.

Require lemmas.
Require natZ.
Require dec.
Require list.
Require exp.
Require divides.
Require prime.
Require mod.
Require gcd.
Require modprime.


(**
 * All numbers in natlist are prime.
 *)

Definition allPrime := (alllist nat Prime): natlist->Prop.


(**
 * For all numbers q in natlist qlist: 1 is a linear combination
 * of a^(m*qlist/qi) and n modulo n.
 *)

Definition allLinCombMod :=
   [a:Z; n,m:nat; qlist:natlist]
      (alllist nat [q:nat](LinCombMod `1`
                      `(Exp a (mult m (multDrop q qlist)))-1`
                      (inject_nat n) n)
         qlist).

Lemma allLinCombMod_ok:
   (a:Z)(n,m:nat)(qlist:natlist)
      (allLinCombMod a n m qlist) ->
         (qi:nat)(inlist nat qi qlist) ->
            (LinCombMod `1`
               `((Exp a) ((mult m) ((multDrop qi) qlist)))-1`
               (inject_nat n) n).
Proof.
   Intros.
   Elim (alllist_ok nat
         [q:nat]
            (LinCombMod `1` `((Exp a) ((mult m) ((multDrop q) qlist)))-1`
            (inject_nat n) n) qlist).
   Intros. Apply H1. Assumption. Assumption.
Qed.


(**
 * This lemma simply states that: if a divides b where 0<a<b,
 * then there is a prime factor qi of b such that a divides (b/qi).
 *)

Lemma techlemma3:
   (qlist:natlist)(a,b:nat)(lt O a)->(lt a b)->(Divides a b)->
      b=(product qlist)->(allPrime qlist)->
         (EX qi:nat | (inlist nat qi qlist)/\(Divides a (multDrop qi qlist))).
Proof.
   Induction qlist.
   Simpl. Intros. Rewrite H2 in H0.
   Elim (lt_not_le a (1)). Assumption. Unfold lt in H. Assumption.
   Intros qi restqs IH. Intros.
   Elim (divdec a qi).

   (* case (Divides qi a) *)

   Intro.
   Elim H1. Intro x. Intros.
   Elim H4. Intro y. Intros.
   Elim (IH y (product restqs)). Intro qj. Intros.
   Elim H7. Intros.
   Split with qj.
   Split.
   Unfold inlist. Simpl. Right. Assumption.
   Rewrite H6.
   Elim H9. Intro z. Intros.
   Elim (eqdec qi qj).
   Intro. Rewrite H11. Rewrite multdrop_cons_eq.
   Rewrite <- (multdrop_mult restqs qj). Split with z.
   Rewrite mult_assoc_r. Rewrite H10. Reflexivity. Assumption.

   Intro. Rewrite multdrop_cons_neq.
   Split with z.
   Rewrite mult_assoc_r.
   Rewrite H10.
   Reflexivity.
   Intro. Elim H11. Rewrite H12. Reflexivity.

   Elim (le_or_lt y O). Intro.
   Elim (le_lt_or_eq y O). Intro.
   Elim (lt_n_O y). Assumption.
   Intro. Rewrite H8 in H6. Rewrite <- mult_n_O in H6. Rewrite H6 in H.
   Elim (lt_n_O O). Assumption.
   Assumption.
   Intro. Assumption.

   Apply simpl_lt_mult_l with qi.
   Rewrite <- H6.
   Simpl in H2.
   Rewrite <- H2.
   Assumption.

   Simpl in H2.
   Rewrite H5 in H2.
   Rewrite H6 in H2.
   Split with x.
   Rewrite mult_assoc_r in H2.
   Apply simpl_eq_mult_l with qi.
   Unfold allPrime in H3.
   Simpl in H3.
   Elim H3.
   Intros.
   Elim H7.
   Intros.
   Apply lt_trans with (1).
   Apply lt_O_Sn.
   Assumption.
   Symmetry.
   Assumption.
   Reflexivity.
   Unfold allPrime in H3.
   Simpl in H3.
   Elim H3.
   Intros.
   Assumption.

   (* case ~(Divides qi a) *)

   Intros.
   Split with qi.
   Split.
   Unfold inlist.
   Simpl.
   Left.
   Elim (beq_nat_ok qi qi).
   Intros.
   Reflexivity.
   Rewrite multdrop_cons_eq.
   Elim H1.
   Intros.
   Simpl in H2.
   Unfold Divides.
   Unfold allPrime in H3.
   Simpl in H3.
   Elim H3.
   Intros.
   Elim (primedivmult qi a x H6).
   Intro.
   Elim H4.
   Assumption.
   Intros.
   Elim H8. Intro z. Intros.
   Split with z.
   Rewrite H2 in H5.
   Rewrite H9 in H5.
   Rewrite (mult_assoc_l a qi) in H5.
   Rewrite (mult_sym a) in H5.
   Rewrite (mult_assoc_r qi a) in H5.
   Apply simpl_eq_mult_l with qi.
   Elim H6.
   Intros.
   Apply lt_trans with (1). Apply lt_O_Sn.
   Assumption.
   Assumption.
   Split with (product restqs). Rewrite <- H5. Assumption.
Qed.


(**
 * The Pocklington theorem.
 * Proves Pocklington for natural numbers.
 *)

Theorem pocklington:
   (n,q,m:nat)(a:Z)(qlist:natlist)
      (gt n (1)) ->
         n=(S (mult q m)) ->
            q=(product qlist) ->
               (allPrime qlist) ->
                  (Mod (Exp a (pred n)) `1` n) ->
                     (allLinCombMod a n m qlist) ->
                        (le n (mult q q)) ->
                           (Prime n).
Proof.
   Intros.
   Apply primepropdiv. Assumption. Intro p. Intros.
   Elim H6. Intros.
   Elim H7. Intro pdn. Intros.
   Unfold gt.
   Apply le_lt_trans with (mult (pred p) (pred p)).
   Apply le_trans with (mult q q).
   Assumption.
   Cut (le q (pred p)). Intros.
   Apply le_le_mult. Assumption. Assumption.
   Apply order_le_predp with (Exp a m).
   Assumption.
   Cut (Mod (Exp (Exp a m) q) `1` p). Intros.
   Elim (order_ex (Exp a m) p). Intro r. Intros.
   Elim H12. Intros.
   Elim H14. Intros.
   Elim H16. Intros.
   Elim (le_lt_or_eq r q).
   Intro.
   Cut (Divides r q). Intros.
   Elim (techlemma3 qlist r q). Intro qi. Intros.
   Elim H21. Intros.
   Elim H23. Intro rdm. Intros.
   Elim (allLinCombMod_ok a n m qlist H4 qi H22).
   Intro alpha. Intros. Elim H25. Intro beta. Intros.
   Elim (mod_0not1 p).
   Assumption.
   Apply mod_trans with `(1-1)*alpha+(inject_nat n)*beta`.
   Rewrite H10. Simpl.
   Rewrite inj_mult.
   Rewrite Zmult_assoc_r.
   Apply mod_sym.
   Apply mod_nx_0_n.
   Apply mod_trans with
      `(((Exp a) ((mult m) ((multDrop qi) qlist)))-1)*alpha+
       (inject_nat n)*beta`.
   Apply mod_plus_compat. Apply mod_mult_compat. Apply mod_minus_compat.
   Rewrite H24.
   Rewrite mult_assoc_l.
   Apply mod_sym.
   Rewrite exp_mult. Apply mod_exp1. Rewrite exp_mult.
   Assumption.
   Apply mod_refl.
   Apply mod_refl.
   Apply mod_refl.
   Apply mod_sym. Apply modpq_modp with pdn. Rewrite <- H10. Assumption.
   Assumption.
   Assumption.
   Assumption.
   Assumption.
   Assumption.
   Apply (order_div (Exp a m) r p H14 q).
   Apply lt_trans with r.
   Assumption.
   Assumption.
   Assumption.
   Intro. Rewrite <- H19. Assumption.
   Apply H18.
   Elim (le_lt_or_eq O q).
   Intro. Assumption.
   Intro. Rewrite <- H19 in H5. Simpl in H5. Elim (le_not_lt n O). Assumption.
   Apply lt_trans with (1). Apply lt_O_Sn. Assumption. Apply le_O_n.
   Assumption.
   Assumption.
   Apply mod_not_exp_0.
   Assumption.
   Intro. Elim (mod_0not1 p). Assumption.
   Apply mod_trans with (Exp a (pred n)).
   Apply mod_sym.
   Apply moda0_exp_compat.
   Unfold gt. Apply lt_trans with (1). Apply lt_O_Sn.
   Assumption.
   Assumption.
   Apply gt_pred. Assumption.
   Rewrite H0. Simpl. Rewrite mult_sym. Rewrite exp_mult. Assumption.
   Rewrite H0 in H3. Simpl in H3. Rewrite <- H0 in H3.
   Apply modpq_modp with pdn.
   Rewrite <- H10. Rewrite <- exp_mult. Rewrite mult_sym. Assumption.
   Apply lt_multpred_pp. Assumption.
Qed.


(**
 * ZallLinCombMod is equivalent to AllLinCombMod but uses Z.
 * This will make computations faster.
 *)

Definition ZallLinCombMod :=
   [a:Z; n,m:Z; N:nat; qlist:natlist]
      (alllist nat [q:nat](LinCombMod `1`
                `(ZExp a (inject_nat (mult (absolu m) (multDrop q qlist))))-1`
                      n N)
         qlist).

Lemma ZallLinCombMod_ok:
   (a:Z)(n,m:Z)(N:nat)(qlist:natlist)
      (ZallLinCombMod a n m N qlist) ->
         (qi:nat)(inlist nat qi qlist) ->
            (LinCombMod `1`
               `(ZExp a (inject_nat (mult (absolu m) (multDrop qi qlist))))-1`
               n N).
Proof.
   Intros.
   Elim (alllist_ok nat
         [q:nat]
         (LinCombMod `1`
            `((ZExp a (inject_nat (mult (absolu m) (multDrop q qlist)))))-1`
            n N) qlist).
   Intros. Apply H1. Assumption. Assumption.
Qed.

Lemma alllincombzalllincomb:
   (a,n,m:Z)(qlist:natlist)
      `0<=n` ->
         `0<=m` ->
            (ZallLinCombMod a n m (absolu n) qlist) ->
               (allLinCombMod a (absolu n) (absolu m) qlist).
Proof.
   Intros.
   Unfold ZallLinCombMod in H.
   Elim (alllist_ok nat
          [q:nat]
           (LinCombMod `1`
             `((ZExp a) (inject_nat (mult (absolu m) (multDrop q qlist))))-1` n
             (absolu n)) qlist).
   Intros.
   Elim (alllist_ok nat
          [q0:nat]
           (LinCombMod `1`
             `((Exp a) (mult (absolu m) (multDrop q0 qlist)))-1`
             (inject_nat (absolu n)) (absolu n)) qlist).
   Intros.
   Apply H5. Intros.
   Rewrite <- inj_zexp.
   Rewrite inj_mult.
   Rewrite inj_abs_pos.
   Rewrite inj_abs_pos.
   Replace m with (inject_nat (absolu m)).
   Rewrite <- inj_mult.
   Apply H2.
   Assumption.
   Assumption.
   Apply inj_abs_pos.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Assumption.
Qed.

(**
 * Zpocklington is equivalent to pocklington but only uses numbers in Z.
 * This will make computations faster.
 *)

Theorem Zpocklington:
   (n,q,m:Z)(a:Z)(qlist:natlist)
   `n>1` -> `0<=q` -> `0<=m` ->
      `n=q*m+1` ->
         `q=(inject_nat (product qlist))` ->
            (allPrime qlist) ->
               (Mod (ZExp a `n-1`) `1` (absolu n)) ->
                  (ZallLinCombMod a n m (absolu n) qlist) ->
                     `n <= q*q` ->
                        (Prime (absolu n)).
Proof.
   Intros. Cut `0 <= n`. Intros.
   Apply (pocklington (absolu n) (absolu q) (absolu m) a qlist).
   Change (gt (absolu n) (absolu `1`)) . Apply gtzgt. Assumption.
   Unfold Zle. Simpl. Discriminate.
   Assumption.
   Rewrite H2. Rewrite abs_plus_pos. Rewrite abs_mult. Rewrite plus_sym.
   Simpl. Reflexivity.
   Apply isnat_mult.
   Assumption.
   Assumption.
   Unfold Zle.
   Simpl.
   Discriminate.
   Rewrite H3.
   Rewrite abs_inj.
   Reflexivity.
   Assumption.
   Apply mod_trans with (ZExp a `n-1`).
   Rewrite <- inj_zexp.
   Rewrite abs_pred_pos.
   Rewrite inj_abs_pos.
   Apply mod_refl.
   Apply Zle_ge.
   Unfold Zminus.
   Simpl.
   Change `0 <= 0+n+(-1)` .
   Rewrite (Zplus_assoc_r `0`).
   Rewrite Zplus_sym.
   Apply (Zlt_left `0` n).
   Apply Zlt_trans with `1`.
   Unfold Zlt.
   Simpl.
   Reflexivity.
   Apply Zgt_lt.
   Assumption.
   Apply Zlt_trans with `1`.
   Unfold Zlt.
   Simpl.
   Reflexivity.
   Apply Zgt_lt.
   Assumption.
   Assumption.
   Apply alllincombzalllincomb.
   Assumption.
   Assumption.
   Assumption.
   Rewrite <- abs_mult.
   Apply lezle.
   Assumption.
   Apply isnat_mult.
   Assumption.
   Assumption.
   Assumption.
   Apply Zle_trans with `1`.
   Unfold Zle. Simpl. Discriminate.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
Qed.