(* G54DTP Dependently Typed Programming.
    Divisibility relation, quotient and remainder. 
    Venanzio Capretta, March 2011.
*)

(* Inductive definition of the "less than" relation. *)

Inductive LessThan: nat -> nat -> Prop :=
  lt_O: forall m:nat, LessThan O m
| lt_S: forall n m: nat, LessThan n m -> LessThan (S n) (S m).

Lemma lt_4_7: LessThan 4 7.
Proof.
repeat (apply lt_S).
apply lt_O.
Qed.

Require Import Arith.

(* Order relations are already defined in the library
   in a slightly different way.
*)

Print le.  (* n<=m is notation for (le n m). *)
Print lt.  (* n<m  is notation for (lt n m). *)

(* Divisibility relation: uses the existential quantifier. *)

Definition Divides (x y:nat): Prop := exists k:nat, (y = k*x).

Lemma div7_21: Divides 7 21.
Proof.
exists 3.  (* "exists" is the tactic to prove an existential. *)
trivial.   (* "trivial" works for easy one-step goals. *)
Qed.

Theorem div_trans: forall x y z, Divides x y -> Divides y z -> Divides x z.
Proof.
intros x y z Hxy Hyz.
elim Hxy.
intros h Hy.
elim Hyz.
intros k Hz.
red.
exists (k*h).
rewrite Hz.
rewrite Hy.
rewrite mult_assoc.  (* "mult_assoc is defined in the library. *)
trivial.
Qed.

(* We want to define quotient and remainder.
   The following definition doesn't work:

 Fixpoint div (n m:nat): nat :=
 if (le_lt_dec m n)
   then S (div (n-m) m)
   else 0.

  It is rejected because it is not structurally recursive.
*)

(* First we define an inductive relation that characterises
   the pairs of arguments on which "div" works.
   "Dom_div n m" means that we can divide n by m.
*)

Inductive Dom_div: nat -> nat -> Set :=
  ddiv_lt: forall n m, n<m -> Dom_div n m
| ddiv_le: forall n m, m<=n -> Dom_div (n-m) m -> Dom_div n m.

(* ddiv_lt says that
     if n<m then we can divide n by m (the result will be 0).
   ddiv_le says that
     if n<m then we can divide n by m if we
       already know how to divide (n-m) by m.
*)

(* We can now define the division operation
   by giving it an extra argument:
   a proof that n can be divided by m.
   We can do recursion on this proof.
*)

Fixpoint div_aux (n m:nat)(h:Dom_div n m): nat :=
match h with
  ddiv_lt n m p => O
| ddiv_le n m q h => S (div_aux (n-m) m h)
end.

(* If m is at least 1, then we can always do the division. *)

Theorem dom_div_all : forall n m, 1<=m -> Dom_div n m.
intro n'.
Check lt_wf_rec.
apply (lt_wf_rec n' (fun n=>forall m : nat, 1 <= m -> Dom_div n m)).
intros n IH m Hm.
case (le_lt_dec m n).
intro Hle; apply ddiv_le.
exact Hle.
apply IH.
apply lt_minus.
exact Hle.
exact Hm.
exact Hm.
intro Hlt; apply ddiv_lt.
exact Hlt.
Defined.

(* The previous theorem always provides a proof of divisibility,
   so we can use that in place of the extra argument.
   (and we return 0 if m is 0.
*)

Definition div (n m:nat): nat :=
match (le_lt_dec 1 m) with
  left h => div_aux n m (dom_div_all n m h)
| right _ => 0
end.

Eval compute in (div 107 15).

(* In a similar way we can define the remainder of the division. *)

Fixpoint rem_aux (n m:nat)(h:Dom_div n m): nat :=
match h with
  ddiv_lt n m p => n
| ddiv_le n m q h => rem_aux (n-m) m h
end.

Definition rem (n m:nat): nat :=
match (le_lt_dec 1 m) with
  left h => rem_aux n m (dom_div_all n m h)
| right _ => n
end.

Eval compute in (rem 107 15).

(* And now some properties of quotient and remainder. *)

Lemma div_rem_aux: forall n m h, n = (div_aux n m h)*m + (rem_aux n m h).
Proof.
induction h; simpl.
trivial.
transitivity (m+(n-m)).
symmetry; apply le_plus_minus_r.
assumption.
rewrite IHh at 1.
apply plus_assoc.
Qed.

Theorem div_rem: forall n m, n = (div n m)*m + (rem n m).
Proof.
intros n m; unfold div; unfold rem.
case (le_lt_dec 1 m).
intro H1m; apply div_rem_aux.
trivial.
Qed.

Theorem rem0_divides: forall n m, rem n m = 0 -> Divides m n.
Proof.
intros n m H.
exists (div n m).
rewrite (div_rem n m) at 1.
rewrite H.
rewrite plus_0_r.
trivial.
Qed.

Lemma mult_lt: forall k m, k*m < m -> k=0.
Proof.
induction k; simpl.
trivial.
intros m Hm.
absurd (m<m).
apply lt_irrefl.
red.
red in Hm.
apply le_trans with (m := S (m+k*m)).
apply le_n_S;apply le_plus_l.
exact Hm.
Qed.

Lemma mult_minus: forall n m, n*m-m = (n-1)*m.
Proof.
induction n; simpl.
trivial.
intros m.
rewrite minus_plus.
rewrite <- minus_n_O.
trivial.
Qed.

Lemma rem_aux_eqmult_0:
  forall n m h, forall k, n=k*m -> rem_aux n m h = 0.
Proof.
intros n' m' h'; elim h'; simpl.
intros n m Hnm k Hk.
rewrite Hk in Hnm.
rewrite Hk.
rewrite (mult_lt k m Hnm).
trivial.

intros n m Hle h IH k Hk.
apply IH with (k:=k-1).
rewrite Hk.
rewrite mult_minus.
trivial.
Qed.

Lemma rem_aux_mult_O: forall m k h, rem_aux (k*m) m h = 0.
Proof.
intros m k h; apply rem_aux_eqmult_0 with (k:=k).
trivial.
Qed.

Lemma divides_remO: forall n m, Divides m n -> rem n m = 0.
Proof.
intros n m.
unfold rem; case (le_lt_dec 1 m).
intros p h; elim h; simpl.
apply rem_aux_eqmult_0.

intros Hm h; elim h.
intros k Hk.
cut (m=0).
intro H0; rewrite Hk; rewrite H0.
apply mult_0_r.
red in Hm.
symmetry.
apply le_n_O_eq.
apply le_S_n.
exact Hm.
Qed.