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