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/grammar/lenv.ma".
19 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
21 inductive frees: relation3 lenv term rtmap ≝
22 | frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
23 | frees_sort: ∀I,L,V,s,f. frees L (⋆s) f →
24 frees (L.ⓑ{I}V) (⋆s) (↑f)
25 | frees_zero: ∀I,L,V,f. frees L V f →
26 frees (L.ⓑ{I}V) (#0) (⫯f)
27 | frees_lref: ∀I,L,V,i,f. frees L (#i) f →
28 frees (L.ⓑ{I}V) (#⫯i) (↑f)
29 | frees_gref: ∀I,L,V,p,f. frees L (§p) f →
30 frees (L.ⓑ{I}V) (§p) (↑f)
31 | frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
32 f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f
33 | frees_flat: ∀I,L,V,T,f1,f2,f. frees L V f1 → frees L T f2 →
34 f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f
38 "context-sensitive free variables (term)"
39 'FreeStar L T t = (frees L T t).
41 (* Basic inversion lemmas ***************************************************)
43 fact frees_inv_atom_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀J. L = ⋆ → X = ⓪{J} → 𝐈⦃f⦄.
44 #L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
45 [5,6: #I #L #V #T [ #p ] #f1 #f2 #f #_ #_ #_ #_ #_ #J #_ #H destruct
46 |*: #I #L #V [1,3,4: #x ] #f #_ #_ #J #H destruct
50 lemma frees_inv_atom: ∀I,f. ⋆ ⊢ 𝐅*⦃⓪{I}⦄ ≡ f → 𝐈⦃f⦄.
51 /2 width=6 by frees_inv_atom_aux/ qed-.
53 fact frees_inv_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
54 #L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
55 [ #_ #L #V #f #_ #_ #x #H destruct
56 | #_ #L #_ #i #f #_ #_ #x #H destruct
57 | #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
58 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
62 lemma frees_inv_sort: ∀L,s,f. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
63 /2 width=5 by frees_inv_sort_aux/ qed-.
65 fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
66 #L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
67 [ #_ #L #V #f #_ #_ #x #H destruct
68 | #_ #L #_ #i #f #_ #_ #x #H destruct
69 | #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
70 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
74 lemma frees_inv_gref: ∀L,l,f. L ⊢ 𝐅*⦃§l⦄ ≡ f → 𝐈⦃f⦄.
75 /2 width=5 by frees_inv_gref_aux/ qed-.
77 fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
79 ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
81 [ /3 width=1 by or_introl, conj/
82 | #I #L #V #s #f #_ #H destruct
83 | /3 width=7 by ex3_4_intro, or_intror/
84 | #I #L #V #i #f #_ #H destruct
85 | #I #L #V #l #f #_ #H destruct
86 | #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #H destruct
87 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct
91 lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f →
93 ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
94 /2 width=3 by frees_inv_zero_aux/ qed-.
96 fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
98 ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
100 [ /3 width=1 by or_introl, conj/
101 | #I #L #V #s #f #_ #j #H destruct
102 | #I #L #V #f #_ #j #H destruct
103 | #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
104 | #I #L #V #l #f #_ #j #H destruct
105 | #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #j #H destruct
106 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
110 lemma frees_inv_lref: ∀L,i,f. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
112 ∃∃I,K,V,g. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
113 /2 width=3 by frees_inv_lref_aux/ qed-.
115 fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T →
116 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
118 [ #I #f #_ #J #W #U #b #H destruct
119 | #I #L #V #s #f #_ #J #W #U #b #H destruct
120 | #I #L #V #f #_ #J #W #U #b #H destruct
121 | #I #L #V #i #f #_ #J #W #U #b #H destruct
122 | #I #L #V #l #f #_ #J #W #U #b #H destruct
123 | #I #L #V #T #p #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
124 | #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
128 lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f →
129 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
130 /2 width=4 by frees_inv_bind_aux/ qed-.
132 fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
133 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
135 [ #I #f #_ #J #W #U #H destruct
136 | #I #L #V #s #f #_ #J #W #U #H destruct
137 | #I #L #V #f #_ #J #W #U #H destruct
138 | #I #L #V #i #f #_ #J #W #U #H destruct
139 | #I #L #V #l #f #_ #J #W #U #H destruct
140 | #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
141 | #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
145 lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
146 ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
147 /2 width=4 by frees_inv_flat_aux/ qed-.
149 (* Basic forward lemmas ****************************************************)
151 lemma frees_fwd_isfin: ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
152 #L #T #f #H elim H -L -T -f
153 /3 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_push, isfin_next/
156 (* Basic properties ********************************************************)
158 lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
159 #L #T #f1 #H elim H -L -T -f1
160 [ /3 width=3 by frees_atom, isid_eq_repl_back/
161 | #I #L #V #s #f1 #_ #IH #f2 #Hf12
162 elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
163 | #I #L #V #f1 #_ #IH #f2 #Hf12
164 elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
165 | #I #L #V #i #f1 #_ #IH #f2 #Hf12
166 elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
167 | #I #L #V #l #f1 #_ #IH #f2 #Hf12
168 elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
169 | /3 width=7 by frees_bind, sor_eq_repl_back3/
170 | /3 width=7 by frees_flat, sor_eq_repl_back3/
174 lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
175 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
178 lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
180 /4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
183 lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
185 /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
188 (* Basic_2A1: removed theorems 27:
189 frees_eq frees_be frees_inv
190 frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
191 frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
192 frees_inv_bind frees_inv_flat frees_inv_bind_O
193 frees_lref_eq frees_lref_be frees_weak
194 frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
195 lreq_frees_trans frees_lreq_conf
196 llor_atom llor_skip llor_total
197 llor_tail_frees llor_tail_cofrees