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

Last change on this file since 327 was 268, checked in by sacerdot, 10 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 5.5 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_Type2_r :
37  ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
38  #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P;
39  ncases p;//;
40nqed.
41
42(*
43nlemma eq_ind_r :
44 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
45 #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
46ncases p0; #Heq; nassumption.
47nqed.
48*)
49
50ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
51#A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
52nqed.
53
54ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
55#A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
56##[ @; ##| nassumption; ##]
57nqed.
58
59ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
60#A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
61nqed.
62
63ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
64#A; #B; #Ha; #Heq;nelim Heq; nassumption.
65nqed.
66
67ndefinition R0 ≝ λT:Type[0].λt:T.t.
68 
69ndefinition R1 ≝ eq_rect_Type0.
70
71ndefinition R2 :
72  ∀T0:Type[0].
73  ∀a0:T0.
74  ∀T1:∀x0:T0. a0=x0 → Type[0].
75  ∀a1:T1 a0 (refl ? a0).
76  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
77  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
78  ∀b0:T0.
79  ∀e0:a0 = b0.
80  ∀b1: T1 b0 e0.
81  ∀e1:R1 ?? T1 a1 ? e0 = b1.
82  T2 b0 e0 b1 e1.
83#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
84napply (eq_rect_Type0 ????? e1);
85napply (R1 ?? ? ?? e0);
86napply a2;
87nqed.
88
89ndefinition R3 :
90  ∀T0:Type[0].
91  ∀a0:T0.
92  ∀T1:∀x0:T0. a0=x0 → Type[0].
93  ∀a1:T1 a0 (refl ? a0).
94  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
95  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
96  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
97      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
98  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
99  ∀b0:T0.
100  ∀e0:a0 = b0.
101  ∀b1: T1 b0 e0.
102  ∀e1:R1 ?? T1 a1 ? e0 = b1.
103  ∀b2: T2 b0 e0 b1 e1.
104  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
105  T3 b0 e0 b1 e1 b2 e2.
106#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
107napply (eq_rect_Type0 ????? e2);
108napply (R2 ?? ? ???? e0 ? e1);
109napply a3;
110nqed.
111
112ndefinition R4 :
113  ∀T0:Type[0].
114  ∀a0:T0.
115  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
116  ∀a1:T1 a0 (refl T0 a0).
117  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
118  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
119  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
120      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
121  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
122      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
123  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
124      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
125      ∀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.
126      Type[0].
127  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
128      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
129      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
130                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
131                   a3).
132  ∀b0:T0.
133  ∀e0:eq (T0 …) a0 b0.
134  ∀b1: T1 b0 e0.
135  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
136  ∀b2: T2 b0 e0 b1 e1.
137  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
138  ∀b3: T3 b0 e0 b1 e1 b2 e2.
139  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
140  T4 b0 e0 b1 e1 b2 e2 b3 e3.
141#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
142napply (eq_rect_Type0 ????? e3);
143napply (R3 ????????? e0 ? e1 ? e2);
144napply a4;
145nqed.
146
147naxiom 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.