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 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 universe constraint Type[0] < Type[1].
24 universe constraint Type[1] < Type[2].
25 universe constraint Type[2] < Type[3].
27 (* ********************************** *)
28 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
29 (* ********************************** *)
31 (* logic/connectives.ma *)
33 ninductive True: Prop ≝
36 ninductive False: Prop ≝.
38 ndefinition Not: Prop → Prop ≝
41 interpretation "logical not" 'not x = (Not x).
43 nlemma absurd : ∀A,C:Prop.A → ¬A → C.
50 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
57 nlemma prop_to_nnprop : ∀P.P → ¬¬P.
58 #P; nnormalize; #H; #H1;
62 ninductive And2 (A,B:Prop) : Prop ≝
63 conj2 : A → B → (And2 A B).
65 interpretation "logical and" 'and x y = (And2 x y).
67 nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
69 napply (And2_ind A B … H);
74 nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
76 napply (And2_ind A B … H);
81 ninductive And3 (A,B,C:Prop) : Prop ≝
82 conj3 : A → B → C → (And3 A B C).
84 nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
86 napply (And3_ind A B C … H);
91 nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
93 napply (And3_ind A B C … H);
98 nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
100 napply (And3_ind A B C … H);
105 ninductive And4 (A,B,C,D:Prop) : Prop ≝
106 conj4 : A → B → C → D → (And4 A B C D).
108 nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
110 napply (And4_ind A B C D … H);
115 nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
117 napply (And4_ind A B C D … H);
122 nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
124 napply (And4_ind A B C D … H);
129 nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
131 napply (And4_ind A B C D … H);
136 ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
137 conj5 : A → B → C → D → E → (And5 A B C D E).
139 nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
140 #A; #B; #C; #D; #E; #H;
141 napply (And5_ind A B C D E … H);
142 #H1; #H2; #H3; #H4; #H5;
146 nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
147 #A; #B; #C; #D; #E; #H;
148 napply (And5_ind A B C D E … H);
149 #H1; #H2; #H3; #H4; #H5;
153 nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
154 #A; #B; #C; #D; #E; #H;
155 napply (And5_ind A B C D E … H);
156 #H1; #H2; #H3; #H4; #H5;
160 nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
161 #A; #B; #C; #D; #E; #H;
162 napply (And5_ind A B C D E … H);
163 #H1; #H2; #H3; #H4; #H5;
167 nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
168 #A; #B; #C; #D; #E; #H;
169 napply (And5_ind A B C D E … H);
170 #H1; #H2; #H3; #H4; #H5;
174 ninductive Or2 (A,B:Prop) : Prop ≝
175 or2_intro1 : A → (Or2 A B)
176 | or2_intro2 : B → (Or2 A B).
178 interpretation "logical or" 'or x y = (Or2 x y).
180 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
183 : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
184 #P1; #P2; #Q; #H; #f1; #f2;
185 napply (Or2_ind P1 P2 ? f1 f2 ?);
189 nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
191 napply (or2_elim P1 P2 ? H);
192 ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
193 ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
197 ninductive Or3 (A,B,C:Prop) : Prop ≝
198 or3_intro1 : A → (Or3 A B C)
199 | or3_intro2 : B → (Or3 A B C)
200 | or3_intro3 : C → (Or3 A B C).
203 : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
204 #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
205 napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
209 nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
211 napply (or3_elim P1 P2 P3 ? H);
212 ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
213 ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
214 ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
218 nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
220 napply (or3_elim P1 P2 P3 ? H);
221 ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
222 ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
223 ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
227 nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
229 napply (or3_elim P1 P2 P3 ? H);
230 ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
231 ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
232 ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
236 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
237 or4_intro1 : A → (Or4 A B C D)
238 | or4_intro2 : B → (Or4 A B C D)
239 | or4_intro3 : C → (Or4 A B C D)
240 | or4_intro4 : D → (Or4 A B C D).
243 : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
244 ∀f3:P3 → Q.∀f4:P4 → Q.Q.
245 #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
246 napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
250 nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
251 #P1; #P2; #P3; #P4; #H;
252 napply (or4_elim P1 P2 P3 P4 ? H);
253 ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
254 ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
255 ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
256 ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
260 nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
261 #P1; #P2; #P3; #P4; #H;
262 napply (or4_elim P1 P2 P3 P4 ? H);
263 ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
264 ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
265 ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
266 ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
270 nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
271 #P1; #P2; #P3; #P4; #H;
272 napply (or4_elim P1 P2 P3 P4 ? H);
273 ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
274 ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
275 ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
276 ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
280 nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
281 #P1; #P2; #P3; #P4; #H;
282 napply (or4_elim P1 P2 P3 P4 ? H);
283 ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
284 ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
285 ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
286 ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
290 nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
291 #P1; #P2; #P3; #P4; #H;
292 napply (or4_elim P1 P2 P3 P4 ? H);
293 ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
294 ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
295 ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
296 ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
300 nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
301 #P1; #P2; #P3; #P4; #H;
302 napply (or4_elim P1 P2 P3 P4 ? H);
303 ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
304 ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
305 ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
306 ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
310 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
311 or5_intro1 : A → (Or5 A B C D E)
312 | or5_intro2 : B → (Or5 A B C D E)
313 | or5_intro3 : C → (Or5 A B C D E)
314 | or5_intro4 : D → (Or5 A B C D E)
315 | or5_intro5 : E → (Or5 A B C D E).
318 : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
319 ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
320 #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
321 napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
325 nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
326 #P1; #P2; #P3; #P4; #P5; #H;
327 napply (or5_elim P1 P2 P3 P4 P5 ? H);
328 ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
329 ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
330 ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
331 ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
332 ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
336 nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
337 #P1; #P2; #P3; #P4; #P5; #H;
338 napply (or5_elim P1 P2 P3 P4 P5 ? H);
339 ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
340 ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
341 ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
342 ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
343 ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
347 nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
348 #P1; #P2; #P3; #P4; #P5; #H;
349 napply (or5_elim P1 P2 P3 P4 P5 ? H);
350 ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
351 ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
352 ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
353 ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
354 ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
358 nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
359 #P1; #P2; #P3; #P4; #P5; #H;
360 napply (or5_elim P1 P2 P3 P4 P5 ? H);
361 ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
362 ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
363 ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
364 ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
365 ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
369 nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
370 #P1; #P2; #P3; #P4; #P5; #H;
371 napply (or5_elim P1 P2 P3 P4 P5 ? H);
372 ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
373 ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
374 ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
375 ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
376 ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
380 nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
381 #P1; #P2; #P3; #P4; #P5; #H;
382 napply (or5_elim P1 P2 P3 P4 P5 ? H);
383 ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
384 ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
385 ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
386 ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
387 ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
391 nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
392 #P1; #P2; #P3; #P4; #P5; #H;
393 napply (or5_elim P1 P2 P3 P4 P5 ? H);
394 ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
395 ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
396 ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
397 ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
398 ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
402 nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
403 #P1; #P2; #P3; #P4; #P5; #H;
404 napply (or5_elim P1 P2 P3 P4 P5 ? H);
405 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
406 ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
407 ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
408 ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
409 ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
413 nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
414 #P1; #P2; #P3; #P4; #P5; #H;
415 napply (or5_elim P1 P2 P3 P4 P5 ? H);
416 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
417 ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
418 ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
419 ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
420 ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
424 nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
425 #P1; #P2; #P3; #P4; #P5; #H;
426 napply (or5_elim P1 P2 P3 P4 P5 ? H);
427 ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
428 ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
429 ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
430 ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
431 ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
435 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
436 ex_intro: ∀x:A.Q x → ex A Q.
438 interpretation "exists" 'exists x = (ex ? x).
440 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
441 ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
444 λA,B.(A → B) ∧ (B → A).
446 (* higher_order_defs/relations *)
448 ndefinition relation : Type → Type ≝
449 λA:Type.A → A → Prop.
451 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
454 ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
455 λA.λR.∀x,y:A.R x y → R y x.
457 ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
458 λA.λR.∀x,y,z:A.R x y → R y z → R x z.
460 ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
461 λA.λR.∀x:A.¬ (R x x).
463 ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
464 λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
466 ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
467 λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
469 ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
470 λA.λR.∀x,y:A.R x y → ¬ (R y x).
472 (* logic/equality.ma *)
474 ninductive eq (A:Type) (x:A) : A → Prop ≝
477 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
479 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
481 nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
482 #T1; #T2; #x; #y; #f; #H;
487 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.
488 #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
494 nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
495 #T1; #T2; #x; #y; #f;
497 napply (H (eq_f … H1)).
500 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
508 nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
509 #A; #x; #P; #H; #y; #H1;
510 nrewrite < (symmetric_eq … H1);
514 nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
518 nrewrite > H1 in H:(%); #H;
519 napply (H (refl_eq …)).
522 ndefinition relationT : Type → Type → Type ≝
525 ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
526 λA,T.λR.∀x,y:A.R x y = R y x.
528 ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
529 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
531 (* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
533 ninductive peqv (A:Prop) (x:A) : A → Prop ≝
534 prefl_eqv : peqv A x x.
536 interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
540 notation > "hvbox(a break ≡ b)"
541 non associative with precedence 45
542 for @{ 'preqv ? $a $b }.
544 nlemma symmetric_peqv: ∀A:Prop. symmetric A (peqv A).
548 napply (peqv_ind A x (λ_.?) ? y H);
552 nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P y.
553 #A; #x; #P; #H; #y; #H1;
554 napply (peqv_ind A x (λ_.?) H y (symmetric_peqv … H1)).
557 naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
559 (* uso P x → P y, H e' P x
560 nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
561 nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));