division.v

Require Export Coq.Init.Nat.


Print div.
Print modulo.
Print nat.
Print divmod.

Eval compute in (divmod 11 2 1 10).

Require Import Omega.

Theorem divmod_eq :
 forall x y q u a b, (a, b) = divmod x y q u -> x + q*(y+1) + b=a*(y+1)+u.
Proof.
induction x.
intros. simpl in H. inversion H.
rewrite Nat.add_0_l. reflexivity.
intros y q.
destruct u. simpl.
intros.
apply (IHx y (S q) y a b) in H.
simpl in H.
omega.
simpl.
intros.
apply IHx in H.
rewrite H. omega. Qed.

Check Nat.divmod_spec.

Theorem div_spec : forall x y, y>0 -> x = (x/y)*y + (x mod y).
Proof.
intros x.
destruct y.
intros. inversion H.
intros.
unfold div. unfold modulo.
remember (divmod x y 0 y) as c.
destruct c. simpl.
assert (let (n, n0) := (divmod x y 0 y) in x + S y * 0 + (y - y) = S y * n + (y - n0) /\ n0 <= y).
apply Nat.divmod_spec. reflexivity.
rewrite <- Heqc in H0.

simpl in H0. rewrite Nat.mul_0_r in H0.
rewrite Nat.sub_diag in H0. 
rewrite Nat.add_0_r in H0.
rewrite Nat.add_0_r in H0.
destruct H0.
rewrite H0.
rewrite Nat.mul_succ_r.
rewrite Nat.add_shuffle0.
rewrite Nat.add_comm.
rewrite Nat.add_assoc. rewrite Nat.mul_comm. reflexivity. Qed.