]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/common/theory.ma
arithmetics for λδ
[helm.git] / matita / matita / contribs / ng_assembly2 / common / theory.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/pts.ma".
24
25 (* ********************************** *)
26 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
27 (* ********************************** *)
28
29 (* logic/connectives.ma *)
30
31 ninductive True: Prop ≝
32  I : True.
33
34 ninductive False: Prop ≝.
35
36 ndefinition Not: Prop → Prop ≝
37 λA.(A → False).
38
39 interpretation "logical not" 'not x = (Not x).
40
41 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
42  #A; #C; #H;
43  nnormalize;
44  #H1;
45  nelim (H1 H).
46 nqed.
47
48 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
49  #A; #B; #H;
50  nnormalize;
51  #H1; #H2;
52  nelim (H1 (H H2)).
53 nqed.
54
55 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
56  #P; nnormalize; #H; #H1;
57  napply (H1 H).
58 nqed.
59
60 ninductive And2 (A,B:Prop) : Prop ≝
61  conj2 : A → B → (And2 A B).
62
63 interpretation "logical and" 'and x y = (And2 x y).
64
65 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
66  #A; #B; #H;
67  napply (And2_ind A B … H);
68  #H1; #H2;
69  napply H1.
70 nqed.
71
72 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
73  #A; #B; #H;
74  napply (And2_ind A B … H);
75  #H1; #H2;
76  napply H2.
77 nqed.
78
79 ninductive And3 (A,B,C:Prop) : Prop ≝
80  conj3 : A → B → C → (And3 A B C).
81
82 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
83  #A; #B; #C; #H;
84  napply (And3_ind A B C … H);
85  #H1; #H2; #H3;
86  napply H1.
87 nqed.
88
89 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
90  #A; #B; #C; #H;
91  napply (And3_ind A B C … H);
92  #H1; #H2; #H3;
93  napply H2.
94 nqed.
95
96 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
97  #A; #B; #C; #H;
98  napply (And3_ind A B C … H);
99  #H1; #H2; #H3;
100  napply H3.
101 nqed.
102
103 ninductive And4 (A,B,C,D:Prop) : Prop ≝
104  conj4 : A → B → C → D → (And4 A B C D).
105
106 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
107  #A; #B; #C; #D; #H;
108  napply (And4_ind A B C D … H);
109  #H1; #H2; #H3; #H4;
110  napply H1.
111 nqed.
112
113 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
114  #A; #B; #C; #D; #H;
115  napply (And4_ind A B C D … H);
116  #H1; #H2; #H3; #H4;
117  napply H2.
118 nqed.
119
120 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
121  #A; #B; #C; #D; #H;
122  napply (And4_ind A B C D … H);
123  #H1; #H2; #H3; #H4;
124  napply H3.
125 nqed.
126
127 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
128  #A; #B; #C; #D; #H;
129  napply (And4_ind A B C D … H);
130  #H1; #H2; #H3; #H4;
131  napply H4.
132 nqed.
133
134 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
135  conj5 : A → B → C → D → E → (And5 A B C D E).
136
137 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
138  #A; #B; #C; #D; #E; #H;
139  napply (And5_ind A B C D E … H);
140  #H1; #H2; #H3; #H4; #H5;
141  napply H1.
142 nqed.
143
144 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
145  #A; #B; #C; #D; #E; #H;
146  napply (And5_ind A B C D E … H);
147  #H1; #H2; #H3; #H4; #H5;
148  napply H2.
149 nqed.
150
151 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
152  #A; #B; #C; #D; #E; #H;
153  napply (And5_ind A B C D E … H);
154  #H1; #H2; #H3; #H4; #H5;
155  napply H3.
156 nqed.
157
158 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
159  #A; #B; #C; #D; #E; #H;
160  napply (And5_ind A B C D E … H);
161  #H1; #H2; #H3; #H4; #H5;
162  napply H4.
163 nqed.
164
165 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
166  #A; #B; #C; #D; #E; #H;
167  napply (And5_ind A B C D E … H);
168  #H1; #H2; #H3; #H4; #H5;
169  napply H5.
170 nqed.
171
172 ninductive Or2 (A,B:Prop) : Prop ≝
173   or2_intro1 : A → (Or2 A B)
174 | or2_intro2 : B → (Or2 A B).
175
176 interpretation "logical or" 'or x y = (Or2 x y).
177
178 ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
179
180 nlemma or2_elim
181  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
182  #P1; #P2; #Q; #H; #f1; #f2;
183  napply (Or2_ind P1 P2 ? f1 f2 ?);
184  napply H.
185 nqed.
186
187 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
188  #P1; #P2; #H;
189  napply (or2_elim P1 P2 ? H);
190  ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
191  ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
192  ##]
193 nqed.
194
195 ninductive Or3 (A,B,C:Prop) : Prop ≝
196   or3_intro1 : A → (Or3 A B C)
197 | or3_intro2 : B → (Or3 A B C)
198 | or3_intro3 : C → (Or3 A B C).
199
200 nlemma or3_elim
201  : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
202  #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
203  napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
204  napply H.
205 nqed.
206
207 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
208  #P1; #P2; #P3; #H;
209  napply (or3_elim P1 P2 P3 ? H);
210  ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
211  ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
212  ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
213  ##]
214 nqed.
215
216 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
217  #P1; #P2; #P3; #H;
218  napply (or3_elim P1 P2 P3 ? H);
219  ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
220  ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
221  ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
222  ##]
223 nqed.
224
225 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
226  #P1; #P2; #P3; #H;
227  napply (or3_elim P1 P2 P3 ? H);
228  ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
229  ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
230  ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
231  ##]
232 nqed.
233
234 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
235   or4_intro1 : A → (Or4 A B C D)
236 | or4_intro2 : B → (Or4 A B C D)
237 | or4_intro3 : C → (Or4 A B C D)
238 | or4_intro4 : D → (Or4 A B C D).
239
240 nlemma or4_elim
241  : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
242    ∀f3:P3 → Q.∀f4:P4 → Q.Q.
243  #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
244  napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
245  napply H.
246 nqed.
247
248 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
249  #P1; #P2; #P3; #P4; #H;
250  napply (or4_elim P1 P2 P3 P4 ? H);
251  ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
252  ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
253  ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
254  ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
255  ##]
256 nqed.
257
258 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
259  #P1; #P2; #P3; #P4; #H;
260  napply (or4_elim P1 P2 P3 P4 ? H);
261  ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
262  ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
263  ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
264  ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
265  ##]
266 nqed.
267
268 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
269  #P1; #P2; #P3; #P4; #H;
270  napply (or4_elim P1 P2 P3 P4 ? H);
271  ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
272  ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
273  ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
274  ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
275  ##]
276 nqed.
277
278 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
279  #P1; #P2; #P3; #P4; #H;
280  napply (or4_elim P1 P2 P3 P4 ? H);
281  ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
282  ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
283  ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
284  ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
285  ##]
286 nqed.
287
288 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
289  #P1; #P2; #P3; #P4; #H;
290  napply (or4_elim P1 P2 P3 P4 ? H);
291  ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
292  ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
293  ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
294  ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
295  ##]
296 nqed.
297
298 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
299  #P1; #P2; #P3; #P4; #H;
300  napply (or4_elim P1 P2 P3 P4 ? H);
301  ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
302  ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
303  ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
304  ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
305  ##]
306 nqed.
307
308 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
309   or5_intro1 : A → (Or5 A B C D E)
310 | or5_intro2 : B → (Or5 A B C D E)
311 | or5_intro3 : C → (Or5 A B C D E)
312 | or5_intro4 : D → (Or5 A B C D E)
313 | or5_intro5 : E → (Or5 A B C D E).
314
315 nlemma or5_elim
316  : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
317    ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
318  #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
319  napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
320  napply H.
321 nqed.
322
323 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
324  #P1; #P2; #P3; #P4; #P5; #H;
325  napply (or5_elim P1 P2 P3 P4 P5 ? H);
326  ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
327  ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
328  ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
329  ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
330  ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
331  ##]
332 nqed.
333
334 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
335  #P1; #P2; #P3; #P4; #P5; #H;
336  napply (or5_elim P1 P2 P3 P4 P5 ? H);
337  ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
338  ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
339  ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
340  ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
341  ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
342  ##]
343 nqed.
344
345 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
346  #P1; #P2; #P3; #P4; #P5; #H;
347  napply (or5_elim P1 P2 P3 P4 P5 ? H);
348  ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
349  ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
350  ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
351  ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
352  ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
353  ##]
354 nqed.
355
356 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
357  #P1; #P2; #P3; #P4; #P5; #H;
358  napply (or5_elim P1 P2 P3 P4 P5 ? H);
359  ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
360  ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
361  ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
362  ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
363  ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
364  ##]
365 nqed.
366
367 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
368  #P1; #P2; #P3; #P4; #P5; #H;
369  napply (or5_elim P1 P2 P3 P4 P5 ? H);
370  ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
371  ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
372  ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
373  ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
374  ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
375  ##]
376 nqed.
377
378 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
379  #P1; #P2; #P3; #P4; #P5; #H;
380  napply (or5_elim P1 P2 P3 P4 P5 ? H);
381  ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
382  ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
383  ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
384  ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
385  ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
386  ##]
387 nqed.
388
389 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
390  #P1; #P2; #P3; #P4; #P5; #H;
391  napply (or5_elim P1 P2 P3 P4 P5 ? H);
392  ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
393  ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
394  ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
395  ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
396  ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
397  ##]
398 nqed.
399
400 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
401  #P1; #P2; #P3; #P4; #P5; #H;
402  napply (or5_elim P1 P2 P3 P4 P5 ? H);
403  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
404  ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
405  ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
406  ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
407  ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
408  ##]
409 nqed.
410
411 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
412  #P1; #P2; #P3; #P4; #P5; #H;
413  napply (or5_elim P1 P2 P3 P4 P5 ? H);
414  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
415  ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
416  ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
417  ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
418  ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
419  ##]
420 nqed.
421
422 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
423  #P1; #P2; #P3; #P4; #P5; #H;
424  napply (or5_elim P1 P2 P3 P4 P5 ? H);
425  ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
426  ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
427  ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
428  ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
429  ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
430  ##]
431 nqed.
432
433 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
434  ex_intro: ∀x:A.Q x → ex A Q.
435
436 interpretation "exists" 'exists x = (ex ? x).
437
438 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
439  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
440
441 (* higher_order_defs/relations *)
442
443 ndefinition relation : Type → Type ≝
444 λA.A → A → Prop. 
445
446 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
447 λA.λR.∀x:A.R x x.
448
449 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
450 λA.λR.∀x,y:A.R x y → R y x.
451
452 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
453 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
454
455 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
456 λA.λR.∀x:A.¬ (R x x).
457
458 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
459 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
460
461 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
462 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
463
464 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
465 λA.λR.∀x,y:A.R x y → ¬ (R y x).
466
467 (* logic/equality.ma *)
468
469 ninductive eq (A:Type) (x:A) : A → Prop ≝
470  refl_eq : eq A x x.
471
472 ndefinition refl ≝ refl_eq.
473
474 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
475
476 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
477
478 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
479  #T1; #T2; #x; #y; #f; #H;
480  nrewrite < H;
481  napply refl_eq.
482 nqed.
483
484 nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
485  #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
486  nrewrite < H1;
487  nrewrite < H2;
488  napply refl_eq.
489 nqed.
490
491 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
492  #T1; #T2; #x; #y; #f;
493  nnormalize; #H; #H1;
494  napply (H (eq_f … H1)).
495 nqed.
496
497 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
498  #A;
499  nnormalize;
500  #x; #y; #H;
501  nrewrite < H;
502  napply refl_eq.
503 nqed.
504
505 nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
506  #A; #x; #P; #H; #y; #H1;
507  nrewrite < (symmetric_eq … H1);
508  napply H.
509 nqed.
510
511 ndefinition R0 ≝ λT:Type[0].λt:T.t.
512
513 ndefinition R1 ≝ eq_rect_Type0.
514
515 ndefinition R2 :
516   ∀T0:Type[0].
517   ∀a0:T0.
518   ∀T1:∀x0:T0. a0=x0 → Type[0].
519   ∀a1:T1 a0 (refl_eq ? a0).
520   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
521   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
522   ∀b0:T0.
523   ∀e0:a0 = b0.
524   ∀b1: T1 b0 e0.
525   ∀e1:R1 ?? T1 a1 ? e0 = b1.
526   T2 b0 e0 b1 e1.
527  #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
528  napply (eq_rect_Type0 ????? e1);
529  napply (R1 ?? ? ?? e0);
530  napply a2;
531 nqed.
532
533 ndefinition R3 :
534   ∀T0:Type[0].
535   ∀a0:T0.
536   ∀T1:∀x0:T0. a0=x0 → Type[0].
537   ∀a1:T1 a0 (refl_eq ? a0).
538   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
539   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
540   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
541       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
542   ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
543   ∀b0:T0.
544   ∀e0:a0 = b0.
545   ∀b1: T1 b0 e0.
546   ∀e1:R1 ?? T1 a1 ? e0 = b1.
547   ∀b2: T2 b0 e0 b1 e1.
548   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
549   T3 b0 e0 b1 e1 b2 e2.
550  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
551  napply (eq_rect_Type0 ????? e2);
552  napply (R2 ?? ? ???? e0 ? e1);
553  napply a3;
554 nqed.
555
556 ndefinition R4 :
557   ∀T0:Type[0].
558   ∀a0:T0.
559   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
560   ∀a1:T1 a0 (refl_eq T0 a0).
561   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
562   ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
563   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
564       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
565   ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
566       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2). 
567   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
568       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
569       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
570       Type[0].
571   ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
572       a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2) 
573       a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
574                    a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
575                    a3).
576   ∀b0:T0.
577   ∀e0:eq (T0 …) a0 b0.
578   ∀b1: T1 b0 e0.
579   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
580   ∀b2: T2 b0 e0 b1 e1.
581   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
582   ∀b3: T3 b0 e0 b1 e1 b2 e2.
583   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
584   T4 b0 e0 b1 e1 b2 e2 b3 e3.
585  #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
586  napply (eq_rect_Type0 ????? e3);
587  napply (R3 ????????? e0 ? e1 ? e2);
588  napply a4;
589 nqed.
590
591 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. 
592
593 nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
594  #T; #x; #y;
595  nnormalize;
596  #H; #H1;
597  nrewrite > H1 in H:(%); #H;
598  napply (H (refl_eq …)).
599 nqed.
600
601 ndefinition relationT : Type → Type → Type ≝
602 λA,T:Type.A → A → T.
603
604 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
605 λA,T.λR.∀x,y:A.R x y = R y x.
606
607 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
608 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).