(* Copyright (C) 2005-2008 Sebastien Briais *)
(* http://lamp.epfl.ch/~sbriais/ *)

(* This library is free software; you can redistribute it and/or modify *)
(* it under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation; either version 2.1 of the *)
(* License, or (at your option) any later version. *)

(* This library is distributed in the hope that it will be useful, but *)
(* WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *)
(* Lesser General Public License for more details. *)

(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)

Require Import missing.
Require Import Wf_nat.

(** b | a if there is q such that a = b * q*)
Definition divides (a b:nat) := exists q:nat,a = (b*q).

(** 1 divides every natural number *)
Lemma one_min_div : forall (n:nat),(divides n 1).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: not (divides (S O) a) *)
  red.
(* Goal: @ex nat (fun q : nat => @eq nat n (Init.Nat.mul (S O) q)) *)
  exists n.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  auto with arith.
Qed.

(** 0 is divides by every natural number *)
Lemma zero_max_div : forall (n:nat),(divides O n).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: not (divides (S O) a) *)
  red.
(* Goal: @ex nat (fun q : nat => @eq nat O (Init.Nat.mul n q)) *)
  exists O.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  auto with arith.
Qed.

(** the relation of divisibility is reflexive *)
Lemma divides_refl : forall (a:nat),(divides a a).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: not (divides (S O) a) *)
  red.
(* Goal: @ex nat (fun q : nat => @eq nat a (Init.Nat.mul a q)) *)
  exists 1.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  auto with arith.
Qed.

(** the relation of divisibility is transitive *)
Lemma divides_trans : forall (a b c:nat),(divides a b)->(divides b c)->(divides a c).
(* Goal: forall (d a b : nat) (_ : divides a d) (_ : divides b d), divides (Init.Nat.sub b a) d *)
  unfold divides.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H;intro q;intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H0;intro q';intro.
(* Goal: @eq nat a b *)
  rewrite H2 in H1.
(* Goal: @ex nat (fun q : nat => @eq nat a (Init.Nat.mul c q)) *)
  exists (q' * q).
(* Goal: @eq nat a (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  rewrite H1.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  auto with arith.
Qed.

(** the relation of divisibility is antisymmetric *)
Lemma divides_antisym : forall (a b:nat),(divides a b)->(divides b a)->a=b.
(* Goal: forall (d a b : nat) (_ : divides a d) (_ : divides b d), divides (Init.Nat.sub b a) d *)
  unfold divides.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H;intro q;intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H0;intro q';intro.
(* Goal: @eq nat a b *)
  rewrite H2 in H1.
(* Goal: @eq nat a b *)
  assert ((a = 0) \/ (q' * q)=1).
(* Goal: or (@eq nat a O) (@eq nat (Init.Nat.mul q' q) (S O)) *)
(* Goal: @eq nat a b *)
  apply mult_lemma4.
(* Goal: @eq nat a (Init.Nat.mul a (Init.Nat.mul q' q)) *)
(* Goal: @eq nat a b *)
  replace (a*(q'*q)) with (a*q'*q);try (auto with arith).
(* Goal: @eq nat a b *)
  case H3;intro.
(* Goal: @eq nat a b *)
(* Goal: @eq nat a b *)
  rewrite H4 in H2;simpl in H2;rewrite H2;trivial.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  elim (mult_lemma5 q' q H4);intros.
(* Goal: @eq nat a b *)
  rewrite H5 in H2;rewrite mult_comm in H2;simpl in H2;rewrite plus_comm in H2;simpl in H2;symmetry;trivial.
Qed.

(** corollary: forall a<>1, not(a | 1) *)
Lemma non_div_1 : forall (a:nat),(a<>1)->~(divides 1 a).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: not (divides (S O) a) *)
  red.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : divides m b), @sig nat (fun q : nat => @eq nat m (Init.Nat.mul b q))) (_ : divides n b), @sig nat (fun q : nat => @eq nat n (Init.Nat.mul b q)) *)
  intro.
(* Goal: False *)
  apply H.
(* Goal: @eq nat a (S O) *)
  apply divides_antisym;trivial.
(* Goal: divides a (S O) *)
  apply one_min_div.
Qed.

(** if d | a and d | b then d | (a+b) *)
Lemma divides_plus : forall (d a b:nat),(divides a d)->(divides b d)->(divides (plus a b) d).
(* Goal: forall (d a b : nat) (_ : divides a d) (_ : divides b d), divides (Init.Nat.sub b a) d *)
  unfold divides.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H;intro q;intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H0;intro q';intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.add a b) (Init.Nat.mul d q)) *)
  exists (q+q').
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  rewrite H1;rewrite H2.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) b) (Init.Nat.mul d (Init.Nat.mul b q)) *)
  ring.
Qed.

(** if d | a then d | a*b *)
Lemma divides_mult : forall (d a b:nat),(divides a d)->(divides (a*b) d).
(* Goal: forall (d a b : nat) (_ : divides a d) (_ : divides b d), divides (Init.Nat.sub b a) d *)
  unfold divides.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H;intro q;intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.mul a b) (Init.Nat.mul d q)) *)
  exists (b * q).
(* Goal: @eq nat (Init.Nat.mul a b) (Init.Nat.mul d (Init.Nat.mul b q)) *)
  rewrite H0.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul d q) b) (Init.Nat.mul d (Init.Nat.mul b q)) *)
  ring.
Qed.

(** if d | a and d | b then d | (b-a) *)
Lemma divides_minus : forall (d a b:nat),(divides a d)->(divides b d)->(divides (b-a) d).
(* Goal: forall (d a b : nat) (_ : divides a d) (_ : divides b d), divides (Init.Nat.sub b a) d *)
  unfold divides.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H;intro q;intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  elim H0;intro q';intro.
(* Goal: @ex nat (fun q : nat => @eq nat (Init.Nat.sub b a) (Init.Nat.mul d q)) *)
  rewrite H1;rewrite H2.
(* Goal: @ex nat (fun q0 : nat => @eq nat (Init.Nat.sub (Init.Nat.mul d q') (Init.Nat.mul d q)) (Init.Nat.mul d q0)) *)
  exists (q'-q).
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  rewrite (mult_comm d q');rewrite (mult_comm d q);rewrite (mult_comm d (q'-q));auto with arith.
Qed.

(** here we show that if b | a then it is possible to compute q such that a = b*q *)
Lemma quo_dec : forall (a b:nat),(divides a b)->{q:nat | a=b*q}.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @sig nat (fun q : nat => @eq nat a (Init.Nat.mul b q)) *)
  apply (lt_wf_rec a (fun x:nat => (divides x b)->{q:nat | x = b*q}));trivial.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : divides m b), @sig nat (fun q : nat => @eq nat m (Init.Nat.mul b q))) (_ : divides n b), @sig nat (fun q : nat => @eq nat n (Init.Nat.mul b q)) *)
  intro.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  case n;intros.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  exists 0;auto with arith.
(* Goal: @sig nat (fun q : nat => @eq nat (S n0) (Init.Nat.mul b q)) *)
  elim (H0 ((S n0)-b)).
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : divides m b), @sig nat (fun q : nat => @eq nat m (Init.Nat.mul b q))) (_ : divides n b), @sig nat (fun q : nat => @eq nat n (Init.Nat.mul b q)) *)
  intro q;intro.
(* Goal: @sig nat (fun q : nat => @eq nat (S n0) (Init.Nat.mul b q)) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  exists (S q).
(* Goal: @eq nat (S n0) (Init.Nat.mul b (S q)) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  replace (S n0) with (b+(S n0-b)).
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  rewrite p;rewrite plus_comm;auto with arith.
(* Goal: @eq nat (Init.Nat.add b (Init.Nat.sub (S n0) b)) (S n0) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  symmetry.
(* Goal: @eq nat (S n0) (Init.Nat.add b (Init.Nat.sub (S n0) b)) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  apply le_plus_minus.
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  elim H1;intros.
(* Goal: le b (S n0) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  rewrite H2.
(* Goal: le b (Init.Nat.mul b x) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  replace (b <= b*x) with (1*b <= b*x);rewrite (mult_comm b x).
(* Goal: le (Init.Nat.mul (S O) b) (Nat.mul x b) *)
(* Goal: @eq Prop (le (Init.Nat.mul (S O) b) (Nat.mul x b)) (le b (Nat.mul x b)) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  apply mult_le_compat_r.
(* Goal: le (S O) x *)
(* Goal: @eq Prop (le (Init.Nat.mul (S O) b) (Nat.mul x b)) (le b (Nat.mul x b)) *)
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  destruct x;[rewrite mult_comm in H2;discriminate | auto with arith].
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul c q') q) (Init.Nat.mul c (Init.Nat.mul q' q)) *)
  simpl;auto with arith.
(* Goal: lt (Init.Nat.sub (S n0) b) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  destruct b.
(* Goal: lt (Init.Nat.sub (S n0) O) (S n0) *)
(* Goal: lt (Init.Nat.sub (S n0) (S b)) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  elim H1;simpl;intros;discriminate.
(* Goal: lt (Init.Nat.sub (S n0) (S b)) (S n0) *)
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  omega.
(* Goal: divides (Init.Nat.sub (S n0) b) b *)
  apply (divides_minus b b (S n0));[apply divides_refl | trivial].
Qed.

(** we can now define the quotient of a by b in case of b | a *)
Definition quo (a b:nat) (H:(divides a b)) := let (q,_):=(quo_dec a b H) in q.

(** the quotient is the quotient! *)
Lemma quo_is_quo : forall (a b:nat)(H:divides a b),a=(mult b (quo a b H)).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: @eq nat a (Init.Nat.mul b (quo a b H)) *)
  unfold quo.
(* Goal: @eq nat a (Init.Nat.mul b (let (q, _) := quo_dec a b H in q)) *)
  generalize (quo_dec a b H);intro;elim s;trivial.
Qed.

(** if b | a then (n*a/b) = n*(a/b) *) 
Lemma quo_mult : forall (a b:nat)(H:divides a b),forall (n:nat),(b<>O)->(quo (a*n) b (divides_mult b a n H))=n*(quo a b H).
(* Goal: forall (a b : nat) (H : divides a b) (n : nat) (_ : not (@eq nat b O)), @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  intros.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : divides m b), @sig nat (fun q : nat => @eq nat m (Init.Nat.mul b q))) (_ : divides n b), @sig nat (fun q : nat => @eq nat n (Init.Nat.mul b q)) *)
  generalize (quo_is_quo (a*n) b (divides_mult b a n H));intro.
(* Goal: forall (n : nat) (_ : forall (m : nat) (_ : lt m n) (_ : divides m b), @sig nat (fun q : nat => @eq nat m (Init.Nat.mul b q))) (_ : divides n b), @sig nat (fun q : nat => @eq nat n (Init.Nat.mul b q)) *)
  generalize (quo_is_quo a b H);intro.
(* Goal: @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
  replace (a*n = b * quo (a * n) b (divides_mult b a n H)) with (b*(quo a b H)*n = b * quo (a * n) b (divides_mult b a n H)) in H1.
(* Goal: @eq nat (quo (Init.Nat.mul a n) b (divides_mult b a n H)) (Init.Nat.mul n (quo a b H)) *)
(* Goal: @eq Prop (@eq nat (Init.Nat.mul (Init.Nat.mul b (quo a b H)) n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) (@eq nat (Init.Nat.mul a n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) *)
  symmetry;rewrite mult_comm.
(* Goal: @eq nat (Nat.mul (quo a b H) n) (quo (Init.Nat.mul a n) b (divides_mult b a n H)) *)
(* Goal: @eq Prop (@eq nat (Init.Nat.mul (Init.Nat.mul b (quo a b H)) n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) (@eq nat (Init.Nat.mul a n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) *)
  apply mult_lemma6 with b;trivial.
(* Goal: @eq nat (Init.Nat.mul b (Nat.mul (quo a b H) n)) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H))) *)
(* Goal: @eq Prop (@eq nat (Init.Nat.mul (Init.Nat.mul b (quo a b H)) n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) (@eq nat (Init.Nat.mul a n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) *)
  rewrite mult_assoc;trivial.
(* Goal: @eq Prop (@eq nat (Init.Nat.mul (Init.Nat.mul b (quo a b H)) n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) (@eq nat (Init.Nat.mul a n) (Init.Nat.mul b (quo (Init.Nat.mul a n) b (divides_mult b a n H)))) *)
  rewrite <- H2;trivial.
Qed.

