(**
 * gcd.
 * Greatest common divisor.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require ZArith.
Require Wf_nat.

Require lemmas.
Require natZ.
Require divides.
Require mod.

(* Linear combinations. *)

Definition LinComb := [c,x,y:Z]
   (EX a:Z | (EX b:Z | `c=x*a+y*b`)).

Definition LinCombMod := [c,x,y:Z; n:nat]
   (EX a:Z | (EX b:Z | (Mod c `x*a+y*b` n))).

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

Lemma lincombmodzlincombmod:
   (c,x,y:Z)(n:nat)
      (LinCombMod c x y n)->(ZLinCombMod c x y (inject_nat n)).
Proof.
   Unfold LinCombMod ZLinCombMod.
   Intros. Elim H. Intros z Hz. Exists z.
   Elim Hz. Intros b Hb. Exists b.
   Apply modzmod. Assumption.
Qed.

Lemma zlincombmodlincombmod:
   (c,x,y:Z)(n:Z)
      (ZLinCombMod c x y n)->(LinCombMod c x y (absolu n)).
Proof.
   Unfold ZLinCombMod LinCombMod.
   Intros. Elim H. Intros a Ha. Exists a.
   Elim Ha. Intros b Hb. Exists b.
   Apply zmodmod. Assumption.
Qed.

(* Greatest common divisor. *)

Definition common_div := [x,y:Z; d:nat]
   (Divides d (absolu x))/\(Divides d (absolu y)).

Definition gcd := [x,y:Z; d:nat]
   (common_div x y d) /\ ((e:nat)(common_div x y e)->(le e d)).

Lemma gcd_unq: (d1,d2:nat)(x,y:Z)(gcd x y d1)->(gcd x y d2)->d1=d2.
Proof.
   Unfold gcd.
   Intros.
   Elim H.
   Elim H0.
   Intros.
   Apply le_antisym.
   Apply H2.
   Assumption.
   Apply H4.
   Assumption.
Qed.

Lemma gcd_sym: (d:nat; x,y:Z)(gcd x y d)->(gcd y x d).
Proof.
   Unfold gcd. Unfold common_div. Intros.
   Elim H. Intros. Elim H0. Intros.
   Split. Split.
   Assumption. Assumption.
   Intros.
   Elim H4. Intros. Apply H1. Split.
   Assumption. Assumption.
Qed.

Lemma gcd_opp_l: (d:nat; x,y:Z)(gcd x y d)->(gcd `-x` y d).
Proof.
   Unfold gcd. Unfold common_div. Intros.
   Elim H. Intros. Elim H0. Intros.
   Split.
   Split.
   Rewrite <- abs_opp.
   Assumption.
   Assumption.
   Intros.
   Elim H4. Intros.
   Apply H1. Split.
   Rewrite abs_opp.
   Assumption.
   Assumption.
Qed.

Lemma gcd_opp_r: (d:nat; x,y:Z)(gcd x y d)->(gcd x `-y` d).
Proof.
   Unfold gcd. Unfold common_div. Intros.
   Elim H. Intros. Elim H0. Intros.
   Split.
   Split.
   Assumption.
   Rewrite <- abs_opp.
   Assumption.
   Intros.
   Elim H4. Intros.
   Apply H1. Split.
   Assumption.
   Rewrite abs_opp.
   Assumption.
Qed.

Lemma gcd_0_l: (d:nat)(gt d O)->(gcd `0` (inject_nat d) d).
Proof.
   Unfold gcd. Unfold common_div.
   Split. Split.
   Split with O. Simpl. Rewrite <- mult_n_O. Reflexivity.
   Split with (1). Simpl. Rewrite <- mult_n_Sm.
   Rewrite <- mult_n_O. Simpl. Rewrite abs_inj. Reflexivity.
   Intros.
   Apply div_le.
   Assumption.
   Elim H0. Intros.
   Rewrite abs_inj in H2. Assumption.
Qed.

Lemma gcd_0_r: (d:nat)(gt d O)->(gcd (inject_nat d) `0` d).
Proof.
   Intros. Apply gcd_sym. Apply gcd_0_l. Assumption.
Qed.

(* Euclid's theorem. *)

Lemma euclid_gcd1:
   (d:nat; x,y:Z; q,r:Z)(gcd x y d)->`x=q*y+r`->(gcd r y d).
Proof.
   Unfold gcd. Unfold common_div. Intros.
   Elim H. Intros.
   Elim H1. Intros.
   Split.
   Split.
   Rewrite <- (abs_inj d). Apply zdivdiv.
   Apply zdiv_plus_r with `q*y`.
   Rewrite Zmult_sym. Apply zdiv_mult_compat_l.
   Apply divzdiv. Rewrite abs_inj. Assumption.
   Rewrite <- H0. Apply divzdiv. Rewrite abs_inj. Assumption.
   Assumption.
   Intros.
   Elim H5. Intros.
   Apply H2.
   Split.
   Rewrite <- (abs_inj e). Apply zdivdiv.
   Rewrite H0.
   Apply zdiv_plus_compat.
   Rewrite Zmult_sym. Apply zdiv_mult_compat_l.
   Apply divzdiv. Rewrite abs_inj.
   Assumption.
   Apply divzdiv. Rewrite abs_inj.
   Assumption.
   Assumption.
Qed.

Theorem euclid_gcd:
   (d1,d2:nat; x,y:Z; q,r:Z)`x=q*y+r`->(gcd x y d1)->(gcd r y d2)->d1=d2.
Proof.
   Intros.
   Apply (gcd_unq d1 d2 r y).
   Apply euclid_gcd1 with x q.
   Assumption.
   Assumption.
   Assumption.
Qed.

(* Greatest common divisor can be written as linear combination. *)

Lemma gcd_lincomb_nat:
   (x,y:nat)(d:nat)
      (gt x O)->
         (gcd (inject_nat x) (inject_nat y) d)->
            (LinComb (inject_nat d) (inject_nat x) (inject_nat y)).
Proof.
   Unfold LinComb. Intro x.
   Apply (lt_wf_ind x). Intros X IH. Intros.
   Elim (div_rem X y). Intro q. Intros. Elim H1.
   Intro r. Case r.

   (* case r = 0 *)
   Intros.
   Elim H2. Intros. Elim H4. Intros.
   Rewrite <- plus_n_O in H6.
   Split with `1`. Split with `0`.
   Rewrite <- Zmult_n_O. Rewrite <- Zplus_n_O.
   Rewrite Zmult_sym. Rewrite Zmult_one.
   Apply inj_eq.
   Apply (euclid_gcd d X (inject_nat y) (inject_nat X) (inject_nat q) `0`).
   Rewrite <- Zplus_n_O. Rewrite <- inj_mult. Apply inj_eq. Assumption.
   Apply gcd_sym. Assumption. Apply gcd_0_l. Assumption.

   (* case r > 0 *)
   Intro r1. Intros.
   Elim H2. Intros. Elim H4. Intros.
   Elim (IH (S r1) H5 X d).
   Intro delta. Intros. Elim H7. Intro gamma. Intros.
   Split with `gamma-(inject_nat q)*delta`. Split with delta.
   Rewrite H6. Rewrite H8.
   Unfold Zminus. Rewrite Zmult_plus_distr_r.
   Rewrite inj_plus. Rewrite Zmult_plus_distr_l.
   Rewrite inj_mult. Rewrite <- Zopp_Zmult.
   Rewrite (Zmult_assoc_l (inject_nat X)).
   Rewrite (Zmult_sym (inject_nat X) `-(inject_nat q)`).
   Rewrite Zopp_Zmult. Rewrite Zopp_Zmult.
   Rewrite (Zplus_assoc_r `(inject_nat X)*gamma`).
   Rewrite <- inj_mult.
   Rewrite (Zplus_assoc_l `-((inject_nat (mult q X))*delta)`). 
   Rewrite Zplus_inverse_l. Simpl. Apply Zplus_sym.
   Apply gt_Sn_O.
   Apply (euclid_gcd1 d (inject_nat y) (inject_nat X)
      (inject_nat q) (inject_nat (S r1))).
   Apply gcd_sym. Assumption.
   Rewrite <- inj_mult. Rewrite <- inj_plus. Apply inj_eq. Assumption.
   Assumption.
Qed.

Lemma gcd_lincomb_pos:
   (x,y:Z)(d:nat)
      `x>0`->(gcd x y d)->(LinComb (inject_nat d) x y).
Proof.
   Intros.
   Elim (Zle_or_lt `0` y).

   (* case 0 <= y *)
   Intro. Rewrite <- (inj_abs_pos x). Rewrite <- (inj_abs_pos y).
   Apply gcd_lincomb_nat.
   Change (gt (absolu x) (absolu `0`)).
   Apply gtzgt. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Unfold Zle. Simpl. Discriminate.
   Assumption.
   Rewrite inj_abs_pos. Rewrite inj_abs_pos. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.

   (* case y < 0 *)
   Intro. Rewrite <- (inj_abs_pos x).
   Replace y with `-(-y)`. Rewrite <- (inj_abs_neg y).
   Elim (gcd_lincomb_nat (absolu x) (absolu y) d).
   Intro alpha. Intros. Elim H2. Intro beta. Intros.
   Split with alpha. Split with `-beta`.
   Rewrite <- Zopp_Zmult_r. Rewrite (Zmult_sym `-(inject_nat (absolu y))`).
   Rewrite <- Zopp_Zmult_r. Rewrite Zopp_Zopp. Rewrite (Zmult_sym beta).
   Assumption.
   Change (gt (absolu x) (absolu `0`)). Apply gtzgt.
   Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Unfold Zle. Simpl. Discriminate.
   Assumption.
   Rewrite inj_abs_pos. Rewrite inj_abs_neg. Apply gcd_opp_r. Assumption.
   Assumption.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
   Assumption.
   Apply Zopp_Zopp.
   Apply Zle_ge. Apply Zlt_le_weak. Apply Zgt_lt. Assumption.
Qed.

Theorem gcd_lincomb:
   (x,y:Z)(d:nat)
      `x<>0`->(gcd x y d)->(LinComb (inject_nat d) x y).
Proof.
   Intros.
   Elim (Zle_or_lt `0` x).
   Intro.
   Elim (Zle_lt_or_eq `0` x).

   (* case 0 < x *)
   Intro.
   Apply gcd_lincomb_pos.
   Apply Zlt_gt.
   Assumption.
   Assumption.

   (* case 0 = x *)
   Intro.
   Elim H.
   Rewrite H2.
   Reflexivity.
   Assumption.

   (* case 0 > x *)
   Intro.
   Elim (gcd_lincomb_pos `-x` y d). Intro alpha. Intros.
   Elim H2. Intro beta. Intros.
   Split with `-alpha`. Split with beta.
   Rewrite H3.
   Rewrite (Zmult_sym x). Rewrite Zopp_Zmult. Rewrite Zopp_Zmult.
   Rewrite (Zmult_sym alpha). Reflexivity.
   Apply Zopp_lt_gt_0. Assumption. Apply gcd_opp_l. Assumption.
Qed.