source: Deliverables/D4.1/Matita/Equality.ma @ 246

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

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

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