]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/teqg.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / teqg.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/xoa/or_3.ma".
16 include "ground/xoa/ex_3_2.ma".
17 include "static_2/notation/relations/stareq_3.ma".
18 include "static_2/syntax/term.ma".
19
20 (* GENERIC EQUIVALENCE ON TERMS *********************************************)
21
22 inductive teqg (S:relation …): relation term ≝
23 | teqg_sort: ∀s1,s2. S s1 s2 → teqg S (⋆s1) (⋆s2)
24 | teqg_lref: ∀i. teqg S (#i) (#i)
25 | teqg_gref: ∀l. teqg S (§l) (§l)
26 | teqg_pair: ∀I,V1,V2,T1,T2. teqg S V1 V2 → teqg S T1 T2 → teqg S (②[I]V1.T1) (②[I]V2.T2)
27 .
28
29 interpretation
30   "context-free generic equivalence (term)"
31   'StarEq S T1 T2 = (teqg S T1 T2).
32
33 (* Basic properties *********************************************************)
34
35 lemma teqg_refl (S):
36       reflexive … S → reflexive … (teqg S).
37 #S #HS #T elim T -T /2 width=1 by teqg_pair/
38 * /2 width=1 by teqg_sort, teqg_lref, teqg_gref/
39 qed.
40
41 lemma teqg_sym (S):
42       symmetric … S → symmetric … (teqg S).
43 #S #HS #T1 #T2 #H elim H -T1 -T2
44 /3 width=3 by teqg_sort, teqg_lref, teqg_gref, teqg_pair/
45 qed-.
46
47 alias symbol "subseteq" (instance 3) = "relation inclusion".
48 lemma teqg_co (S1) (S2):
49       S1 ⊆ S2 →
50       ∀T1,T2. T1 ≛[S1] T2 → T1 ≛[S2] T2.
51 #S1 #S2 #HS #T1 #T2 #H elim H -T1 -T2
52 /3 width=1 by teqg_pair, teqg_sort/
53 qed-.
54
55 (* Basic inversion lemmas ***************************************************)
56
57 fact teqg_inv_sort1_aux (S):
58      ∀X,Y. X ≛[S] Y → ∀s1. X = ⋆s1 →
59      ∃∃s2. S s1 s2 & Y = ⋆s2.
60 #S #X #Y * -X -Y
61 [ #s1 #s2 #Hs12 #s #H destruct /2 width=3 by ex2_intro/
62 | #i #s #H destruct
63 | #l #s #H destruct
64 | #I #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
65 ]
66 qed-.
67
68 lemma teqg_inv_sort1 (S):
69       ∀Y,s1. ⋆s1 ≛[S] Y →
70       ∃∃s2. S s1 s2 & Y = ⋆s2.
71 /2 width=4 by teqg_inv_sort1_aux/ qed-.
72
73 fact teqg_inv_lref1_aux (S):
74      ∀X,Y. X ≛[S] Y → ∀i. X = #i → Y = #i.
75 #S #X #Y * -X -Y //
76 [ #s1 #s2 #_ #j #H destruct
77 | #I #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
78 ]
79 qed-.
80
81 lemma teqg_inv_lref1 (S):
82       ∀Y,i. #i ≛[S] Y → Y = #i.
83 /2 width=5 by teqg_inv_lref1_aux/ qed-.
84
85 fact teqg_inv_gref1_aux (S):
86      ∀X,Y. X ≛[S] Y → ∀l. X = §l → Y = §l.
87 #S #X #Y * -X -Y //
88 [ #s1 #s2 #_ #k #H destruct
89 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
90 ]
91 qed-.
92
93 lemma teqg_inv_gref1 (S):
94       ∀Y,l. §l ≛[S] Y → Y = §l.
95 /2 width=5 by teqg_inv_gref1_aux/ qed-.
96
97 fact teqg_inv_pair1_aux (S):
98      ∀X,Y. X ≛[S] Y → ∀I,V1,T1. X = ②[I]V1.T1 →
99      ∃∃V2,T2. V1 ≛[S] V2 & T1 ≛[S] T2 & Y = ②[I]V2.T2.
100 #S #X #Y * -X -Y
101 [ #s1 #s2 #_ #J #W1 #U1 #H destruct
102 | #i #J #W1 #U1 #H destruct
103 | #l #J #W1 #U1 #H destruct
104 | #I #V1 #V2 #T1 #T2 #HV #HT #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
105 ]
106 qed-.
107
108 lemma teqg_inv_pair1 (S):
109       ∀I,V1,T1,Y. ②[I]V1.T1 ≛[S] Y →
110       ∃∃V2,T2. V1 ≛[S] V2 & T1 ≛[S] T2 & Y = ②[I]V2.T2.
111 /2 width=3 by teqg_inv_pair1_aux/ qed-.
112
113 fact teqg_inv_sort2_aux (S):
114      ∀X,Y. X ≛[S] Y → ∀s2. Y = ⋆s2 →
115      ∃∃s1. S s1 s2 & X = ⋆s1.
116 #S #X #Y * -X -Y
117 [ #s1 #s2 #Hs12 #s #H destruct /2 width=3 by ex2_intro/
118 | #i #s #H destruct
119 | #l #s #H destruct
120 | #I #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
121 ]
122 qed-.
123
124 lemma teqg_inv_sort2 (S):
125       ∀X1,s2. X1 ≛[S] ⋆s2 →
126       ∃∃s1. S s1 s2 & X1 = ⋆s1.
127 /2 width=3 by teqg_inv_sort2_aux/ qed-.
128
129 fact teqg_inv_pair2_aux (S):
130      ∀X,Y. X ≛[S] Y → ∀I,V2,T2. Y = ②[I]V2.T2 →
131      ∃∃V1,T1. V1 ≛[S] V2 & T1 ≛[S] T2 & X = ②[I]V1.T1.
132 #S #X #Y * -X -Y
133 [ #s1 #s2 #_ #J #W2 #U2 #H destruct
134 | #i #J #W2 #U2 #H destruct
135 | #l #J #W2 #U2 #H destruct
136 | #I #V1 #V2 #T1 #T2 #HV #HT #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
137 ]
138 qed-.
139
140 lemma teqg_inv_pair2 (S):
141       ∀I,X1,V2,T2. X1 ≛[S] ②[I]V2.T2 →
142       ∃∃V1,T1. V1 ≛[S] V2 & T1 ≛[S] T2 & X1 = ②[I]V1.T1.
143 /2 width=3 by teqg_inv_pair2_aux/ qed-.
144
145 (* Advanced inversion lemmas ************************************************)
146
147 lemma teqg_inv_pair (S):
148       ∀I1,I2,V1,V2,T1,T2. ②[I1]V1.T1 ≛[S] ②[I2]V2.T2 →
149       ∧∧ I1 = I2 & V1 ≛[S] V2 & T1 ≛[S] T2.
150 #S #I1 #I2 #V1 #V2 #T1 #T2 #H elim (teqg_inv_pair1 … H) -H
151 #V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
152 qed-.
153
154 lemma teqg_inv_pair_xy_x (S):
155       ∀I,V,T. ②[I]V.T ≛[S] V → ⊥.
156 #S #I #V elim V -V
157 [ #J #T #H elim (teqg_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
158 | #J #X #Y #IHX #_ #T #H elim (teqg_inv_pair … H) -H #H #HY #_ destruct /2 width=2 by/
159 ]
160 qed-.
161
162 lemma teqg_inv_pair_xy_y (S):
163       ∀I,T,V. ②[I]V.T ≛[S] T → ⊥.
164 #S #I #T elim T -T
165 [ #J #V #H elim (teqg_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
166 | #J #X #Y #_ #IHY #V #H elim (teqg_inv_pair … H) -H #H #_ #HY destruct /2 width=2 by/
167 ]
168 qed-.
169
170 (* Basic forward lemmas *****************************************************)
171
172 lemma teqg_fwd_atom1 (S):
173       ∀I,Y. ⓪[I] ≛[S] Y → ∃J. Y = ⓪[J].
174 #S * #x #Y #H [ elim (teqg_inv_sort1 … H) -H ]
175 /3 width=4 by teqg_inv_gref1, teqg_inv_lref1, ex_intro/
176 qed-.
177
178 (* Advanced properties ******************************************************)
179
180 lemma teqg_dec (S):
181       (∀s1,s2. Decidable (S s1 s2)) →
182       ∀T1,T2. Decidable (T1 ≛[S] T2).
183 #S #HS #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
184 [ elim (HS s1 s2) -HS [ /3 width=1 by or_introl, teqg_sort/ ] #HS
185   @or_intror #H
186   elim (teqg_inv_sort1 … H) -H #x #Hx #H destruct /2 width=1 by/
187 |2,3,13:
188   @or_intror #H
189   elim (teqg_inv_sort1 … H) -H #x #_ #H destruct
190 |4,6,14:
191   @or_intror #H
192   lapply (teqg_inv_lref1 … H) -H #H destruct
193 |5:
194   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
195   @or_intror #H
196   lapply (teqg_inv_lref1 … H) -H #H destruct /2 width=1 by/
197 |7,8,15:
198   @or_intror #H
199   lapply (teqg_inv_gref1 … H) -H #H destruct
200 |9:
201   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
202   @or_intror #H
203   lapply (teqg_inv_gref1 … H) -H #H destruct /2 width=1 by/
204 |10,11,12:
205   @or_intror #H
206   elim (teqg_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
207 |16:
208   elim (eq_item2_dec I1 I2) #HI12 destruct
209   [ elim (IHV V2) -IHV #HV12
210     elim (IHT T2) -IHT #HT12
211     [ /3 width=1 by teqg_pair, or_introl/ ]
212   ]
213   @or_intror #H
214   elim (teqg_inv_pair … H) -H /2 width=1 by/
215 ]
216 qed-.
217
218 (* Negated inversion lemmas *************************************************)
219
220 lemma tneqg_inv_pair (S):
221       (∀s1,s2. Decidable (S s1 s2)) →
222       ∀I1,I2,V1,V2,T1,T2.
223       (②[I1]V1.T1 ≛[S] ②[I2]V2.T2 → ⊥) →
224       ∨∨ I1 = I2 → ⊥
225        | (V1 ≛[S] V2 → ⊥)
226        | (T1 ≛[S] T2 → ⊥).
227 #S #HS #I1 #I2 #V1 #V2 #T1 #T2 #H12
228 elim (eq_item2_dec I1 I2) /3 width=1 by or3_intro0/ #H destruct
229 elim (teqg_dec S … V1 V2) /3 width=1 by or3_intro1/
230 elim (teqg_dec S … T1 T2) /4 width=1 by teqg_pair, or3_intro2/
231 qed-.