1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/xoa/ex_1_2.ma".
16 include "ground/xoa/ex_3_2.ma".
17 include "static_2/notation/relations/tildeminus_2.ma".
18 include "static_2/syntax/term_weight.ma".
20 (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
22 inductive teqw: relation term ≝
23 | teqw_sort: ∀s1,s2. teqw (⋆s1) (⋆s2)
24 | teqw_lref: ∀i. teqw (#i) (#i)
25 | teqw_gref: ∀l. teqw (§l) (§l)
26 | teqw_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→teqw T1 T2) → teqw (ⓓ[p]V1.T1) (ⓓ[p]V2.T2)
27 | teqw_abst: ∀p,V1,V2,T1,T2. teqw (ⓛ[p]V1.T1) (ⓛ[p]V2.T2)
28 | teqw_appl: ∀V1,V2,T1,T2. teqw T1 T2 → teqw (ⓐV1.T1) (ⓐV2.T2)
29 | teqw_cast: ∀V1,V2,T1,T2. teqw V1 V2 → teqw T1 T2 → teqw (ⓝV1.T1) (ⓝV2.T2)
33 "context-free tail sort-irrelevant equivalence (term)"
34 'TildeMinus T1 T2 = (teqw T1 T2).
36 (* Basic properties *********************************************************)
38 lemma teqw_abbr_pos: ∀V1,V2,T1,T2. T1 ≃ T2 → +ⓓV1.T1 ≃ +ⓓV2.T2.
39 /3 width=1 by teqw_abbr/ qed.
41 lemma teqw_abbr_neg: ∀V1,V2,T1,T2. -ⓓV1.T1 ≃ -ⓓV2.T2.
43 @teqw_abbr #H destruct
46 lemma teqw_refl: reflexive … teqw.
47 #T elim T -T * [||| #p * | * ]
48 /2 width=1 by teqw_sort, teqw_lref, teqw_gref, teqw_abbr, teqw_abst, teqw_appl, teqw_cast/
51 lemma teqw_sym: symmetric … teqw.
52 #T1 #T2 #H elim H -T1 -T2
53 /3 width=3 by teqw_sort, teqw_lref, teqw_gref, teqw_abbr, teqw_abst, teqw_appl, teqw_cast/
56 (* Left basic inversion lemmas **********************************************)
58 fact teqw_inv_sort_sn_aux:
59 ∀X,Y. X ≃ Y → ∀s1. X = ⋆s1 → ∃s2. Y = ⋆s2.
61 [1 : #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
62 |2,3: #i #s #H destruct
63 |4 : #p #V1 #V2 #T1 #T2 #_ #s #H destruct
64 |5 : #p #V1 #V2 #T1 #T2 #s #H destruct
65 |6 : #V1 #V2 #T1 #T2 #_ #s #H destruct
66 |7 : #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
70 lemma teqw_inv_sort_sn:
71 ∀Y,s1. ⋆s1 ≃ Y → ∃s2. Y = ⋆s2.
72 /2 width=4 by teqw_inv_sort_sn_aux/ qed-.
74 fact teqw_inv_lref_sn_aux:
75 ∀X,Y. X ≃ Y → ∀i. X = #i → Y = #i.
77 [1 : #s1 #s2 #j #H destruct
79 |4 : #p #V1 #V2 #T1 #T2 #_ #j #H destruct
80 |5 : #p #V1 #V2 #T1 #T2 #j #H destruct
81 |6 : #V1 #V2 #T1 #T2 #_ #j #H destruct
82 |7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
86 lemma teqw_inv_lref_sn: ∀Y,i. #i ≃ Y → Y = #i.
87 /2 width=5 by teqw_inv_lref_sn_aux/ qed-.
89 fact teqw_inv_gref_sn_aux:
90 ∀X,Y. X ≃ Y → ∀l. X = §l → Y = §l.
92 [1 : #s1 #s2 #k #H destruct
94 |4 : #p #V1 #V2 #T1 #T2 #_ #k #H destruct
95 |5 : #p #V1 #V2 #T1 #T2 #k #H destruct
96 |6 : #V1 #V2 #T1 #T2 #_ #k #H destruct
97 |7 : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
101 lemma teqw_inv_gref_sn:
102 ∀Y,l. §l ≃ Y → Y = §l.
103 /2 width=5 by teqw_inv_gref_sn_aux/ qed-.
105 fact teqw_inv_abbr_sn_aux:
106 ∀X,Y. X ≃ Y → ∀p,V1,T1. X = ⓓ[p]V1.T1 →
107 ∃∃V2,T2. p = Ⓣ → T1 ≃ T2 & Y = ⓓ[p]V2.T2.
109 [1 : #s1 #s2 #q #W1 #U1 #H destruct
110 |2,3: #i #q #W1 #U1 #H destruct
111 |4 : #p #V1 #V2 #T1 #T2 #HT #q #W1 #U1 #H destruct /3 width=4 by ex2_2_intro/
112 |5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct
113 |6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
114 |7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
118 lemma teqw_inv_abbr_sn:
119 ∀p,V1,T1,Y. ⓓ[p]V1.T1 ≃ Y →
120 ∃∃V2,T2. p = Ⓣ → T1 ≃ T2 & Y = ⓓ[p]V2.T2.
121 /2 width=4 by teqw_inv_abbr_sn_aux/ qed-.
123 fact teqw_inv_abst_sn_aux:
124 ∀X,Y. X ≃ Y → ∀p,V1,T1. X = ⓛ[p]V1.T1 →
125 ∃∃V2,T2. Y = ⓛ[p]V2.T2.
127 [1 : #s1 #s2 #q #W1 #U1 #H destruct
128 |2,3: #i #q #W1 #U1 #H destruct
129 |4 : #p #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
130 |5 : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
131 |6 : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
132 |7 : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
136 lemma teqw_inv_abst_sn:
137 ∀p,V1,T1,Y. ⓛ[p]V1.T1 ≃ Y →
138 ∃∃V2,T2. Y = ⓛ[p]V2.T2.
139 /2 width=5 by teqw_inv_abst_sn_aux/ qed-.
141 fact teqw_inv_appl_sn_aux:
142 ∀X,Y. X ≃ Y → ∀V1,T1. X = ⓐV1.T1 →
143 ∃∃V2,T2. T1 ≃ T2 & Y = ⓐV2.T2.
145 [1 : #s1 #s2 #W1 #U1 #H destruct
146 |2,3: #i #W1 #U1 #H destruct
147 |4 : #p #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct
148 |5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
149 |6 : #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct /2 width=4 by ex2_2_intro/
150 |7 : #V1 #V2 #T1 #T2 #_ #_ #W1 #U1 #H destruct
154 lemma teqw_inv_appl_sn:
155 ∀V1,T1,Y. ⓐV1.T1 ≃ Y →
156 ∃∃V2,T2. T1 ≃ T2 & Y = ⓐV2.T2.
157 /2 width=4 by teqw_inv_appl_sn_aux/ qed-.
159 fact teqw_inv_cast_sn_aux:
160 ∀X,Y. X ≃ Y → ∀V1,T1. X = ⓝV1.T1 →
161 ∃∃V2,T2. V1 ≃ V2 & T1 ≃ T2 & Y = ⓝV2.T2.
163 [1 : #s1 #s2 #W1 #U1 #H destruct
164 |2,3: #i #W1 #U1 #H destruct
165 |4 : #p #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
166 |5 : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
167 |6 : #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
168 |7 : #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
172 lemma teqw_inv_cast_sn:
173 ∀V1,T1,Y. ⓝV1.T1 ≃ Y →
174 ∃∃V2,T2. V1 ≃ V2 & T1 ≃ T2 & Y = ⓝV2.T2.
175 /2 width=3 by teqw_inv_cast_sn_aux/ qed-.
177 (* Advanced inversion lemmas ************************************************)
179 lemma teqw_inv_abbr_pos_sn:
180 ∀V1,T1,Y. +ⓓV1.T1 ≃ Y → ∃∃V2,T2. T1 ≃ T2 & Y = +ⓓV2.T2.
182 elim (teqw_inv_abbr_sn … H) -H #V2 #T2
183 /3 width=4 by ex2_2_intro/
186 lemma teqw_inv_abbr_neg_sn:
187 ∀V1,T1,Y. -ⓓV1.T1 ≃ Y → ∃∃V2,T2. Y = -ⓓV2.T2.
189 elim (teqw_inv_abbr_sn … H) -H #V2 #T2 #_
190 /2 width=3 by ex1_2_intro/
193 lemma teqw_inv_abbr_pos_bi:
194 ∀V1,V2,T1,T2. +ⓓV1.T1 ≃ +ⓓV2.T2 → T1 ≃ T2.
196 elim (teqw_inv_abbr_pos_sn … H) -H #W2 #U2 #HTU #H destruct //
199 lemma teqw_inv_appl_bi:
200 ∀V1,V2,T1,T2. ⓐV1.T1 ≃ ⓐV2.T2 → T1 ≃ T2.
202 elim (teqw_inv_appl_sn … H) -H #W2 #U2 #HTU #H destruct //
205 lemma teqw_inv_cast_bi:
206 ∀V1,V2,T1,T2. ⓝV1.T1 ≃ ⓝV2.T2 → ∧∧ V1 ≃ V2 & T1 ≃ T2.
208 elim (teqw_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
212 lemma teqw_inv_cast_xy_y: ∀T,V. ⓝV.T ≃ T → ⊥.
213 @(f_ind … tw) #n #IH #T #Hn #V #H destruct
214 elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
218 (* Advanced forward lemmas **************************************************)
220 lemma teqw_fwd_pair_sn (I):
221 ∀V1,T1,X2. ②[I]V1.T1 ≃ X2 → ∃∃V2,T2. X2 = ②[I]V2.T2.
222 * [ #p ] * [ cases p -p ] #V1 #T1 #X2 #H
223 [ elim (teqw_inv_abbr_pos_sn … H) -H #V2 #T2 #_ #H
224 | elim (teqw_inv_abbr_neg_sn … H) -H #V2 #T2 #H
225 | elim (teqw_inv_abst_sn … H) -H #V2 #T2 #H
226 | elim (teqw_inv_appl_sn … H) -H #V2 #T2 #_ #H
227 | elim (teqw_inv_cast_sn … H) -H #V2 #T2 #_ #_ #H
228 ] /2 width=3 by ex1_2_intro/
231 lemma teqw_fwd_pair_bi (I1) (I2):
232 ∀V1,V2,T1,T2. ②[I1]V1.T1 ≃ ②[I2]V2.T2 → I1 = I2.
233 #I1 #I2 #V1 #V2 #T1 #T2 #H
234 elim (teqw_fwd_pair_sn … H) -H #W2 #U2 #H destruct //
237 (* Advanced properties ******************************************************)
239 lemma teqw_dec: ∀T1,T2. Decidable (T1 ≃ T2).
240 #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
241 [ /3 width=1 by teqw_sort, or_introl/
244 elim (teqw_inv_sort_sn … H) -H #x #H destruct
247 lapply (teqw_inv_lref_sn … H) -H #H destruct
249 elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
251 lapply (teqw_inv_lref_sn … H) -H #H destruct /2 width=1 by/
254 lapply (teqw_inv_gref_sn … H) -H #H destruct
256 elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
258 lapply (teqw_inv_gref_sn … H) -H #H destruct /2 width=1 by/
261 elim (teqw_fwd_pair_sn … H) -H #X1 #X2 #H destruct
263 elim (eq_item2_dec I1 I2) #HI12 destruct
264 [ cases I2 -I2 [ #p ] * [ cases p -p ]
265 [ elim (IHT T2) -IHT #HT12
266 [ /3 width=1 by teqw_abbr_pos, or_introl/
267 | /4 width=3 by teqw_inv_abbr_pos_bi, or_intror/
269 | /3 width=1 by teqw_abbr_neg, or_introl/
270 | /3 width=1 by teqw_abst, or_introl/
271 | elim (IHT T2) -IHT #HT12
272 [ /3 width=1 by teqw_appl, or_introl/
273 | /4 width=3 by teqw_inv_appl_bi, or_intror/
275 | elim (IHV V2) -IHV #HV12
276 elim (IHT T2) -IHT #HT12
277 [1: /3 width=1 by teqw_cast, or_introl/
279 elim (teqw_inv_cast_bi … H) -H #HV12 #HT12
283 | /4 width=5 by teqw_fwd_pair_bi, or_intror/