(**
 * order.
 * The order of elements in the multgroup modulo p.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require Arith.
Require ZArith.
Require Wf_nat.

Require lemmas.
Require natZ.
Require dec.
Require list.

Require exp.
Require divides.
Require prime.
Require mod.
Require modprime.
Require fermat.

(* (Order b q p) means the order of b is q in multgroup(Z_p). *)

Definition Order :=
   [b:Z][q,p:nat](lt O q) /\
      (Mod (Exp b q) `1` p) /\
         ((d:nat)(lt O d)->(Mod (Exp b d) `1` p)->(le q d)).

Lemma orderdec: (b:Z; q,p:nat)(Order b q p)\/~(Order b q p).
Proof.
   Intros. Unfold Order.
   Apply anddec.
   Apply ltdec.
   Apply anddec.
   Apply moddec.
   Elim (exdec [d:nat](lt O d)/\(Mod (Exp b d) `1` p) q).
   Right. Intros.
   Elim H. Intro d. Intros.
   Elim H0. Intros.
   Elim H2. Intros.
   Intro. Elim (le_not_lt q d).
   Apply H5.
   Assumption.
   Assumption.
   Assumption.
   Left. Intros.
   Elim (le_or_lt q d).
   Intro. Assumption.
   Intro.
   Elim H.
   Split with d.
   Split.
   Assumption.
   Split.
   Assumption.
   Assumption.
   Intro.
   Apply anddec.
   Apply ltdec.
   Apply moddec.
Qed.

Lemma order_ex1: (b:Z)(p:nat)(Prime p)->
                    (EX d:nat | (lt O d)/\(Mod (Exp b d) `1` p))->
                       (EX x:nat | (Order b x p)).
Proof.
   Intros. Elim H0.
   Intro. Apply (lt_wf_ind x).
   Intros X IH.
   Intros.
   Elim (exdec [m:nat](lt O m)/\(Mod (Exp b m) `1` p) X).
   Intro.
   Elim H2. 
   Intros.
   Elim H3. Intros.
   Elim H5. Intros.
   Elim (IH x0). Intros.
   Split with x1.
   Assumption.
   Assumption.
   Split. Assumption. Assumption.
   Intros. Split with X.
   Elim H1. Intros.
   Split.
   Assumption.
   Split.
   Assumption.
   Intros.
   Elim (le_or_lt X d).
   Intro. Assumption.
   Intros.
   Elim H2.
   Split with d.
   Split.
   Assumption.
   Split.
   Assumption.
   Assumption.
   Intro. Apply anddec. Apply ltdec. Apply moddec.
Qed.

Lemma order_ex: (b:Z)(p:nat)(Prime p)->~(Mod b `0` p)->
                   (EX x:nat | (lt x p) /\ (Order b x p)).
Proof.
   Intros.
   Elim H.
   Intros.
   Elim (order_ex1 b p H).
   Intros.
   Split with x.
   Split.
   Apply le_lt_trans with (pred p).
   Elim H3.
   Intros.
   Elim H5.
   Intros.
   Apply (H7 (pred p)).
   Apply lt_pred.
   Assumption.
   Apply flt. Assumption. Assumption.
   Apply lt_pred_n_n.
   Apply lt_trans with (1). Apply lt_O_Sn. Assumption.
   Assumption.
   Split with (pred p).
   Split.
   Apply lt_pred.
   Assumption.
   Apply flt. Assumption. Assumption.
Qed.

Lemma order_div:
   (b:Z)(x,p:nat)(Order b x p) ->
      (y:nat)(lt O y)->(Mod (Exp b y) `1` p)->(Divides x y).
Proof.
   Intros.
   Elim H. Intros.
   Elim H3. Intros.
   Elim (divdec y x). Intro. Assumption. Intro.
   Elim (notdiv_rem x y H2 H6).
   Intro q. Intros. Elim H7. Intro r. Intros.
   Elim H8. Intros. Elim H10. Intros.
   Rewrite H12 in H1.
   Elim (lt_not_le r x).
   Assumption.
   Apply H5.
   Assumption.
   Apply mod_trans with `(Exp b (mult q x))*(Exp b r)`.
   Apply mod_trans with `(Exp (Exp b x) q)*(Exp b r)`.
   Pattern 1 (Exp b r).
   Replace (Exp b r) with `1*(Exp b r)`.
   Apply mod_mult_compat.
   Apply mod_sym.
   Apply mod_exp1.
   Assumption.
   Apply mod_refl.
   Apply Zmult_one.
   Rewrite mult_sym.
   Rewrite exp_mult.
   Apply mod_refl.
   Rewrite <- exp_plus.
   Assumption.
Qed.

Lemma order_le_predp:
   (b:Z)(q,p:nat)(Prime p)->(Order b q p)->(le q (pred p)).
Proof.
   Intros.
   Elim H. Intros.
   Elim H0. Intros.
   Elim H4. Intros.
   Apply H6.
   Apply lt_pred. Assumption.
   Apply flt.
   Assumption.
   Intro.
   Elim (mod_0not1 p).
   Assumption.
   Apply mod_trans with (Exp b q).
   Apply mod_sym.
   Apply moda0_exp_compat.
   Unfold gt.
   Unfold gt in H1.
   Unfold lt.
   Apply lt_le_weak.
   Assumption.
   Assumption.
   Assumption.
   Assumption.
Qed.