(**
 * divides.
 * The division predicate.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require ZArith.
Require Wf_nat.

Require lemmas.
Require natZ.
Require dec.
Require exp.

Definition Divides: nat -> nat -> Prop :=
   [n,m:nat](EX q:nat | m=(mult n q)).

Lemma div_refl: (a:nat)(Divides a a).
Proof.
   Intros. Split with (1).
   Rewrite <- mult_n_Sm.
   Rewrite <- mult_n_O.
   Simpl. Reflexivity.
Qed.

Lemma div_trans: (p,q,r:nat)(Divides p q)->(Divides q r)->(Divides p r).
Proof.
   Intros.
   Elim H.
   Elim H0.
   Intros.
   Unfold Divides.
   Split with (mult x0 x).
   Rewrite H1.
   Rewrite H2.
   Rewrite mult_assoc_l.
   Reflexivity.
Qed.

Lemma div_antisym: (a,b:nat)(Divides a b)->(Divides b a)->a=b.
Proof.
   Intros. Elim H. Elim H0. Intros x Ha y Hb.
   Rewrite Hb in Ha.
   Rewrite mult_assoc_r in Ha.
   Elim (mult_ppq_p0q1 a (mult y x)). Intro.
   Rewrite H1 in Hb.
   Simpl in Hb. Rewrite H1. Rewrite Hb. Reflexivity.
   Intros. Elim (mult_pq1_p1q1 y x H1).
   Intros.
   Rewrite H2 in Hb. Rewrite <- mult_n_Sm in Hb. Rewrite <- mult_n_O in Hb.
   Simpl in Hb. Symmetry. Assumption. Assumption.
Qed.

Lemma div_le1: (n,d:nat)(Divides d (S n))->(le d (S n)).
Proof.
   Unfold Divides.
   Intros.
   Elim H.
   Intro q.
   Case q.
   Rewrite <- (mult_n_O d).
   Intros.
   Discriminate H0.
   Intro q1.
   Intros.
   Rewrite H0.
   Apply le_n_nm.
Qed.

Lemma div_le: (d,n:nat)(lt O n)->(Divides d n)->(le d n).
Proof.
   Intros d n. Case n.
   Intro. Elim (lt_n_n O). Assumption.
   Intros. Apply div_le1. Assumption.
Qed.

(* Divides with bounded ex quantifier. *)

Definition bDivides :=
   [d,n:nat](n=O) \/ (EX q:nat | (lt q (S n)) /\ (n=(mult d q))).

Lemma divbdiv: (n,d:nat) (Divides d n) <-> (bDivides d n).
Proof.
   Unfold Divides.
   Unfold bDivides.
   Split.
   Case n.
   Left.
   Reflexivity.
   Right.
   Elim H.
   Intro q.
   Case d.
   Simpl.
   Intros.
   Discriminate H0.
   Intro d1.
   Intros.
   Split with q.
   Split.
   Rewrite H0.
   Unfold lt.
   Apply le_n_S.
   Apply le_n_mn.
   Assumption.
   Intros.
   Elim H.
   Intros.
   Rewrite H0.
   Split with O.
   Rewrite <- (mult_n_O d).
   Reflexivity.
   Elim H.
   Intros.
   Rewrite H0.
   Split with O.
   Rewrite <- (mult_n_O d).
   Reflexivity.
   Intros.
   Elim H0.
   Intros.
   Split with x.
   Elim H2.
   Intros.
   Assumption.
Qed.

(* Divides is decidable. *)

Lemma bdivdec: (n,d:nat) (bDivides d n) \/  ~(bDivides d n).
Proof.
   Intros. Unfold bDivides.
   Apply ordec.
   Apply eqdec.
   Apply (exdec [q:nat]n=(mult d q) (S n)).
   Intros. Apply eqdec.
Qed.

Lemma divdec: (n,d:nat) (Divides d n) \/  ~(Divides d n).
Proof.
   Intros. Elim (divbdiv n d).
   Intros. Elim (bdivdec n d).
   Left. Apply (H0 H1).
   Right. Intro. Apply H1. Apply (H H2).
Qed.

(* If d|n, then either d<sqrt(n) or the other divisor x<sqrt(n). *)

Theorem sqrdivbound:
   (n,d:nat)(Divides d n) ->
      (EX x:nat |
         (Divides x n) /\ (le (mult x x) n) /\ ((x=d) \/ (mult d x)=n)).
Proof.
   Intros.
   Unfold Divides in H.
   Elim H.
   Intros.
   Rewrite H0.
   Elim (sqrbound d x).
   Intros.
   Split with d.
   Split.
   Split with x.
   Reflexivity.
   Split.
   Assumption.
   Left.
   Reflexivity.
   Intros.
   Split with x.
   Split.
   Split with d.
   Apply mult_sym.
   Split.
   Assumption.
   Right.
   Reflexivity.
Qed.


(**
 * Division with remainder.
 *)

Theorem div_rem:
   (d,n:nat)(gt d O)->
      (EX q:nat | (EX r:nat | (le O r) /\ (lt r d) /\ n=(plus (mult q d) r))).
Proof.
   Intros d n.
   Apply (lt_wf_ind n). Intros N IH. Intros.
   Elim (le_or_lt d N).

   (* case d<=N *)
   Intro.
   Elim (le_witness d N). Intros x Hx.
   Elim (IH x). Intro q'. Intros. Elim H1. Intro r'. Intros.
   Elim H2. Intros. Elim H4. Intros.
   Split with (S q'). Split with r'.
   Split. Assumption.
   Split. Assumption.
   Simpl. Rewrite <- Hx. Rewrite (plus_assoc_r d (mult q' d)).
   Rewrite <- H6. Reflexivity.
   Unfold lt. Apply witness_le. Split with (pred d). Rewrite plus_Snm_nSm.
   Rewrite <- (S_pred d O). Rewrite plus_sym. Assumption. Assumption.
   Assumption.
   Assumption.

   (* case N<d *)
   Intro.
   Split with O. Split with N.
   Split. Apply le_O_n.
   Split. Assumption.
   Simpl. Reflexivity.
Qed.

Lemma div_rem0:
   (n,d,q,r:nat)n=(plus (mult q d) r)->(lt r d)->(Divides d n)->r=(0).
Proof.
   Intros.
   Elim H1.
   Intros.
   Rewrite H2 in H.
   Rewrite (mult_sym q d) in H.
   Apply (le_diff0 (mult d q) (mult d x)).
   Apply le_mult_l.
   Apply le_S_n.
   Change (lt x (S q)) .
   Apply simpl_lt_mult_l with d.
   Rewrite <- (mult_n_Sm d q).
   Replace (mult d x) with (plus (mult d q) r).
   Apply lt_reg_l.
   Assumption.
   Assumption.
Qed.

Theorem notdiv_rem:
   (d,n:nat)(lt O d) -> ~(Divides d n) ->
      (EX q:nat |  (EX r:nat | (lt O r) /\ (lt r d) /\ n=(plus (mult q d) r))).
Proof.
   Intros d n.
   Elim (le_or_lt d n).
   Intro.
   Elim (le_lt_or_eq d n).
   Apply (lt_wf_ind n).
   Intros N IH. Intros.
   Elim (lt_witness d N). Intros.
   Elim H3. Intros.
   Elim (le_or_lt d x).
   Intro.
   Elim (le_lt_or_eq d x).
   Intro.
   Elim (divdec x d).
   Intros.
   Elim H8.
   Intros.
   Rewrite H9 in H4.
   Rewrite plus_sym in H4.
   Rewrite mult_n_Sm in H4.
   Elim H2.
   Split with (S x0).
   Symmetry.
   Assumption.
   Intros.
   Elim (IH x).
   Intro q'.
   Intros.
   Elim H9.
   Intro r'.
   Intros.
   Elim H10.
   Intros.
   Elim H12.
   Intros.
   Split with (S q').
   Split with r'.
   Split.
   Assumption.
   Split.
   Assumption.
   Simpl.
   Rewrite plus_assoc_r.
   Rewrite <- H14.
   Symmetry.
   Assumption.
   Rewrite <- H4.
   Pattern 1 x.
   Replace x with (plus O x).
   Apply lt_reg_r.
   Assumption.
   Simpl.
   Reflexivity.
   Assumption.
   Assumption.
   Assumption.
   Intro.
   Elim H2.
   Split with (2).
   Rewrite mult_sym.
   Simpl.
   Rewrite <- (plus_n_O d).
   Rewrite <- H4.
   Rewrite H7.
   Reflexivity.
   Assumption.
   Intro.
   Split with (1).
   Split with x.
   Split.
   Assumption.
   Split.
   Assumption.
   Simpl.
   Rewrite <- (plus_n_O d).
   Rewrite H4.
   Reflexivity.
   Assumption.
   Intros.
   Elim H2.
   Split with (1).
   Rewrite mult_sym.
   Simpl.
   Rewrite <- (plus_n_O d).
   Symmetry.
   Assumption.
   Assumption.
   Case n.
   Intros.
   Elim H1.
   Split with O.
   Apply mult_n_O.
   Intro n1.
   Intros.
   Split with O.
   Split with (S n1).
   Split.
   Apply lt_O_Sn.
   Split.
   Assumption.
   Simpl. Reflexivity.
Qed.

(* Compatibility results. *)

Lemma div_plus_compat:
   (a,b,c:nat)(Divides a b)->(Divides a c) -> (Divides a (plus b c)).
Proof.
   Intros.
   Elim H. Intro x. Intros.
   Elim H0. Intro y. Intros.
   Split with (plus x y).
   Rewrite H1. Rewrite H2. Symmetry.
   Rewrite (mult_sym a). Rewrite (mult_sym a). Rewrite (mult_sym a).
   Apply mult_plus_distr.
Qed.

Lemma div_minus_compat:
   (a,b,d:nat)(Divides d a)->(Divides d b)->(Divides d (minus a b)).
Proof.
   Intros. Elim H. Elim H0. Intros.
   Unfold Divides. Rewrite H1. Rewrite H2.
   Rewrite (mult_sym d).
   Rewrite (mult_sym d).
   Rewrite <- mult_minus_distr.
   Split with (minus x0 x).
   Apply mult_sym.
Qed.

Lemma div_mult_compat_l:
   (a,b,c:nat)(Divides a b) -> (Divides a (mult b c)).
Proof.
   Intros.
   Elim H.
   Intro x.
   Intros.
   Unfold Divides.
   Rewrite H0.
   Split with (mult x c).
   Rewrite mult_assoc_l.
   Reflexivity.
Qed.

Lemma div_absexp_compat:
   (b:Z)(d:nat)(Divides d (absolu b))->
      (n:nat)(Divides d (absolu (Exp b (S n)))).
Proof.
   Intros b d H. Elim H. Intros k Hk. Induction n.
   Split with k.
   Rewrite <- Hk.
   Simpl.
   Rewrite abs_mult.
   Rewrite mult_sym.
   Simpl.
   Rewrite <- plus_n_O.
   Reflexivity.
   Intros m IH.
   Replace (Exp b (S (S m))) with `b*((Exp b) (S m))`.
   Rewrite abs_mult.
   Apply div_mult_compat_l.
   Assumption.
   Simpl. Reflexivity.
Qed.

Lemma div_plus_r:
   (a,b,d:nat)(Divides d a)->(Divides d (plus a b))->(Divides d b).
Proof.
   Intros. Elim H. Elim H0. Intros.
   Split with (minus x x0).
   Rewrite mult_sym.
   Rewrite mult_minus_distr.
   Rewrite mult_sym.
   Rewrite <- H1.
   Rewrite mult_sym.
   Rewrite <- H2.
   Rewrite minus_plus.
   Reflexivity.
Qed.

(* Division on Z. *)

Definition ZDivides: Z -> Z -> Prop :=
   [x,y:Z](EX q:Z | y=(Zmult x q)).

Lemma zdivdiv: (a,b:Z)(ZDivides a b)->(Divides (absolu a) (absolu b)).
Proof.
   Intros.
   Elim H.
   Intros d Hd.
   Exists (absolu d).
   Rewrite Hd.
   Apply abs_mult.
Qed.

Lemma divzdiv: (a,b:Z)(Divides (absolu a) (absolu b))->(ZDivides a b).
Proof.
   Intros.
   Elim H.
   Intros d Hd.
   Elim (Zle_or_lt `0` a).
   Elim (Zle_or_lt `0` b).

   (* case 0<=b, a<=b *)
   Intros.
   Exists (inject_nat d).
   Rewrite <- (inj_abs_pos b).
   Rewrite <- (inj_abs_pos a).
   Rewrite <- inj_mult.
   Rewrite Hd. Reflexivity.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Assumption.

   (* case b<0, 0<=a *)
   Intros.
   Exists (Zopp (inject_nat d)).
   Rewrite <- (Zopp_Zopp b).
   Rewrite <- (inj_abs_neg b).
   Rewrite <- (inj_abs_pos a).
   Rewrite Zmult_sym. Rewrite Zopp_Zmult. Rewrite Zmult_sym.
   Rewrite <- inj_mult.
   Apply (f_equal Z).
   Rewrite Hd.
   Reflexivity.
   Apply Zle_ge. Assumption.
   Assumption.

   Elim (Zle_or_lt `0` b).

   (* case 0<=b, a<0 *)
   Intros.
   Exists (Zopp (inject_nat d)).
   Rewrite <- (Zopp_Zopp a).
   Rewrite <- (inj_abs_neg a).
   Rewrite <- (inj_abs_pos b).
   Rewrite Zmult_Zopp_Zopp.
   Rewrite <- inj_mult.
   Rewrite Hd.
   Reflexivity.
   Apply Zle_ge. Assumption.
   Assumption.

   (* case b<0, a<0 *)
   Intros.
   Exists (inject_nat d).
   Rewrite <- (Zopp_Zopp b).
   Rewrite <- (Zopp_Zopp a).
   Rewrite <- (inj_abs_neg b).
   Rewrite <- (inj_abs_neg a).
   Rewrite Zopp_Zmult.
   Rewrite <- inj_mult.
   Apply (f_equal Z).
   Rewrite Hd.
   Reflexivity.
   Assumption.
   Assumption.
Qed.

Lemma zdivdec: (x,d:Z)(ZDivides d x)\/~(ZDivides d x). 
Proof.
   Intros.
   Elim (divdec (absolu x) (absolu d)).
   Left. Apply divzdiv. Assumption.
   Right. Intro. Apply H. Apply zdivdiv. Assumption.
Qed.

Lemma zdiv_plus_r:
   (a,b,d:Z)(ZDivides d a)->(ZDivides d `a+b`)->(ZDivides d b).
Proof.
   Intros.
   Elim H.
   Elim H0.
   Intros.
   Split with `x-x0`.
   Rewrite Zmult_sym.
   Rewrite Zmult_minus_distr.
   Rewrite Zmult_sym.
   Rewrite <- H1.
   Rewrite Zmult_sym.
   Rewrite <- H2.
   Rewrite Zminus_plus.
   Reflexivity.
Qed.

Lemma zdiv_plus_compat:
   (a,b,c:Z)(ZDivides a b)->(ZDivides a c) -> (ZDivides a `b+c`).
Proof.
   Intros.
   Elim H. Intro x. Intros.
   Elim H0. Intro y. Intros.
   Split with `x+y`.
   Rewrite H1. Rewrite H2. Symmetry.
   Rewrite (Zmult_sym a). Rewrite (Zmult_sym a). Rewrite (Zmult_sym a).
   Apply Zmult_plus_distr.
Qed.

Lemma zdiv_mult_compat_l:
   (a,b,c:Z)(ZDivides a b)->(ZDivides a `b*c`).
Proof.
   Intros.
   Elim H.
   Intro x.
   Intros.
   Unfold ZDivides.
   Rewrite H0.
   Split with `x*c`.
   Rewrite Zmult_assoc_l.
   Reflexivity.
Qed.

Theorem zdiv_rem:
   (d,n:Z)`d>0`->(EX q:Z | (EX r:Z | `0<=r<d` /\ `n=q*d+r`)).
Proof.
   Intros d n. Intro.
   Elim (Zle_or_lt `0` n).

   (* case 0<=n *)
   Intro. Rewrite <- (inj_abs_pos d). Rewrite <- (inj_abs_pos n).
   Elim (div_rem (absolu d) (absolu n)).
   Intro qn. Intros. Elim H1. Intro rn. Intros.
   Elim H2. Intros. Elim H4. Intros.
   Split with (inject_nat qn). Split with (inject_nat rn).
   Split. Split. Change `(inject_nat O) <= (inject_nat rn)`.
   Apply inj_le. Apply le_O_n.
   Apply inj_lt. Assumption.
   Rewrite <- inj_mult. Rewrite <- inj_plus. Apply inj_eq.
   Assumption. Change (gt (absolu d) (absolu `0`)). Apply gtzgt.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption. Apply Zle_refl. Reflexivity.
   Assumption. Apply Zle_ge. Assumption. Apply Zle_ge.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.

   (* case n<0 *)
   Intro. Rewrite <- (inj_abs_pos d).
   Replace n with `-(-n)`. Rewrite <- (inj_abs_neg n).
   Elim (div_rem (absolu d) (absolu n)).
   Intro qn. Intros. Elim H1. Intro rn. Intros.
   Elim H2. Intros. Elim H4. Intros.
   Elim (le_lt_or_eq O rn).

   (* case 0<rn *)
   Intro. Split with `-(inject_nat (S qn))`. Split with `d-(inject_nat rn)`.
   Split. Split. Rewrite <- (inj_abs_pos d). Apply Zle_minus. Apply inj_le.
   Apply lt_le_weak. Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Rewrite inj_abs_pos. Apply Zsimpl_lt_plus_l with (inject_nat rn).
   Unfold Zminus. Rewrite (Zplus_sym d).
   Rewrite (Zplus_assoc_l (inject_nat rn)).
   Rewrite Zplus_inverse_r. Simpl. Change `0+d < (inject_nat rn)+d`.
   Rewrite Zplus_sym. Rewrite (Zplus_sym (inject_nat rn)). Apply Zlt_reg_l.
   Change `(inject_nat O) < (inject_nat rn)`. Apply inj_lt. Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Rewrite inj_S. Unfold Zs. Rewrite Zopp_Zmult.
   Rewrite Zmult_plus_distr_l. Rewrite <- inj_mult. Rewrite Zmult_one.
   Rewrite (inj_abs_pos d). Rewrite Zopp_Zplus.
   Unfold Zminus. Rewrite Zplus_assoc_r. Rewrite (Zplus_assoc_l `-d`).
   Rewrite Zplus_inverse_l. Simpl. Rewrite <- Zopp_Zplus. Rewrite <- inj_plus.
   Rewrite <- H6. Reflexivity.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.

   (* case 0=rn *)
   Intro.
   Split with `-(inject_nat qn)`. Split with `0`.
   Split. Split. Unfold Zle. Simpl. Discriminate.
   Apply Zle_lt_trans with (inject_nat rn).
   Change `(inject_nat O) <= (inject_nat rn)`. Apply inj_le. Apply le_O_n.
   Apply inj_lt. Assumption.
   Rewrite <- Zplus_n_O. Rewrite inj_abs_neg.
   Rewrite Zopp_Zmult. Rewrite <- inj_mult.
   Rewrite <- H7 in H6. Rewrite <- plus_n_O in H6. Rewrite <- H6.
   Rewrite inj_abs_neg. Reflexivity.
   Assumption. Assumption. Assumption.
   Change (gt (absolu d) (absolu `0`)). Apply gtzgt. Apply Zlt_le_weak.
   Apply Zgt_lt. Assumption.
   Unfold Zle. Simpl. Discriminate.
   Assumption. Assumption.
   Apply Zopp_Zopp.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
Qed.