X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Ffrees.ma;h=dee6950e315cf3d41d12a890fa4571290b714418;hb=629687db8a55432e95c82f0c79e3f51c023e65a6;hp=604a918c51a192bef5e6fcfc928d38a1fab86b34;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
index 604a918c5..dee6950e3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma
@@ -12,95 +12,158 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/trace_sor.ma".
-include "ground_2/relocation/trace_isun.ma".
+include "ground_2/relocation/rtmap_sor.ma".
 include "basic_2/notation/relations/freestar_3.ma".
 include "basic_2/grammar/lenv.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
-inductive frees: relation3 lenv term trace ≝
-| frees_atom: ∀I. frees (⋆) (⓪{I}) (◊)
-| frees_sort: ∀I,L,V,s,t. frees L (⋆s) t →
-              frees (L.ⓑ{I}V) (⋆s) (Ⓕ @ t)
-| frees_zero: ∀I,L,V,t. frees L V t →
-              frees (L.ⓑ{I}V) (#0) (Ⓣ @ t)
-| frees_lref: ∀I,L,V,i,t. frees L (#i) t →
-              frees (L.ⓑ{I}V) (#⫯i) (Ⓕ @ t)
-| frees_gref: ∀I,L,V,p,t. frees L (§p) t →
-              frees (L.ⓑ{I}V) (§p) (Ⓕ @ t)
-| frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) →
-              t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t
-| frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 →
-              t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t
+inductive frees: relation3 lenv term rtmap ≝
+| frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
+| frees_sort: ∀I,L,V,s,f. frees L (⋆s) f →
+              frees (L.ⓑ{I}V) (⋆s) (↑f)
+| frees_zero: ∀I,L,V,f. frees L V f →
+              frees (L.ⓑ{I}V) (#0) (⫯f)
+| frees_lref: ∀I,L,V,i,f. frees L (#i) f →
+              frees (L.ⓑ{I}V) (#⫯i) (↑f)
+| frees_gref: ∀I,L,V,p,f. frees L (§p) f →
+              frees (L.ⓑ{I}V) (§p) (↑f)
+| frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
+              f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f
+| frees_flat: ∀I,L,V,T,f1,f2,f. frees L V f1 → frees L T f2 →
+              f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f
 .
 
 interpretation
    "context-sensitive free variables (term)"
    'FreeStar L T t = (frees L T t).
 
-(* Basic forward lemmas *****************************************************)
+(* Basic inversion lemmas ***************************************************)
 
-fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄.
-#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
-[ #_ #L #V #t #_ #_ #x #H destruct
-| #_ #L #_ #i #t #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
+fact frees_inv_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[ #_ #L #V #f #_ #_ #x #H destruct
+| #_ #L #_ #i #f #_ #_ #x #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
 ]
 qed-.
 
-lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄.
-/2 width=5 by frees_fwd_sort_aux/ qed-.
+lemma frees_inv_sort: ∀L,s,f. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=5 by frees_inv_sort_aux/ qed-.
 
-fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄.
-#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
-[ #_ #L #V #t #_ #_ #x #H destruct
-| #_ #L #_ #i #t #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
+fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[ #_ #L #V #f #_ #_ #x #H destruct
+| #_ #L #_ #i #f #_ #_ #x #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
 ]
 qed-.
 
-lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄.
-/2 width=5 by frees_fwd_gref_aux/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
+lemma frees_inv_gref: ∀L,p,f. L ⊢ 𝐅*⦃§p⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=5 by frees_inv_gref_aux/ qed-.
 
-fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 →
-                         (L = ⋆ ∧ t = ◊) ∨
-                         ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
-#L #X #t * -L -X -t
+fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
+                         (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+                         ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
+#L #X #f * -L -X -f
 [ /3 width=1 by or_introl, conj/
-| #I #L #V #s #t #_ #H destruct
+| #I #L #V #s #f #_ #H destruct
 | /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #i #t #_ #H destruct
-| #I #L #V #p #t #_ #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct
+| #I #L #V #i #f #_ #H destruct
+| #I #L #V #p #f #_ #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t →
-                      (L = ⋆ ∧ t = ◊) ∨
-                      ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
+lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f →
+                      (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+                      ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
 /2 width=3 by frees_inv_zero_aux/ qed-.
 
-fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) →
-                         (L = ⋆ ∧ t = ◊) ∨
-                         ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
-#L #X #t * -L -X -t
+fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
+                         (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+                         ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
+#L #X #f * -L -X -f
 [ /3 width=1 by or_introl, conj/
-| #I #L #V #s #t #_ #j #H destruct
-| #I #L #V #t #_ #j #H destruct
-| #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #p #t #_ #j #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct
+| #I #L #V #s #f #_ #j #H destruct
+| #I #L #V #f #_ #j #H destruct
+| #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
+| #I #L #V #p #f #_ #j #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #j #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
 ]
 qed-.
 
-lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t →
-                      (L = ⋆ ∧ t = ◊) ∨
-                      ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
+lemma frees_inv_lref: ∀L,i,f. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
+                      (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+                      ∃∃I,K,V,g. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
 /2 width=3 by frees_inv_lref_aux/ qed-.
+
+fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T →
+                         ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #b #H destruct
+| #I #L #V #s #f #_ #J #W #U #b #H destruct
+| #I #L #V #f #_ #J #W #U #b #H destruct
+| #I #L #V #i #f #_ #J #W #U #b #H destruct
+| #I #L #V #p #f #_ #J #W #U #b #H destruct
+| #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
+]
+qed-.
+
+lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f →
+                      ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+/2 width=4 by frees_inv_bind_aux/ qed-.
+
+fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
+                         ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #H destruct
+| #I #L #V #s #f #_ #J #W #U #H destruct
+| #I #L #V #f #_ #J #W #U #H destruct
+| #I #L #V #i #f #_ #J #W #U #H destruct
+| #I #L #V #p #f #_ #J #W #U #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
+| #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
+                      ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+/2 width=4 by frees_inv_flat_aux/ qed-.
+
+(* Basic properties ********************************************************)
+
+lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T #f1 #H elim H -L -T -f1
+[ /3 width=3 by frees_atom, isid_eq_repl_back/
+| #I #L #V #s #f1 #_ #IH #f2 #Hf12
+  elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
+| #I #L #V #f1 #_ #IH #f2 #Hf12
+  elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
+| #I #L #V #i #f1 #_ #IH #f2 #Hf12
+  elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
+| #I #L #V #p #f1 #_ #IH #f2 #Hf12
+  elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
+| /3 width=7 by frees_bind, sor_eq_repl_back3/
+| /3 width=7 by frees_flat, sor_eq_repl_back3/
+]
+qed-.
+
+lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
+qed-.
+
+lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
+qed.
+
+lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
+qed.