ivor-0.1.5: lib/nat.tt

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

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

Match plus : Nat->Nat->Nat =
   plus O y = y
 | plus (S k) y = S (plus k y);

Match mult : Nat->Nat->Nat =
   mult O y = O
 | mult (S k) y = plus y (mult k y);

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

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

eq_resp_S:(n,m:_)(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,m:_)(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:_)(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:_)(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:_)(q:Eq _ _ O (S k))A;
intros;
local false:False;
fill notO_S k q;
induction false;
Qed;
Freeze discriminate_Nat;

plusnO:(n:_)(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,m:_)(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,m:_)(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:_)(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:_)(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:_)(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;
intros;
fill plus_eq_fst m n p q;
Qed;
Freeze plus_eq_fst_sym;

multnO:(n:_)(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,m:_)(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;