Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 23d8bc68d7
March 09, 2008
file 174 lines (154 sloc) 2.897 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
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;

Something went wrong with that request. Please try again.