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