1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 inductive True: Prop \def
19 inductive False: Prop \def .
21 definition Not: Prop \to Prop \def
22 \lambda A. (A \to False).
24 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
28 inductive And (A,B:Prop) : Prop \def
29 conj : A \to B \to (And A B).
31 theorem proj1: \forall A,B:Prop. (And A B) \to A.
32 intros. elim H. assumption.
35 theorem proj2: \forall A,B:Prop. (And A B) \to A.
36 intros. elim H. assumption.
39 inductive Or (A,B:Prop) : Prop \def
40 or_introl : A \to (Or A B)
41 | or_intror : B \to (Or A B).
43 inductive ex (A:Type) (P:A \to Prop) : Prop \def
44 ex_intro: \forall x:A. P x \to ex A P.
46 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
47 ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
49 inductive eq (A:Type) (x:A) : A \to Prop \def
50 refl_equal : eq A x x.
52 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x.
53 intros. elim H. apply refl_equal.
56 theorem trans_eq : \forall A:Type.
57 \forall x,y,z:A. eq A x y \to eq A y z \to eq A x z.
58 intros.elim H1.assumption.
61 theorem f_equal: \forall A,B:Type.\forall f:A\to B.
62 \forall x,y:A. eq A x y \to eq B (f x) (f y).
63 intros.elim H.apply refl_equal.
66 theorem f_equal2: \forall A,B,C:Type.\forall f:A\to B \to C.
67 \forall x1,x2:A. \forall y1,y2:B.
68 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
69 intros.elim H1.elim H.apply refl_equal.
72 inductive nat : Set \def
76 definition pred: nat \to nat \def
77 \lambda n:nat. match n with
79 | (S u) \Rightarrow u ].
81 theorem pred_Sn : \forall n:nat.
82 (eq nat n (pred (S n))).
83 intros.apply refl_equal.
86 theorem injective_S : \forall n,m:nat.
87 (eq nat (S n) (S m)) \to (eq nat n m).
88 intros.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))).
89 apply f_equal. assumption.
92 theorem not_eq_S : \forall n,m:nat.
93 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
94 intros. simplify.intros.
95 apply H.apply injective_S.assumption.
98 definition not_zero : nat \to Prop \def
101 [ O \Rightarrow False
102 | (S p) \Rightarrow True ].
104 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
105 intros.simplify.intros.
106 cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H).
110 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
111 intros.elim n.apply O_S.apply not_eq_S.assumption.
115 let rec plus n m \def
118 | (S p) \Rightarrow S (plus p m) ].
120 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
121 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
124 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n m)) (plus n (S m)).
125 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
128 theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
129 intros.elim n.simplify.apply plus_n_O.
130 simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm.
134 \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)).
135 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
138 let rec times n m \def
141 | (S p) \Rightarrow (plus m (times p m)) ].
143 theorem times_n_O: \forall n:nat. eq nat O (times n O).
144 intros.elim n.simplify.apply refl_equal.simplify.assumption.
148 \forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)).
149 intros.elim n.simplify.apply refl_equal.
150 simplify.apply f_equal.elim H.
151 apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq.
152 apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)).
154 apply sym_plus.apply refl_equal.apply assoc_plus.
158 \forall n,m:nat. eq nat (times n m) (times m n).
159 intros.elim n.simplify.apply times_n_O.
160 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
163 let rec minus n m \def
169 | (S q) \Rightarrow minus p q ]].
172 \forall n:nat.\forall P:nat \to Prop.
173 P O \to (\forall m:nat. P (S m)) \to P n.
174 intros.elim n.assumption.apply H1.
177 theorem nat_double_ind :
178 \forall R:nat \to nat \to Prop.
179 (\forall n:nat. R O n) \to
180 (\forall n:nat. R (S n) O) \to
181 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
182 intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H.
183 apply nat_case m1.apply H1.intros.apply H2. apply H3.
186 inductive bool : Set \def
190 definition notn : bool \to bool \def
193 [ true \Rightarrow false
194 | false \Rightarrow true ].
196 definition andb : bool \to bool \to bool\def
200 match b2 with [true \Rightarrow true | false \Rightarrow false]
201 | false \Rightarrow false ].
203 definition orb : bool \to bool \to bool\def
207 match b2 with [true \Rightarrow true | false \Rightarrow false]
208 | false \Rightarrow false ].
210 definition if_then_else : bool \to Prop \to Prop \to Prop \def
211 \lambda b:bool.\lambda P,Q:Prop.
214 | false \Rightarrow Q].
216 inductive le (n:nat) : nat \to Prop \def
218 | le_S : \forall m:nat. le n m \to le n (S m).
220 theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p.
223 apply le_S.assumption.
226 theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m).
228 apply le_n.apply le_S.assumption.
231 theorem le_O_n : \forall n:nat. le O n.
232 intros.elim n.apply le_n.apply le_S. assumption.
235 theorem le_n_Sn : \forall n:nat. le n (S n).
236 intros. apply le_S.apply le_n.
239 theorem le_pred_n : \forall n:nat. le (pred n) n.
240 intros.elim n.simplify.apply le_n.simplify.
244 theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m.
245 intros.elim H.exact I.exact I.
248 theorem le_Sn_O: \forall n:nat. Not (le (S n) O).
249 intros.simplify.intros.apply not_zero_le ? O H.
252 theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n).
253 intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption.
254 elim n.apply refl_equal.apply False_ind.apply (le_Sn_O ? H2).
257 theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m.
258 intros.cut le (pred (S n)) (pred (S m)).exact Hcut.
259 elim H.apply le_n.apply trans_le ? (pred x).assumption.
263 theorem le_Sn_n : \forall n:nat. Not (le (S n) n).
264 intros.elim n.apply le_Sn_O.simplify.intros.
265 cut le (S e) e.apply H.assumption.apply le_S_n.assumption.
268 theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m).
269 intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1.
270 apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
272 apply le_n_O_eq.assumption.
273 intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption.
274 intros.whd.intros.apply f_equal.apply H2.
275 apply le_S_n.assumption.
276 apply le_S_n.assumption.
284 [ O \Rightarrow false
285 | (S q) \Rightarrow leb p q]].
287 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
289 apply (nat_double_ind
290 (\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
291 simplify.intros.apply le_O_n.
292 simplify.exact le_Sn_O.
293 intros 2.simplify.elim (leb n1 m1).
294 simplify.apply le_n_S.apply H.
295 simplify.intros.apply H.apply le_S_n.assumption.
298 (*CSC: this requires too much time
300 let three \def (S (S (S O))) in
301 let nine \def (times three three) in
302 let eightyone \def (times nine nine) in
303 let square \def (times eightyone eightyone) in
308 normalize goal at (? ? % ?).