(**
 * mod.
 * Modulo Arithmetic.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require ZArith.

Require lemmas.
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.

Lemma mod_repr_eq:
   (p:nat)(x,y:Z)(lt O p)->
      `0 < x < (inject_nat p)`->
      `0 < y < (inject_nat p)`->
         (Mod x y p)->x=y.
Proof.
   Intros. Unfold Mod in H2.
   Elim H2. Intros q Hq.
   Rewrite Hq in H0.
   Elim H0. Elim H1. Intros.
   Elim (Zle_or_lt `0` q).
   Intro. Elim (Zle_lt_or_eq `0` q).

   (* 0<q *)
   Intro. Elim (Zlt_not_le `0` y).
   Assumption. Apply Zsimpl_le_plus_l with (inject_nat p).
   Rewrite (Zplus_sym (inject_nat p)).
   Rewrite (Zplus_sym (inject_nat p)). Simpl.
   Apply Zlt_le_weak.
   Apply Zle_lt_trans with `y+(inject_nat p)*q`.
   Apply Zle_reg_l. Pattern 1 (inject_nat p). 
   Rewrite <- Zmult_one with (inject_nat p).
   Rewrite (Zmult_sym `1`). Apply Zle_mult_l.
   Change `(inject_nat O) < (inject_nat p)`.
   Apply inj_lt. Assumption.
   Change `(Zs 0) <= q`. Apply Zlt_le_S. Assumption.
   Assumption.

   (* 0=q *)
   Intro. Rewrite <- H8 in Hq. Rewrite Zmult_sym in Hq.
   Rewrite Zplus_sym in Hq. Simpl in Hq. Assumption.

   Assumption.

   (* q<0 *)
   Intro. Elim (Zlt_not_le `0` `y+(inject_nat p)*q`).
   Assumption. Apply Zle_trans with `y+(inject_nat p)*(-1)`.
   Apply Zle_reg_l. Apply Zle_mult_l.
   Change `(inject_nat O) < (inject_nat p)`. Apply inj_lt.
   Assumption. Apply Zlt_n_Sm_le. Simpl. Assumption.
   Apply Zsimpl_le_plus_l with (inject_nat p).
   Rewrite (Zplus_sym (inject_nat p)).
   Rewrite (Zplus_sym (inject_nat p)).
   Rewrite (Zmult_sym (inject_nat p)).
   Rewrite (Zopp_Zmult `1`). Rewrite Zmult_one.
   Rewrite Zplus_assoc_r. Rewrite Zplus_inverse_l.
   Rewrite(Zplus_sym y `0`). Simpl. Apply Zlt_le_weak.
   Assumption.
Qed.

(* ZMod, same as Mod but only uses Z. *)

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

Lemma zmodpq_modp: (a,b:Z; p,q:Z)(ZMod a b (Zmult p q))->(ZMod a b p).
Proof.
   Unfold ZMod.
   Intros.
   Elim H.
   Intros.
   Split with `q*x`.
   Rewrite Zmult_assoc.
   Assumption.
Qed.

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

Lemma zmod_sym: (a,b:Z)(n:Z)(ZMod a b n)->(ZMod b a n).
Proof.
   Unfold ZMod. 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 zmod_trans: (a,b,c:Z)(n:Z)(ZMod a b n)->(ZMod b c n)->(ZMod a c n).
Proof.
   Unfold ZMod. Intros.
   Elim H. Elim H0.
   Intros. Rewrite H2. Rewrite H1.
   Split with `x+x0`.
   Rewrite Zmult_plus_distr_r.
   Rewrite (Zplus_assoc_l c `n*x` `n*x0`).
   Reflexivity.
Qed.

Lemma zeqmod: (x,y:Z)x=y -> (n:Z)(ZMod x y n).
Proof.
   Intros. Rewrite H. Apply zmod_refl.
Qed.

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

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

Lemma zmod_sqr_compat:
   (a,b:Z)(n:Z)(ZMod a b n) -> (ZMod `a*a` `b*b` n).
Proof.
   Intros. Apply zmod_mult_compat. Assumption. Assumption.
Qed.

Lemma zmodmod: (a,b:Z)(n:Z)(ZMod a b n)->(Mod a b (absolu n)).
Proof.
   Unfold ZMod Mod.
   Intros. Elim H. Intros.
   Rewrite H0.
   Elim (Zle_or_lt `0` n).
   Intro. Rewrite inj_abs_pos.
   Split with x. Reflexivity.
   Apply Zle_ge. Assumption.
   Intro. Rewrite inj_abs_neg.
   Split with `-x`. Rewrite Zopp_Zmult.
   Rewrite Zopp_Zmult_r. Rewrite Zopp_Zopp.
   Reflexivity.
   Assumption.
Qed.

Lemma modzmod: (a,b:Z)(n:nat)(Mod a b n)->(ZMod a b (inject_nat n)).
Proof.
   Unfold Mod ZMod. Intros. Elim H.
   Intros. Rewrite H0. Split with x.
   Reflexivity.
Qed.

(*

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

*)

Lemma zmoda0_exp_compat:
   (a:Z)(n:Z)(Zgt n `0`)->(ZMod a `0` n) ->
      (m:Z)(Zgt m `0`)->(ZMod (ZExp a m) `0` n).
Proof.
   Intros. Rewrite <- (inj_abs_pos n).
   Apply modzmod. Rewrite expzexp.
   Apply moda0_exp_compat.
   Change (gt (absolu n) (absolu `0`)). Apply gtzgt.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Apply Zle_refl. Reflexivity.
   Assumption.
   Apply zmodmod. Assumption.
   Change (gt (absolu m) (absolu `0`)). Apply gtzgt.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Apply Zle_refl. Reflexivity.
   Assumption.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
Qed.

Lemma zmod_opp_compat:
   (a,b:Z)(n:Z)(ZMod a b n) -> (ZMod `-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 zmod_minus_compat:
   (a,b,c,d:Z)(n:Z)(ZMod a b n) -> (ZMod c d n) -> (ZMod `a-c` `b-d` n).
Proof.
   Intros.
   Unfold Zminus.
   Apply zmod_plus_compat.
   Assumption.
   Apply zmod_opp_compat.
   Assumption.
Qed.

Lemma zmod_nx_0_n: (n:Z)(x:Z)(ZMod `n*x` `0` n).
Proof.
   Intros. Unfold ZMod.
   Split with x.
   Simpl. Reflexivity.
Qed.

Lemma zmoddivmin: (a,b:Z; n:Z)(ZMod a b n)<->(ZDivides n `a-b`).
Proof.
   Unfold ZMod 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 x.
   Reflexivity.

   (* <- *)
   Intros. Elim H. Intros.
   Split with x.
   Rewrite <- H0.
   Unfold Zminus.
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_sym.
   Rewrite Zplus_assoc_l.
   Rewrite Zplus_inverse_l.
   Simpl. Reflexivity.
Qed.

Lemma zmoddec: (a,b:Z)(n:Z)(ZMod a b n)\/~(ZMod a b n).
Proof.
   Intros.
   Elim (zmoddivmin a b n).
   Intros.
   Elim (zdivdec `a-b` n).
   Left.
   Apply H0.
   Assumption.
   Right.
   Intro.
   Elim H1.
   Apply H.
   Assumption.
Qed.

Lemma zmod_0not1: (n:Z)`n>1`->~(ZMod `0` `1` n).
Proof.
   Intros. Intro.
   Elim (mod_0not1 (absolu n)).
   Change (gt (absolu n) (absolu `1`)). Apply gtzgt.
   Apply Zlt_le_weak. Apply Zlt_trans with `1`.
   Unfold Zlt. Simpl. Reflexivity.
   Apply Zgt_lt. Assumption.
   Unfold Zle. Simpl. Discriminate.
   Assumption.
   Apply zmodmod. Assumption.
Qed.

Lemma zmod_exp1:
   (a:Z)(n:Z)(ZMod a `1` n) -> (m:nat)(ZMod (Exp a m) `1` n).
Proof.
   Intros a n H.
   Induction m.
   Simpl.
   Apply zmod_refl.
   Intros m1 IH.
   Simpl.
   Replace `1` with `1*1`.
   Apply zmod_mult_compat.
   Assumption.
   Apply IH.
   Simpl.
   Reflexivity.
Qed.

Lemma zmod_repr_non_0:
   (n:Z; x:Z)`0 < x < n`->~(ZMod x `0` n).
Proof.
   Intros.
   Intro.
   Elim H.
   Intros.
   Elim (mod_repr_non_0 (absolu n) x).
   Split.
   Assumption. Rewrite inj_abs_pos.
   Assumption. Apply Zle_ge. Apply Zle_trans with x.
   Apply Zlt_le_weak. Assumption.
   Apply Zlt_le_weak. Assumption.
   Apply zmodmod. Assumption.
Qed.