]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/logic/equality.ma
- transcript: bugfix
[helm.git] / helm / software / matita / library / logic / equality.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 include "higher_order_defs/relations.ma".
16
17 inductive eq (A:Type) (x:A) : A \to Prop \def
18     refl_eq : eq A x x.
19
20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
21
22 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
23
24 theorem eq_rect':
25  \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.
26   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
27  intros.
28  exact
29   (match p1 return \lambda y. \lambda p.P y p with
30     [refl_eq \Rightarrow p]).
31 qed.
32  
33 variant reflexive_eq : \forall A:Type. reflexive A (eq A)
34 \def refl_eq.
35 (* simplify.intros.apply refl_eq. *)
36     
37 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
38 unfold symmetric.intros.elim H. apply refl_eq.
39 qed.
40
41 variant sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
42 \def symmetric_eq.
43
44 theorem transitive_eq : \forall A:Type. transitive A (eq A).
45 unfold transitive.intros.elim H1.assumption.
46 qed.
47
48 variant trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
49 \def transitive_eq.
50
51 theorem eq_elim_r:
52  \forall A:Type.\forall x:A. \forall P: A \to Prop.
53    P x \to \forall y:A. y=x \to P y.
54 intros. elim (sym_eq ? ? ? H1).assumption.
55 qed.
56
57 theorem eq_elim_r':
58  \forall A:Type.\forall x:A. \forall P: A \to Set.
59    P x \to \forall y:A. y=x \to P y.
60 intros. elim (sym_eq ? ? ? H).assumption.
61 qed.
62
63 theorem eq_elim_r'':
64  \forall A:Type.\forall x:A. \forall P: A \to Type.
65    P x \to \forall y:A. y=x \to P y.
66 intros. elim (sym_eq ? ? ? H).assumption.
67 qed.
68
69 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
70 \forall x,y:A. x=y \to f x = f y.
71 intros.elim H.apply refl_eq.
72 qed.
73
74 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
75 \forall x,y:A. x=y \to f y = f x.
76 intros.elim H.apply refl_eq.
77 qed.
78
79 (*  *)
80 coercion sym_eq.
81 coercion eq_f.
82 (* *)
83
84 default "equality"
85  cic:/matita/logic/equality/eq.ind
86  cic:/matita/logic/equality/sym_eq.con
87  cic:/matita/logic/equality/transitive_eq.con
88  cic:/matita/logic/equality/eq_ind.con
89  cic:/matita/logic/equality/eq_elim_r.con
90  cic:/matita/logic/equality/eq_rec.con
91  cic:/matita/logic/equality/eq_elim_r'.con
92  cic:/matita/logic/equality/eq_rect.con
93  cic:/matita/logic/equality/eq_elim_r''.con
94  cic:/matita/logic/equality/eq_f.con
95 (* *)
96  cic:/matita/logic/equality/eq_OF_eq.con.
97 (* *)
98 (*  
99  cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *)
100  *)
101  
102 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
103 \forall x1,x2:A. \forall y1,y2:B.
104 x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
105 intros.elim H1.elim H.reflexivity.
106 qed.
107
108 definition comp \def
109  \lambda A.
110   \lambda x,y,y':A.
111    \lambda eq1:x=y.
112     \lambda eq2:x=y'.
113      eq_ind ? ? (\lambda a.a=y') eq2 ? eq1.
114      
115 lemma trans_sym_eq:
116  \forall A.
117   \forall x,y:A.
118    \forall u:x=y.
119     comp ? ? ? ? u u = refl_eq ? y.
120  intros.
121  apply (eq_rect' ? ? ? ? ? u).
122  reflexivity.
123 qed.
124
125 definition nu \def
126  \lambda A.
127   \lambda H: \forall x,y:A. decidable (x=y).
128    \lambda x,y. \lambda p:x=y.
129      match H x y with
130       [ (or_introl p') \Rightarrow p'
131       | (or_intror K) \Rightarrow False_ind ? (K p) ].
132
133 theorem nu_constant:
134  \forall A.
135   \forall H: \forall x,y:A. decidable (x=y).
136    \forall x,y:A.
137     \forall u,v:x=y.
138      nu ? H ? ? u = nu ? H ? ? v.
139  intros.
140  unfold nu.
141  unfold decidable in H.
142  apply (Or_ind' ? ? ? ? ? (H x y)); simplify.
143   intro; reflexivity.
144   intro; elim (q u).
145 qed.
146
147 definition nu_inv \def
148  \lambda A.
149   \lambda H: \forall x,y:A. decidable (x=y).
150    \lambda x,y:A.
151     \lambda v:x=y.
152      comp ? ? ? ? (nu ? H ? ? (refl_eq ? x)) v.
153
154 theorem nu_left_inv:
155  \forall A.
156   \forall H: \forall x,y:A. decidable (x=y).
157    \forall x,y:A.
158     \forall u:x=y.
159      nu_inv ? H ? ? (nu ? H ? ? u) = u.
160  intros.
161  apply (eq_rect' ? ? ? ? ? u).
162  unfold nu_inv.
163  apply trans_sym_eq.
164 qed.
165
166 theorem eq_to_eq_to_eq_p_q:
167  \forall A. \forall x,y:A.
168   (\forall x,y:A. decidable (x=y)) \to
169    \forall p,q:x=y. p=q.
170  intros.
171  rewrite < (nu_left_inv ? H ? ? p).
172  rewrite < (nu_left_inv ? H ? ? q).
173  elim (nu_constant ? H ? ? q).
174  reflexivity.
175 qed.
176
177 (*CSC: alternative proof that does not pollute the environment with
178   technical lemmata. Unfortunately, it is a pain to do without proper
179   support for let-ins.
180 theorem eq_to_eq_to_eq_p_q:
181  \forall A. \forall x,y:A.
182   (\forall x,y:A. decidable (x=y)) \to
183    \forall p,q:x=y. p=q.
184 intros.
185 letin nu \def
186  (\lambda x,y. \lambda p:x=y.
187    match H x y with
188     [ (or_introl p') \Rightarrow p'
189     | (or_intror K) \Rightarrow False_ind ? (K p) ]).
190 cut
191  (\forall q:x=y.
192    eq_ind ? ? (\lambda z. z=y) (nu ? ? q) ? (nu ? ? (refl_eq ? x))
193    = q).
194 focus 8.
195  clear q; clear p.
196  intro.
197  apply (eq_rect' ? ? ? ? ? q);
198  fold simplify (nu ? ? (refl_eq ? x)).
199  generalize in match (nu ? ? (refl_eq ? x)); intro.
200  apply
201   (eq_rect' A x
202    (\lambda y. \lambda u.
203     eq_ind A x (\lambda a.a=y) u y u = refl_eq ? y)
204    ? x H1).
205  reflexivity.
206 unfocus.
207 rewrite < (Hcut p); fold simplify (nu ? ? p).
208 rewrite < (Hcut q); fold simplify (nu ? ? q).
209 apply (Or_ind' (x=x) (x \neq x)
210  (\lambda p:decidable (x=x). eq_ind A x (\lambda z.z=y) (nu x y p) x
211    ([\lambda H1.eq A x x]
212     match p with
213     [(or_introl p') \Rightarrow p'
214     |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))]) =
215    eq_ind A x (\lambda z.z=y) (nu x y q) x
216     ([\lambda H1.eq A x x]
217      match p with
218     [(or_introl p') \Rightarrow p'
219     |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))]))
220  ? ? (H x x)).
221 intro; simplify; reflexivity.
222 intro q; elim (q (refl_eq ? x)).
223 qed.
224 *)
225
226 (*
227 theorem a:\forall x.x=x\land True.
228
229 2:intros;
230   split;
231   [
232     exact (refl_eq Prop x);
233   |
234     exact I;
235   ]
236 1:
237   skip
238 ]
239 qed.
240 *)
241