(**
 * pock.
 * Pocklington's criterion.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require Arith.
Require ZArith.

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

(**
 * 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).
   Split.
   Intros. Apply H. Assumption. Assumption.
   Intros. Apply H0. Assumption.
Qed.

(**
 * Pocklington's theorem (finally).
 * 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).
   Intros AH1 AH2. Elim (AH1 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.


(**
 * Below is an attempt to restate Pocklington's theorem
 * using only numbers from Z. This will make concrete
 * computations faster.
 *)

(* ZallLinCombMod is equivalent to AllLinCombMod but uses Z. *)

Definition ZallLinCombMod :=
   [a:Z; n,m:Z; N:Z; qlist:Zlist]
      (alllist Z [q:Z](ZLinCombMod `1`
                `(ZExp a (Zmult m (zmultDrop q qlist)))-1`
                      n N)
         qlist).

Lemma ZallLinCombMod_ok:
   (a:Z)(n,m:Z)(N:Z)(qlist:Zlist)
      (ZallLinCombMod a n m N qlist) ->
         (qi:Z)(inlist Z qi qlist) ->
            (ZLinCombMod `1`
               `(ZExp a (Zmult m (zmultDrop qi qlist)))-1`
               n N).
Proof.
   Intros.
   Elim (alllist_ok Z
         [q:Z]
         (ZLinCombMod `1`
            `((ZExp a (Zmult m (zmultDrop q qlist))))-1`
            n N) qlist).
   Intros. Apply H1. Assumption. Assumption.
Qed.

Lemma alllincombzalllincomb:
   (a,n,m:Z)(qlist:Zlist)
      `0<=n` ->
         `0<=m` ->
            (allPos qlist) ->
               (ZallLinCombMod a n m n qlist) ->
                  (allLinCombMod a (absolu n) (absolu m) (Map absolu qlist)).
Proof.
   Intros.
   Unfold ZallLinCombMod in H.
   Elim (alllist_ok Z
          [q:Z]
           (ZLinCombMod `1`
             `((ZExp a) (Zmult m (zmultDrop q qlist)))-1` n
             n) qlist).
   Intros.
   Elim (alllist_ok nat
          [q0:nat]
           (LinCombMod `1`
             `((Exp a) (mult (absolu m) (multDrop q0 (Map absolu qlist))))-1`
             (inject_nat (absolu n)) (absolu n)) (Map absolu qlist)).
   Intros.
   Apply H6. 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 zlincombmodlincombmod.
   Rewrite inj_mult. Rewrite inj_abs_pos.
   Rewrite multdropzmultdrop.
   Rewrite inj_abs_pos_list.
   Apply H3.
   Assumption.
   Apply inlist_inj_abs_pos_list.
   Assumption. Assumption.
   Assumption.
   Apply Zle_ge. 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. *)

Theorem Zpocklington:
   (n,q,m:Z)(a:Z)(qlist:Zlist)
   `n>1` -> `0<=q` -> `0<=m` ->
      `n=q*m+1` ->
         q=(zproduct qlist) ->
            (allZPrime qlist) ->
               (ZMod (ZExp a `n-1`) `1` n) ->
                  (ZallLinCombMod a n m n qlist) ->
                     `n <= q*q` ->
                        (ZPrime n).
Proof.
   Intros. Cut `0 <= n`. Intros.
   Rewrite <- (inj_abs_pos n). Apply primezprime.
   Apply (pocklington (absolu n) (absolu q) (absolu m) a (Map absolu 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.
   Apply zproductproduct.
   Apply allzprimeallprime. 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.
   Apply zmodmod.
   Assumption.
   Apply alllincombzalllincomb.
   Assumption.
   Assumption.
   Apply allzprimeallpos.
   Assumption.
   Assumption.
   Rewrite <- abs_mult.
   Apply lezle.
   Assumption.
   Apply isnat_mult.
   Assumption.
   Assumption.
   Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_trans with `1`.
   Unfold Zle. Simpl. Discriminate.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
Qed.