Require ZArith.

Require natZ.
Require exp.
Require divides.

(* (Mod a b n) means (a = b (mod n)) *)

Definition Mod := [a,b:Z;n:nat](EX q:Z | `a = b + (inject_nat n) * q`).

Lemma modpq_modp: (a,b:Z; p,q:nat)(Mod a b (mult p q))->(Mod a b p).
Proof.
   Unfold Mod.
   Intros.
   Elim H.
   Intros.
   Split with `(inject_nat q)*x`.
   Rewrite (inj_mult p q) in H0.
   Rewrite Zmult_assoc.
   Assumption.
Qed.

Lemma mod_refl: (a:Z)(n:nat)(Mod a a n).
Proof.
   Unfold Mod. Intros.
   Split with `0`.
   Rewrite <- Zmult_n_O.
   Rewrite <- Zplus_n_O.
   Reflexivity.
Qed.

Lemma mod_sym: (a,b:Z)(n:nat)(Mod a b n)->(Mod b a n).
Proof.
   Unfold Mod. Intros.
   Elim H.
   Intros.
   Split with `-x`.
   Simpl.
   Rewrite H0.
   Simpl.
   Rewrite Zplus_assoc_r.
   Rewrite <- Zmult_plus_distr_r.
   Rewrite Zplus_inverse_r.
   Rewrite <- Zmult_n_O.
   Apply Zplus_n_O.
Qed.

Lemma mod_trans: (a,b,c:Z)(n:nat)(Mod a b n)->(Mod b c n)->(Mod a c n).
Proof.
   Unfold Mod. Intros.
   Elim H. Elim H0.
   Intros. Rewrite H2. Rewrite H1.
   Split with `x+x0`.
   Rewrite Zmult_plus_distr_r.
   Rewrite (Zplus_assoc_l c `(inject_nat n)*x` `(inject_nat n)*x0`).
   Reflexivity.
Qed.

Lemma eqmod: (x,y:Z)x=y -> (n:nat)(Mod x y n).
Proof.
   Intros. Rewrite H. Apply mod_refl.
Qed.

Lemma mod_plus_compat:
   (a,b,c,d:Z)(n:nat)(Mod a b n) -> (Mod c d n) -> (Mod `a+c` `b+d` n).
Proof.
   Unfold Mod. Intros.
   Elim H. Elim H0.
   Intros. Split with `x+x0`.
   Rewrite H1.
   Rewrite H2.
   Rewrite (Zplus_assoc_l `b+(inject_nat n)*x0` d `(inject_nat n)*x`).
   Rewrite (Zplus_assoc_r b `(inject_nat n)*x0` d).
   Rewrite (Zplus_sym `(inject_nat n)*x0` d).
   Rewrite (Zplus_sym x x0).
   Rewrite (Zmult_plus_distr_r (inject_nat n) x0 x).
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_assoc_l.
   Reflexivity.
Qed.

Lemma mod_mult_compat:
   (a,b,c,d:Z)(n:nat)(Mod a b n) -> (Mod c d n) -> (Mod `a*c` `b*d` n).
Proof.
   Unfold Mod. Intros.
   Elim H. Elim H0.
   Intros. Rewrite H1. Rewrite H2. Split with `x0*d+x*b+(inject_nat n)*x0*x`.
   Rewrite (Zmult_plus_distr_r `b+(inject_nat n)*x0` d `(inject_nat n)*x`).
   Rewrite Zmult_plus_distr_l.
   Rewrite Zmult_plus_distr_l.
   Rewrite (Zmult_assoc_l b (inject_nat n) x).
   Rewrite (Zmult_sym b (inject_nat n)).
   Rewrite (Zmult_assoc_l `(inject_nat n)*x0` (inject_nat n) x).
   Rewrite (Zmult_assoc_r (inject_nat n) x0 (inject_nat n)).
   Rewrite (Zmult_assoc_r (inject_nat n) `x0*(inject_nat n)` x).
   Rewrite (Zmult_assoc_r (inject_nat n) b x).
   Rewrite <- (Zmult_plus_distr_r (inject_nat n) `b*x` `x0*(inject_nat n)*x`).
   Rewrite (Zplus_assoc_r `b*d`).
   Rewrite (Zmult_assoc_r (inject_nat n) x0 d).
   Rewrite <- (Zmult_plus_distr_r (inject_nat n) `x0*d`
               `b*x+x0*(inject_nat n)*x`).
   Rewrite (Zmult_sym x0 (inject_nat n)).
   Rewrite Zplus_assoc_l.
   Rewrite (Zmult_sym b x).
   Reflexivity.
Qed.

Lemma mod_sqr_compat:
   (a,b:Z)(n:nat)(Mod a b n) -> (Mod `a*a` `b*b` n).
Proof.
   Intros. Apply mod_mult_compat. Assumption. Assumption.
Qed.

(*

Lemma mod_exp_compat:
   (a,b:Z)(n:nat)(Mod a b n)->(m:nat)(Mod (Exp a m) (Exp b m) n).
Proof.
Qed.

*)

Lemma moda0_exp_compat:
   (a:Z)(n:nat)(gt n O)->(Mod a `0` n) ->
      (m:nat)(gt m O)->(Mod (Exp a m) `0` n).
Proof.
   Intros a n.
   Case n.
   Intro.
   Elim (lt_n_n O).
   Assumption.
   Intro.
   Intro.
   Intro.
   Intro.
   Case m.
   Intro.
   Elim (lt_n_n O).
   Assumption.
   Intro m0.
   Intros.
   Elim H0.
   Intros.
   Rewrite H2.
   Split with `x*((Exp ((inject_nat (S n0))*x)) m0)`.
   Rewrite Zmult_assoc_l.
   Simpl.
   Reflexivity.
Qed.

Lemma mod_opp_compat:
   (a,b:Z)(n:nat)(Mod a b n) -> (Mod `-a` `-b` n).
Proof.
   Intros. Elim H. Intros.
   Split with `-x`. Rewrite H0.
   Rewrite Zopp_one.
   Rewrite Zopp_one.
   Rewrite Zopp_one.
   Rewrite Zmult_assoc_l.
   Rewrite <- Zmult_plus_distr_l.
   Reflexivity.
Qed.

Lemma mod_minus_compat:
   (a,b,c,d:Z)(n:nat)(Mod a b n) -> (Mod c d n) -> (Mod `a-c` `b-d` n).
Proof.
   Intros.
   Unfold Zminus.
   Apply mod_plus_compat.
   Assumption.
   Apply mod_opp_compat.
   Assumption.
Qed.

Lemma mod_nx_0_n: (n:nat)(x:Z)(Mod `(inject_nat n)*x` `0` n).
Proof.
   Intros. Unfold Mod.
   Split with x.
   Simpl. Reflexivity.
Qed.

Lemma moddivmin: (a,b:Z; n:nat)(Mod a b n)<->(Divides n (absolu `a-b`)).
Proof.
   Unfold Mod Divides. Split.
   Intros.
   Elim H.
   Intros.
   Rewrite H0.
   Unfold Zminus.
   Rewrite Zplus_assoc_r.
   Rewrite Zplus_sym.
   Rewrite Zplus_assoc_r.
   Rewrite (Zplus_sym `-b` b).
   Rewrite Zplus_inverse_r.
   Rewrite <- Zplus_n_O.
   Split with (absolu x).
   Pattern 2 n.
   Rewrite <- (abs_inj n).
   Apply abs_mult.
   Intros. Elim H. Intros.
   Elim (Zle_or_lt b a).
   Split with (inject_nat x).
   Rewrite <- inj_mult.
   Rewrite <- H0.
   Rewrite inj_abs_pos.
   Unfold Zminus.
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_sym.
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_inverse_l.
   Simpl. Reflexivity.
   Apply Zle_ge.
   Replace `0` with `b-b`. Unfold Zminus.
   Apply Zle_reg_r. Assumption.
   Unfold Zminus.
   Apply Zplus_inverse_r.
   Split with `-(inject_nat x)`.
   Rewrite Zmult_sym.
   Rewrite Zopp_Zmult.
   Rewrite <- inj_mult.
   Rewrite mult_sym.
   Rewrite <- H0.
   Rewrite inj_abs_neg.
   Rewrite Zopp_Zopp.
   Unfold Zminus.
   Rewrite (Zplus_sym a).
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_inverse_r.
   Simpl. Reflexivity.
   Replace `0` with `b-b`. Unfold Zminus.
   Rewrite (Zplus_sym a). Rewrite (Zplus_sym b). Apply Zlt_reg_l.
   Assumption.
   Unfold Zminus. Apply Zplus_inverse_r.
Qed.

Lemma moddec: (a,b:Z)(n:nat)(Mod a b n)\/~(Mod a b n).
Proof.
   Intros.
   Elim (moddivmin a b n).
   Intros.
   Elim (divdec (absolu `a-b`) n).
   Left.
   Apply H0.
   Assumption.
   Right.
   Intro.
   Elim H1.
   Apply H.
   Assumption.
Qed.

Lemma mod_0not1: (n:nat)(gt n (1))->~(Mod `0` `1` n).
Proof.
   Intros.
   Intro.
   Absurd (Divides n (1)).
   Intro.
   Elim (le_not_lt n (1)).
   Apply div_le1.
   Assumption.
   Assumption.
   Elim (moddivmin `0` `1` n).
   Intros.
   Apply H1.
   Assumption.
Qed.

Lemma mod_exp1:
   (a:Z)(n:nat)(Mod a `1` n) -> (m:nat)(Mod (Exp a m) `1` n).
Proof.
   Intros a n H.
   Induction m.
   Simpl.
   Apply mod_refl.
   Intros m1 IH.
   Simpl.
   Replace `1` with `1*1`.
   Apply mod_mult_compat.
   Assumption.
   Apply IH.
   Simpl.
   Reflexivity.
Qed.

Lemma mod_repr_non_0:
   (n:nat; x:Z)`0 < x < (inject_nat n)`->~(Mod x `0` n).
Proof.
   Intros.
   Intro.
   Elim H.
   Intros.
   Elim (moddivmin x `0` n).
   Rewrite <- Zminus_n_O.
   Intros.
   Elim (le_not_lt n (absolu x)).
   Apply div_le.
   Change (lt (absolu `0`) (absolu x)) .
   Apply ltzlt.
   Unfold Zle.
   Simpl.
   Discriminate.
   Apply Zlt_le_weak.
   Assumption.
   Assumption.
   Apply H3.
   Assumption.
   Rewrite <- (abs_inj n).
   Apply ltzlt.
   Apply Zlt_le_weak.
   Assumption.
   Change `(inject_nat O) <= (inject_nat n)` .
   Apply inj_le.
   Apply le_O_n.
   Assumption.
Qed.