1 inductive True: Prop \def
4 inductive False: Prop \def .
6 definition Not: Prop \to Prop \def
7 \lambda A:Prop. (A \to False).
9 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
10 intros.cut False.elim Hcut.apply H1.assumption.
13 inductive And (A,B:Prop) : Prop \def
14 conj : A \to B \to (And A B).
16 theorem proj1: \forall A,B:Prop. (And A B) \to A.
17 intros. elim H. assumption.
20 theorem proj2: \forall A,B:Prop. (And A B) \to A.
21 intros. elim H. assumption.
24 inductive Or (A,B:Prop) : Prop \def
25 or_introl : A \to (Or A B)
26 | or_intror : B \to (Or A B).
28 inductive ex (A:Type) (P:A \to Prop) : Prop \def
29 ex_intro: \forall x:A. P x \to ex A P.
31 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
32 ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
34 inductive eq (A:Type) (x:A) : A \to Prop \def
35 refl_equal : eq A x x.
37 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x.
38 intros. elim H. apply refl_equal.
41 theorem trans_eq : \forall A:Type.
42 \forall x,y,z:A. eq A x y \to eq A y z \to eq A x z.
43 intros.elim H1.assumption.
46 theorem f_equal: \forall A,B:Type.\forall f:A\to B.
47 \forall x,y:A. eq A x y \to eq B (f x) (f y).
48 intros.elim H.apply refl_equal.
51 theorem f_equal2: \forall A,B,C:Type.\forall f:A\to B \to C.
52 \forall x1,x2:A. \forall y1,y2:B.
53 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
54 intros.elim H1.elim H.apply refl_equal.
57 inductive nat : Set \def
61 definition pred: nat \to nat \def
62 \lambda n:nat. match n with
64 | (S u) \Rightarrow u ].
66 theorem pred_Sn : \forall n:nat.
67 (eq nat n (pred (S n))).
68 intros.apply refl_equal.
71 theorem injective_S : \forall n,m:nat.
72 (eq nat (S n) (S m)) \to (eq nat n m).
73 intros.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))).
74 apply f_equal. assumption.
77 theorem not_eq_S : \forall n,m:nat.
78 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
79 intros. simplify.intros.
80 apply H.apply injective_S.assumption.
83 definition not_zero : nat \to Prop \def
87 | (S p) \Rightarrow True ].
89 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
90 intros.simplify.intros.
91 cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H).
95 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
96 intros.elim n.apply O_S.apply not_eq_S.assumption.
100 definition plus : nat \to nat \to nat \def
101 let rec plus (n,m:nat) \def
104 | (S p) \Rightarrow S (plus p m) ]
108 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
109 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
112 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n m)) (plus n (S m)).
113 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
116 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
117 intros.elim n.simplify.apply plus_n_O.
118 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
122 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
123 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
126 definition times : nat \to nat \to nat \def
127 let rec times (n,m:nat) \def
130 | (S p) \Rightarrow (plus m (times p m)) ]
134 theorem times_n_O: \forall n:nat. eq nat O (times n O).
135 intros.elim n.simplify.apply refl_equal.simplify.assumption.
139 \forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)).
140 intros.elim n.simplify.apply refl_equal.
141 simplify.apply f_equal.elim H.
142 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
143 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
145 apply sym_plus.apply refl_equal.apply assoc_plus.
149 \forall n,m:nat. eq nat (times n m) (times m n).
150 intros.elim n.simplify.apply times_n_O.
151 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
154 definition minus : nat \to nat \to nat \def
155 let rec minus (n,m:nat) \def
156 [\lambda n:nat.nat] match n:nat with
159 [\lambda n:nat.nat] match m:nat with
161 | (S q) \Rightarrow minus p q ]]
166 \forall n:nat.\forall P:nat \to Prop.
167 P O \to (\forall m:nat. P (S m)) \to P n.
168 intros.elim n.assumption.apply H1.
171 theorem nat_double_ind :
172 \forall R:nat \to nat \to Prop.
173 (\forall n:nat. R O n) \to
174 (\forall n:nat. R (S n) O) \to
175 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
176 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
177 apply nat_case m1.apply H1.intros.apply H2. apply H3.
180 inductive bool : Set \def
184 definition notn : bool \to bool \def
187 [ true \Rightarrow false
188 | false \Rightarrow true ].
190 definition andb : bool \to bool \to bool\def
194 match b2 with [true \Rightarrow true | false \Rightarrow false]
195 | false \Rightarrow false ].
197 definition orb : bool \to bool \to bool\def
201 match b2 with [true \Rightarrow true | false \Rightarrow false]
202 | false \Rightarrow false ].
204 definition if_then_else : bool \to Prop \to Prop \to Prop \def
205 \lambda b:bool.\lambda P,Q:Prop.
208 | false \Rightarrow Q].
210 inductive le (n:nat) : nat \to Prop \def
212 | le_S : \forall m:nat. le n m \to le n (S m).
214 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
217 apply le_S.assumption.
220 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
222 apply le_n.apply le_S.assumption.
225 theorem le_O_n : \forall n:nat. le O n.
226 intros.elim n.apply le_n.apply le_S. assumption.
229 theorem le_n_Sn : \forall n:nat. le n (S n).
230 intros. apply le_S.apply le_n.
233 theorem le_pred_n : \forall n:nat. le (pred n) n.
234 intros.elim n.simplify.apply le_n.simplify.
238 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
239 intros.elim H.exact I.exact I.
242 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
243 intros.simplify.intros.apply not_zero_le ? O H.
246 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
247 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
248 elim n.apply refl_equal.apply False_ind.apply (le_Sn_O ? H2).
251 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
252 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
253 elim H.apply le_n.apply trans_le ? (pred x).assumption.
257 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
258 intros.elim n.apply le_Sn_O.simplify.intros.
259 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
262 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
263 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
264 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
266 apply le_n_O_eq.assumption.
267 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
268 intros.whd.intros.apply f_equal.apply H2.
269 apply le_S_n.assumption.
270 apply le_S_n.assumption.
273 definition leb : nat \to nat \to bool \def
274 let rec leb (n,m:nat) \def
275 [\lambda n:nat.bool] match n:nat with
278 [\lambda n:nat.bool] match m:nat with
279 [ O \Rightarrow false
280 | (S q) \Rightarrow leb p q]]
283 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
285 apply (nat_double_ind
286 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
287 simplify.intros.apply le_O_n.
288 simplify.exact le_Sn_O.
289 intros 2.simplify.elim (leb n1 m1).
290 simplify.apply le_n_S.apply H.
291 simplify.intros.apply H.apply le_S_n.assumption.
295 let three \def (S (S (S O))) in
296 let nine \def (times three three) in
297 let eightyone \def (times nine nine) in
298 let square \def (times eightyone eightyone) in
303 normalize goal at (? ? % ?).