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 โ
91 โโg. ๐โฆgโฆ & f = โg.
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 (* Basic properties ********************************************************)
177 lemma frees_eq_repl_back: โL,T. eq_repl_back โฆ (ฮปf. L โข ๐
*โฆTโฆ โ f).
178 #L #T #f1 #H elim H -f1 -L -T
179 [ /3 width=3 by frees_sort, isid_eq_repl_back/
181 elim (eq_inv_pushs_sn โฆ H) -H #g #Hg #H destruct
182 elim (eq_inv_nx โฆ Hg) -Hg
183 /3 width=3 by frees_atom, isid_eq_repl_back/
184 | #f1 #I #L #V #_ #IH #g2 #H
185 elim (eq_inv_nx โฆ H) -H
186 /3 width=3 by frees_pair/
187 | #f1 #I #L #Hf1 #g2 #H
188 elim (eq_inv_nx โฆ H) -H
189 /3 width=3 by frees_unit, isid_eq_repl_back/
190 | #f1 #I #L #i #_ #IH #g2 #H
191 elim (eq_inv_px โฆ H) -H /3 width=3 by frees_lref/
192 | /3 width=3 by frees_gref, isid_eq_repl_back/
193 | /3 width=7 by frees_bind, sor_eq_repl_back3/
194 | /3 width=7 by frees_flat, sor_eq_repl_back3/
198 lemma frees_eq_repl_fwd: โL,T. eq_repl_fwd โฆ (ฮปf. L โข ๐
*โฆTโฆ โ f).
199 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
202 lemma frees_lref_push: โf,i. โ โข ๐
*โฆ#iโฆ โ f โ โ โข ๐
*โฆ#โiโฆ โ โซฏf.
204 elim (frees_inv_atom โฆ H) -H #g #Hg #H destruct
205 /2 width=1 by frees_atom/
208 (* Forward lemmas with test for finite colength *****************************)
210 lemma frees_fwd_isfin: โf,L,T. L โข ๐
*โฆTโฆ โ f โ ๐
โฆfโฆ.
211 #f #L #T #H elim H -f -L -T
212 /4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
215 (* Basic_2A1: removed theorems 30:
216 frees_eq frees_be frees_inv
217 frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
218 frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
219 frees_inv_bind frees_inv_flat frees_inv_bind_O
220 frees_lref_eq frees_lref_be frees_weak
221 frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
222 frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
223 lreq_frees_trans frees_lreq_conf
224 llor_atom llor_skip llor_total
225 llor_tail_frees llor_tail_cofrees