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