(**
 * modprime.
 * Some nice lemmas about div, mult, mod, prime, and gcd. 
 *
 * @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 gcd.

Transparent inject_nat.

Lemma prime_div_or_gcd1:
   (p:nat)(a:Z)(Prime p)->
      (ZDivides (inject_nat p) a)\/(gcd (inject_nat p) a (1)).
Proof.
   Intros. Elim (zdivdec a (inject_nat p)).
   Left. Assumption.
   Right. Unfold gcd. Unfold common_div.
   Split. Split.
   Split with p. Simpl. Rewrite <- plus_n_O. Apply abs_inj.
   Split with (absolu a). Simpl. Apply plus_n_O.
   Intros. Elim H1. Intros. Rewrite abs_inj in H2.
   Elim (primediv1p p e).
   Intro. Rewrite H4. Apply le_n.
   Intro. Rewrite H4 in H3. Elim H0. Apply divzdiv.
   Rewrite abs_inj. Assumption. Assumption. Assumption.
Qed.

Lemma divmultgcd:
   (a,b,c:Z)`a<>0`->(ZDivides a `b*c`)->(gcd a b (1))->(ZDivides a c).
Proof.
   Intros. Elim (gcd_lincomb a b (1)).
   Intro alpha. Intros. Elim H2. Intro beta. Intros.
   Elim H0. Intro y. Intros.
   Split with `c*alpha+y*beta`. Rewrite Zmult_plus_distr_r.
   Rewrite Zmult_assoc_l. Rewrite Zmult_assoc_l.
   Rewrite <- H4. Rewrite (Zmult_sym a c). Rewrite (Zmult_sym b c).
   Rewrite Zmult_assoc_r. Rewrite Zmult_assoc_r.
   Rewrite <- Zmult_plus_distr_r. Transitivity `c*1`.
   Rewrite Zmult_sym. Rewrite Zmult_one. Reflexivity.
   Apply (f_equal Z). Assumption. Assumption. Assumption.
Qed.

Lemma primedivmult:
   (p,n,m:nat)(Prime p)->
      (Divides p (mult n m))->(Divides p n)\/(Divides p m).
Proof.
   Intros. Elim (prime_div_or_gcd1 p (inject_nat n)).
   Left. Rewrite <- (abs_inj p). Rewrite <- (abs_inj n).
   Apply zdivdiv. Assumption.
   Right. Rewrite <- (abs_inj p). Rewrite <- (abs_inj m).
   Apply zdivdiv. Apply divmultgcd with (inject_nat n).
   Elim H. Intros. Apply Zgt_neq.
   Change `(inject_nat p) > (inject_nat O)`. Apply inj_gt.
   Apply gt_trans with (1). Assumption. Unfold gt. Unfold lt. Apply le_n.
   Rewrite <- inj_mult. Apply divzdiv. Rewrite abs_inj. Rewrite abs_inj.
   Assumption. Assumption. Assumption.
Qed.

Lemma mod_mult_inv_r:
   (a:Z)(p:nat)(Prime p)->~(Mod a `0` p)->(EX ra:Z | (Mod `a*ra` `1` p)).
Proof.
   Intros. Elim (prime_div_or_gcd1 p a).

   (* case p divides a *)
   Intro. Elim H0. Elim H1. Intros. Split with x. Simpl. Assumption.

   (* case gcd(p,a)=1 *)
   Intro. Elim (gcd_lincomb (inject_nat p) a (1)).
   Intro alpha. Intros. Elim H2. Intro beta. Intros.
   Unfold Mod. Split with beta. Split with `-alpha`.
   Simpl in H3. Rewrite H3.
   Rewrite (Zplus_sym `(inject_nat p)*alpha`). Rewrite Zplus_assoc_r.
   Rewrite <- Zmult_plus_distr_r. Rewrite Zplus_inverse_r.
   Rewrite <- Zmult_n_O. Rewrite <- Zplus_n_O. Reflexivity.
   Apply Zgt_neq. Change `(inject_nat p) > (inject_nat O)` .
   Apply inj_gt. Apply gt_trans with (1). Elim H. Intros. Assumption.
   Unfold gt. Unfold lt. Apply le_n.
   Assumption. Assumption.
Qed.

Lemma mod_mult_cancel_r:
   (a,b,c:Z; p:nat)(Prime p)->~(Mod c `0` p)->
      (Mod `a*c` `b*c` p)->(Mod a b p).
Proof.
   Intros. Elim (mod_mult_inv_r c p). Intro rc. Intros.
   Apply mod_trans with `a*c*rc`. Rewrite Zmult_assoc_r.
   Pattern 1 a. Replace a with `a*1`. Apply mod_mult_compat. Apply mod_refl.
   Apply mod_sym. Assumption.
   Rewrite Zmult_sym. Apply Zmult_one.
   Apply mod_trans with `b*c*rc`.
   Apply mod_mult_compat. Assumption. Apply mod_refl. Rewrite Zmult_assoc_r.
   Pattern 2 b. Replace b with `b*1`. Apply mod_mult_compat. Apply mod_refl.
   Assumption.
   Rewrite Zmult_sym. Apply Zmult_one.
   Assumption. Assumption.
Qed.

Lemma mod_mult_0:
   (p:nat)(a,b:Z)(Prime p)->
      (Mod `a*b` `0` p)->(Mod a `0` p)\/(Mod b `0` p).
Proof.
   Intros.
   Elim (moddivmin `a*b` `0` p).
   Intros.
   Rewrite <- Zminus_n_O in H1.
   Rewrite abs_mult in H1.
   Elim (primedivmult p (absolu a) (absolu b)).
   Left. Elim (moddivmin a `0` p). Intros.
   Apply H5. Rewrite <- Zminus_n_O. Assumption.
   Right. Elim (moddivmin b `0` p). Intros.
   Apply H5. Rewrite <- Zminus_n_O. Assumption.
   Assumption.
   Apply H1.
   Assumption.
Qed.

Lemma mod_not_exp_0:
   (p:nat)(Prime p)->
      (a:Z)~(Mod a `0` p) -> (m:nat)~(Mod (Exp a m) `0` p).
Proof.
   Intros p Hp a Ha. Induction m.
   Simpl. Intro. Elim (mod_0not1 p).
   Elim Hp. Intros. Assumption.
   Apply mod_sym. Assumption.
   Simpl. Intros. Intro.
   Elim (mod_mult_0 p a (Exp a n) Hp).
   Assumption. 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).
 * I.e. If you divide by a non-trivial divisor, then the other
 * divisor contains a prime factor.
 *)

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.