source: Deliverables/D4.1/Matita/Plogic/equality.ma @ 328

Last change on this file since 328 was 328, checked in by mulligan, 9 years ago

Got fold_right_i to type check. Moved eq_rect_Type0 into Plogic/equality.ma. Added new file for main processor execution loop.

File size: 5.7 KB
Line 
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
15include "Universes.ma".
16
17ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
18    refl: eq A x x.
19
20notation "hvbox(t⌈h ↦ o⌉)"
21  with precedence 45
22  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
23 
24interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
25
26nlemma eq_rect_r:
27 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl A a) → P x p.
28 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
29nqed.
30
31nlemma eq_ind_r :
32 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
34nqed.
35
36nlemma eq_rect_Type0_r :
37  ∀A: Type[0].
38  ∀a:A.
39  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
40  #A a P H x p.
41  ngeneralize in match H.
42  ngeneralize in match P.
43  ncases p.
44  //.
45nqed.
46
47nlemma eq_rect_Type2_r :
48  ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
49  #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P;
50  ncases p;//;
51nqed.
52
53(*
54nlemma eq_ind_r :
55 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
56 #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
57ncases p0; #Heq; nassumption.
58nqed.
59*)
60
61ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
62#A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
63nqed.
64
65ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
66#A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
67##[ @; ##| nassumption; ##]
68nqed.
69
70ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
71#A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
72nqed.
73
74ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
75#A; #B; #Ha; #Heq;nelim Heq; nassumption.
76nqed.
77
78ndefinition R0 ≝ λT:Type[0].λt:T.t.
79 
80ndefinition R1 ≝ eq_rect_Type0.
81
82ndefinition R2 :
83  ∀T0:Type[0].
84  ∀a0:T0.
85  ∀T1:∀x0:T0. a0=x0 → Type[0].
86  ∀a1:T1 a0 (refl ? a0).
87  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
88  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
89  ∀b0:T0.
90  ∀e0:a0 = b0.
91  ∀b1: T1 b0 e0.
92  ∀e1:R1 ?? T1 a1 ? e0 = b1.
93  T2 b0 e0 b1 e1.
94#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
95napply (eq_rect_Type0 ????? e1);
96napply (R1 ?? ? ?? e0);
97napply a2;
98nqed.
99
100ndefinition R3 :
101  ∀T0:Type[0].
102  ∀a0:T0.
103  ∀T1:∀x0:T0. a0=x0 → Type[0].
104  ∀a1:T1 a0 (refl ? a0).
105  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
106  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
107  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
108      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
109  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
110  ∀b0:T0.
111  ∀e0:a0 = b0.
112  ∀b1: T1 b0 e0.
113  ∀e1:R1 ?? T1 a1 ? e0 = b1.
114  ∀b2: T2 b0 e0 b1 e1.
115  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
116  T3 b0 e0 b1 e1 b2 e2.
117#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
118napply (eq_rect_Type0 ????? e2);
119napply (R2 ?? ? ???? e0 ? e1);
120napply a3;
121nqed.
122
123ndefinition R4 :
124  ∀T0:Type[0].
125  ∀a0:T0.
126  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
127  ∀a1:T1 a0 (refl T0 a0).
128  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
129  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
130  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
131      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
132  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
133      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
134  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
135      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
136      ∀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.
137      Type[0].
138  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
139      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
140      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
141                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
142                   a3).
143  ∀b0:T0.
144  ∀e0:eq (T0 …) a0 b0.
145  ∀b1: T1 b0 e0.
146  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
147  ∀b2: T2 b0 e0 b1 e1.
148  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
149  ∀b3: T3 b0 e0 b1 e1 b2 e2.
150  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
151  T4 b0 e0 b1 e1 b2 e2 b3 e3.
152#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
153napply (eq_rect_Type0 ????? e3);
154napply (R3 ????????? e0 ? e1 ? e2);
155napply a4;
156nqed.
157
158naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
Note: See TracBrowser for help on using the repository browser.