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_2/relocation/rtmap_sor.ma".
16 include "basic_2/notation/relations/freestar_3.ma".
17 include "basic_2/syntax/lenv.ma".
19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
21 inductive frees: relation3 lenv term rtmap ≝
22 | frees_sort: ∀f,L,s. 𝐈⦃f⦄ → frees L (⋆s) f
23 | frees_atom: ∀f,i. 𝐈⦃f⦄ → frees (⋆) (#i) (↑*[i]⫯f)
24 | frees_pair: ∀f,I,L,V. frees L V f →
25 frees (L.ⓑ{I}V) (#0) (⫯f)
26 | frees_unit: ∀f,I,L. 𝐈⦃f⦄ → frees (L.ⓤ{I}) (#0) (⫯f)
27 | frees_lref: ∀f,I,L,i. frees L (#i) f →
28 frees (L.ⓘ{I}) (#⫯i) (↑f)
29 | frees_gref: ∀f,L,l. 𝐈⦃f⦄ → frees L (§l) f
30 | frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
31 f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{p,I}V.T) f
32 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
33 f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f
37 "context-sensitive free variables (term)"
38 'FreeStar L T f = (frees L T f).
40 (* Basic inversion lemmas ***************************************************)
42 fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
43 #L #X #f #H elim H -f -L -X //
44 [ #f #i #_ #x #H destruct
45 | #f #_ #L #V #_ #_ #x #H destruct
46 | #f #_ #L #_ #x #H destruct
47 | #f #_ #L #i #_ #_ #x #H destruct
48 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
49 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
53 lemma frees_inv_sort: ∀f,L,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
54 /2 width=5 by frees_inv_sort_aux/ qed-.
56 fact frees_inv_atom_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀i. L = ⋆ → X = #i →
57 ∃∃g. 𝐈⦃g⦄ & f = ↑*[i]⫯g.
58 #f #L #X #H elim H -f -L -X
59 [ #f #L #s #_ #j #_ #H destruct
60 | #f #i #Hf #j #_ #H destruct /2 width=3 by ex2_intro/
61 | #f #I #L #V #_ #_ #j #H destruct
62 | #f #I #L #_ #j #H destruct
63 | #f #I #L #i #_ #_ #j #H destruct
64 | #f #L #l #_ #j #_ #H destruct
65 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #j #_ #H destruct
66 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #j #_ #H destruct
70 lemma frees_inv_atom: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ↑*[i]⫯g.
71 /2 width=5 by frees_inv_atom_aux/ qed-.
73 fact frees_inv_pair_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
74 ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
76 [ #f #L #s #_ #Z #Y #X #_ #H destruct
77 | #f #i #_ #Z #Y #X #H destruct
78 | #f #I #L #V #Hf #Z #Y #X #H #_ destruct /2 width=3 by ex2_intro/
79 | #f #I #L #_ #Z #Y #X #H destruct
80 | #f #I #L #i #_ #Z #Y #X #_ #H destruct
81 | #f #L #l #_ #Z #Y #X #_ #H destruct
82 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #X #_ #H destruct
83 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #X #_ #H destruct
87 lemma frees_inv_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
88 /2 width=6 by frees_inv_pair_aux/ qed-.
90 fact frees_inv_unit_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K. L = K.ⓤ{I} → X = #0 →
93 [ #f #L #s #_ #Z #Y #_ #H destruct
94 | #f #i #_ #Z #Y #H destruct
95 | #f #I #L #V #_ #Z #Y #H destruct
96 | #f #I #L #Hf #Z #Y #H destruct /2 width=3 by ex2_intro/
97 | #f #I #L #i #_ #Z #Y #_ #H destruct
98 | #f #L #l #_ #Z #Y #_ #H destruct
99 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
100 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
104 lemma frees_inv_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
105 /2 width=7 by frees_inv_unit_aux/ qed-.
107 fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,j. L = K.ⓘ{I} → X = #(⫯j) →
108 ∃∃g. K ⊢ 𝐅*⦃#j⦄ ≡ g & f = ↑g.
110 [ #f #L #s #_ #Z #Y #j #_ #H destruct
111 | #f #i #_ #Z #Y #j #H destruct
112 | #f #I #L #V #_ #Z #Y #j #_ #H destruct
113 | #f #I #L #_ #Z #Y #j #_ #H destruct
114 | #f #I #L #i #Hf #Z #Y #j #H1 #H2 destruct /2 width=3 by ex2_intro/
115 | #f #L #l #_ #Z #Y #j #_ #H destruct
116 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
117 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
121 lemma frees_inv_lref: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
122 ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
123 /2 width=6 by frees_inv_lref_aux/ qed-.
125 fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
126 #f #L #X #H elim H -f -L -X //
127 [ #f #i #_ #x #H destruct
128 | #f #_ #L #V #_ #_ #x #H destruct
129 | #f #_ #L #_ #x #H destruct
130 | #f #_ #L #i #_ #_ #x #H destruct
131 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
132 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
136 lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅*⦃§l⦄ ≡ f → 𝐈⦃f⦄.
137 /2 width=5 by frees_inv_gref_aux/ qed-.
139 fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
140 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
142 [ #f #L #s #_ #q #J #W #U #H destruct
143 | #f #i #_ #q #J #W #U #H destruct
144 | #f #I #L #V #_ #q #J #W #U #H destruct
145 | #f #I #L #_ #q #J #W #U #H destruct
146 | #f #I #L #i #_ #q #J #W #U #H destruct
147 | #f #L #l #_ #q #J #W #U #H destruct
148 | #f1 #f2 #f #p #I #L #V #T #HV #HT #Hf #q #J #W #U #H destruct /2 width=5 by ex3_2_intro/
149 | #f1 #f2 #f #I #L #V #T #_ #_ #_ #q #J #W #U #H destruct
153 lemma frees_inv_bind: ∀f,p,I,L,V,T. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≡ f →
154 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
155 /2 width=4 by frees_inv_bind_aux/ qed-.
157 fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
158 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
160 [ #f #L #s #_ #J #W #U #H destruct
161 | #f #i #_ #J #W #U #H destruct
162 | #f #I #L #V #_ #J #W #U #H destruct
163 | #f #I #L #_ #J #W #U #H destruct
164 | #f #I #L #i #_ #J #W #U #H destruct
165 | #f #L #l #_ #J #W #U #H destruct
166 | #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #J #W #U #H destruct
167 | #f1 #f2 #f #I #L #V #T #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
171 lemma frees_inv_flat: ∀f,I,L,V,T. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
172 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
173 /2 width=4 by frees_inv_flat_aux/ qed-.
175 (* Advanced inversion lemmas ***********************************************)
177 lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f →
178 ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g.
179 #f #I #K #V #H elim (frees_inv_zero … H) -H *
181 | #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
182 | #g #Z #Y #_ #H destruct
186 lemma frees_inv_zero_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
187 #f #I #K #H elim (frees_inv_zero … H) -H *
189 | #g #Z #Y #X #_ #H destruct
190 | /2 width=3 by ex2_intro/
194 lemma frees_inv_lref_bind: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
195 ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
196 #f #I #K #i #H elim (frees_inv_lref … H) -H *
198 | #g #Z #Y #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/
202 (* Basic properties ********************************************************)
204 lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
205 #L #T #f1 #H elim H -f1 -L -T
206 [ /3 width=3 by frees_sort, isid_eq_repl_back/
208 elim (eq_inv_pushs_sn … H) -H #g #Hg #H destruct
209 elim (eq_inv_nx … Hg) -Hg
210 /3 width=3 by frees_atom, isid_eq_repl_back/
211 | #f1 #I #L #V #_ #IH #g2 #H
212 elim (eq_inv_nx … H) -H
213 /3 width=3 by frees_pair/
214 | #f1 #I #L #Hf1 #g2 #H
215 elim (eq_inv_nx … H) -H
216 /3 width=3 by frees_unit, isid_eq_repl_back/
217 | #f1 #I #L #i #_ #IH #g2 #H
218 elim (eq_inv_px … H) -H /3 width=3 by frees_lref/
219 | /3 width=3 by frees_gref, isid_eq_repl_back/
220 | /3 width=7 by frees_bind, sor_eq_repl_back3/
221 | /3 width=7 by frees_flat, sor_eq_repl_back3/
225 lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
226 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
229 (* Forward lemmas with test for finite colength *****************************)
231 lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
232 #f #L #T #H elim H -f -L -T
233 /4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
236 (* Basic_2A1: removed theorems 30:
237 frees_eq frees_be frees_inv
238 frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
239 frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
240 frees_inv_bind frees_inv_flat frees_inv_bind_O
241 frees_lref_eq frees_lref_be frees_weak
242 frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
243 frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
244 lreq_frees_trans frees_lreq_conf
245 llor_atom llor_skip llor_total
246 llor_tail_frees llor_tail_cofrees