Load "eq.tt";
Load "logic.tt";

Data Nat:* where 
   O:Nat 
 | S:(k:Nat)Nat;

plus : Nat -> Nat -> Nat;
intro m;
induction m;
intros;
fill X0;
intros;
fill S (k_IH X1);
Qed;

mult : (m:Nat) -> (n:Nat) -> Nat;
intro m;
induction m;
intros;
fill O;
intros;
fill (plus n0 (k_IH n0));
Qed;

simplifyO:(n:Nat)(Eq _ (plus O n) n);
intros;
refine refl;
Qed;

simplifyS:(m,n:Nat)(Eq _ (plus (S m) n) (S (plus m n)));
intros;
refine refl;
Qed;

eq_resp_S:(n:Nat)(m:Nat)(q:Eq _ n m)(Eq _ (S n) (S m));
intros;
fill (eq_resp_f _ _ S n m q);
Qed;
Freeze eq_resp_S;

s_injective:(n:Nat)(m:Nat)(q:Eq _ (S n) (S m))(Eq _ n m);
intros;
local unS:(m:Nat)Nat;
intros;
induction m0;
fill n;
intros;
fill k;
fill eq_resp_f _ _ unS _ _ q;
Qed;
Freeze s_injective;

notO_S:(k:Nat)(not (Eq _ O (S k)));
intros;
compute;
intro q;
local dmotive : (x:Nat)(q:Eq _ O x)*;
intros;
induction x;
fill True;
intros;
fill False;
fill EqElim _ _ _ q dmotive II;
Qed;
Freeze notO_S;

notn_S:(n:Nat)(not (Eq _ n (S n)));
intro;
induction n;
fill notO_S O;
intros;
unfold not;
intros;
claim q:Eq _ k (S k);
fill k_IH q;
refine s_injective;
fill a;
Qed;
Freeze notn_S;

discriminate_Nat:(A:*)(k:Nat)(q:Eq _ O (S k))A;
intros;
local false:False;
fill notO_S k q;
induction false;
Qed;
Freeze discriminate_Nat;

plusnO:(n:Nat)(Eq _ (plus n O) n);
intro;
induction n;
refine refl;
intros;
equiv Eq _ (S (plus k O)) (S k);
refine eq_resp_S;
fill k_IH;
Qed;
Freeze plusnO;

plusnSm:(n:Nat)(m:Nat)(Eq _ (plus n (S m)) (S (plus n m)));
intros;
induction n;
refine refl;
intros;
refine eq_resp_S;
fill k_IH;
Qed;
Freeze plusnSm;

plus_comm:(n:Nat)(m:Nat)(Eq _ (plus n m) (plus m n));
intros;
induction n;
refine sym;
refine plusnO;
intros;
equiv Eq _ (S (plus k m)) (plus m (S k));
replace k_IH;
refine sym;
refine plusnSm;
Qed;
Freeze plus_comm;

plus_assoc:(m,n,p:Nat)(Eq _ (plus m (plus n p)) (plus (plus m n) p));
intros;
induction m;
refine refl;
intros;
equiv Eq _ (S (plus k (plus n p))) (plus (S (plus k n)) p);
replace k_IH;
refine refl;
Qed;
Freeze plus_assoc;

plus_eq_fst : (m,n,p:Nat)(q:Eq _ (plus p m) (plus p n))(Eq _ m n);
intro m n p;
induction p;
intros;
fill q;
intros;
refine k_IH;
refine s_injective;
refine q0;
Qed;
Freeze plus_eq_fst;

plus_eq_fst_sym : (m,n,p:Nat)(q:Eq _ (plus m p) (plus n p))(Eq _ m n);
intro m n p;
replace plus_comm m p;
replace plus_comm n p;
fill plus_eq_fst m n p;
Qed;
Freeze plus_eq_fst_sym;

multnO:(n:Nat)(Eq _ (mult n O) O);
intro;
induction n;
refine refl;
intros;
equiv Eq _ (plus O (mult k O)) O;
replace k_IH;
refine refl;
Qed;
Freeze multnO;

multnSm:(n:Nat)(m:Nat)(Eq _ (mult n (S m)) (plus n (mult n m)));
intro;
induction n;
intros;
refine refl;
intros;
equiv Eq _ (S (plus m0 (mult k (S m0))))
             (S (plus k (plus m0 (mult k m0))));
refine eq_resp_S;
replace (k_IH m0);
generalise mult k m0;
intros;
replace (plus_comm m0 x);
replace (plus_assoc k x m0);
replace (plus_comm m0 (plus k x));
refine refl;
Qed;
Freeze multnSm;

mult_comm : (m,n:Nat) -> (Eq _ (mult m n) (mult n m));
intro m;
induction m;
intros;
replace (multnO n);
refine refl;
intros;
replace (multnSm n0 k);
replace sym (k_IH n0);
refine refl;
Qed;
Freeze mult_comm;

mult_distrib:(m,n,p:Nat)(Eq _ (plus (mult m p) (mult n p))
                              (mult (plus m n) p));
intros;
induction m;
refine refl;
intros;
equiv Eq _ (plus (plus p (mult k p)) (mult n p))
           (plus p (mult (plus k n) p));
replace sym k_IH;
generalise mult k p;
generalise mult n p;
intro x y;
replace plus_assoc p y x;
refine refl;
Qed;

mult_assoc:(m,n,p:Nat)(Eq _ (mult m (mult n p)) (mult (mult m n) p));
intro m;
induction m;
intros;
compute;
refine refl;
intros;
equiv Eq _ (plus (mult n0 p0) (mult k (mult n0 p0)))
           (mult (plus n0 (mult k n0)) p0);
replace k_IH n0 p0;
generalise mult k n0;
intros;
replace mult_distrib n0 x p0;
refine refl;
Qed;