--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_sor.ma".
+include "static_2/notation/relations/freestar_3.ma".
+include "static_2/syntax/lenv.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+inductive frees: relation3 lenv term rtmap โ
+| frees_sort: โf,L,s. ๐โฆfโฆ โ frees L (โs) f
+| frees_atom: โf,i. ๐โฆfโฆ โ frees (โ) (#i) (โซฏ*[i]โf)
+| frees_pair: โf,I,L,V. frees L V f โ
+ frees (L.โ{I}V) (#0) (โf)
+| frees_unit: โf,I,L. ๐โฆfโฆ โ frees (L.โค{I}) (#0) (โf)
+| frees_lref: โf,I,L,i. frees L (#i) f โ
+ frees (L.โ{I}) (#โi) (โซฏf)
+| frees_gref: โf,L,l. ๐โฆfโฆ โ frees L (ยงl) f
+| frees_bind: โf1,f2,f,p,I,L,V,T. frees L V f1 โ frees (L.โ{I}V) T f2 โ
+ f1 โ โซฑf2 โ f โ frees L (โ{p,I}V.T) f
+| frees_flat: โf1,f2,f,I,L,V,T. 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 f = (frees L T f).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact frees_inv_sort_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โx. X = โx โ ๐โฆfโฆ.
+#L #X #f #H elim H -f -L -X //
+[ #f #i #_ #x #H destruct
+| #f #_ #L #V #_ #_ #x #H destruct
+| #f #_ #L #_ #x #H destruct
+| #f #_ #L #i #_ #_ #x #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+]
+qed-.
+
+lemma frees_inv_sort: โf,L,s. L โข ๐
*โฆโsโฆ โ f โ ๐โฆfโฆ.
+/2 width=5 by frees_inv_sort_aux/ qed-.
+
+fact frees_inv_atom_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โi. L = โ โ X = #i โ
+ โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
+#f #L #X #H elim H -f -L -X
+[ #f #L #s #_ #j #_ #H destruct
+| #f #i #Hf #j #_ #H destruct /2 width=3 by ex2_intro/
+| #f #I #L #V #_ #_ #j #H destruct
+| #f #I #L #_ #j #H destruct
+| #f #I #L #i #_ #_ #j #H destruct
+| #f #L #l #_ #j #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #j #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #j #_ #H destruct
+]
+qed-.
+
+lemma frees_inv_atom: โf,i. โ โข ๐
*โฆ#iโฆ โ f โ โโg. ๐โฆgโฆ & f = โซฏ*[i]โg.
+/2 width=5 by frees_inv_atom_aux/ qed-.
+
+fact frees_inv_pair_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K,V. L = K.โ{I}V โ X = #0 โ
+ โโg. K โข ๐
*โฆVโฆ โ g & f = โg.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #Z #Y #X #_ #H destruct
+| #f #i #_ #Z #Y #X #H destruct
+| #f #I #L #V #Hf #Z #Y #X #H #_ destruct /2 width=3 by ex2_intro/
+| #f #I #L #_ #Z #Y #X #H destruct
+| #f #I #L #i #_ #Z #Y #X #_ #H destruct
+| #f #L #l #_ #Z #Y #X #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #X #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #X #_ #H destruct
+]
+qed-.
+
+lemma frees_inv_pair: โf,I,K,V. K.โ{I}V โข ๐
*โฆ#0โฆ โ f โ โโg. K โข ๐
*โฆVโฆ โ g & f = โg.
+/2 width=6 by frees_inv_pair_aux/ qed-.
+
+fact frees_inv_unit_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K. L = K.โค{I} โ X = #0 โ
+ โโg. ๐โฆgโฆ & f = โg.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #Z #Y #_ #H destruct
+| #f #i #_ #Z #Y #H destruct
+| #f #I #L #V #_ #Z #Y #H destruct
+| #f #I #L #Hf #Z #Y #H destruct /2 width=3 by ex2_intro/
+| #f #I #L #i #_ #Z #Y #_ #H destruct
+| #f #L #l #_ #Z #Y #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
+]
+qed-.
+
+lemma frees_inv_unit: โf,I,K. K.โค{I} โข ๐
*โฆ#0โฆ โ f โ โโg. ๐โฆgโฆ & f = โg.
+/2 width=7 by frees_inv_unit_aux/ qed-.
+
+fact frees_inv_lref_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,K,j. L = K.โ{I} โ X = #(โj) โ
+ โโg. K โข ๐
*โฆ#jโฆ โ g & f = โซฏg.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #Z #Y #j #_ #H destruct
+| #f #i #_ #Z #Y #j #H destruct
+| #f #I #L #V #_ #Z #Y #j #_ #H destruct
+| #f #I #L #_ #Z #Y #j #_ #H destruct
+| #f #I #L #i #Hf #Z #Y #j #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #f #L #l #_ #Z #Y #j #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
+]
+qed-.
+
+lemma frees_inv_lref: โf,I,K,i. K.โ{I} โข ๐
*โฆ#(โi)โฆ โ f โ
+ โโg. K โข ๐
*โฆ#iโฆ โ g & f = โซฏg.
+/2 width=6 by frees_inv_lref_aux/ qed-.
+
+fact frees_inv_gref_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โx. X = ยงx โ ๐โฆfโฆ.
+#f #L #X #H elim H -f -L -X //
+[ #f #i #_ #x #H destruct
+| #f #_ #L #V #_ #_ #x #H destruct
+| #f #_ #L #_ #x #H destruct
+| #f #_ #L #i #_ #_ #x #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+]
+qed-.
+
+lemma frees_inv_gref: โf,L,l. L โข ๐
*โฆยงlโฆ โ f โ ๐โฆfโฆ.
+/2 width=5 by frees_inv_gref_aux/ qed-.
+
+fact frees_inv_bind_aux: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โp,I,V,T. X = โ{p,I}V.T โ
+ โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L.โ{I}V โข ๐
*โฆTโฆ โ f2 & f1 โ โซฑf2 โ f.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #q #J #W #U #H destruct
+| #f #i #_ #q #J #W #U #H destruct
+| #f #I #L #V #_ #q #J #W #U #H destruct
+| #f #I #L #_ #q #J #W #U #H destruct
+| #f #I #L #i #_ #q #J #W #U #H destruct
+| #f #L #l #_ #q #J #W #U #H destruct
+| #f1 #f2 #f #p #I #L #V #T #HV #HT #Hf #q #J #W #U #H destruct /2 width=5 by ex3_2_intro/
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #q #J #W #U #H destruct
+]
+qed-.
+
+lemma frees_inv_bind: โf,p,I,L,V,T. L โข ๐
*โฆโ{p,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: โf,L,X. L โข ๐
*โฆXโฆ โ f โ โI,V,T. X = โ{I}V.T โ
+ โโf1,f2. L โข ๐
*โฆVโฆ โ f1 & L โข ๐
*โฆTโฆ โ f2 & f1 โ f2 โ f.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #J #W #U #H destruct
+| #f #i #_ #J #W #U #H destruct
+| #f #I #L #V #_ #J #W #U #H destruct
+| #f #I #L #_ #J #W #U #H destruct
+| #f #I #L #i #_ #J #W #U #H destruct
+| #f #L #l #_ #J #W #U #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #J #W #U #H destruct
+| #f1 #f2 #f #I #L #V #T #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma frees_inv_flat: โf,I,L,V,T. 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 -f1 -L -T
+[ /3 width=3 by frees_sort, isid_eq_repl_back/
+| #f1 #i #Hf1 #g2 #H
+ elim (eq_inv_pushs_sn โฆ H) -H #g #Hg #H destruct
+ elim (eq_inv_nx โฆ Hg) -Hg
+ /3 width=3 by frees_atom, isid_eq_repl_back/
+| #f1 #I #L #V #_ #IH #g2 #H
+ elim (eq_inv_nx โฆ H) -H
+ /3 width=3 by frees_pair/
+| #f1 #I #L #Hf1 #g2 #H
+ elim (eq_inv_nx โฆ H) -H
+ /3 width=3 by frees_unit, isid_eq_repl_back/
+| #f1 #I #L #i #_ #IH #g2 #H
+ elim (eq_inv_px โฆ H) -H /3 width=3 by frees_lref/
+| /3 width=3 by frees_gref, isid_eq_repl_back/
+| /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_lref_push: โf,i. โ โข ๐
*โฆ#iโฆ โ f โ โ โข ๐
*โฆ#โiโฆ โ โซฏf.
+#f #i #H
+elim (frees_inv_atom โฆ H) -H #g #Hg #H destruct
+/2 width=1 by frees_atom/
+qed.
+
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma frees_fwd_isfin: โf,L,T. L โข ๐
*โฆTโฆ โ f โ ๐
โฆfโฆ.
+#f #L #T #H elim H -f -L -T
+/4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
+qed-.
+
+(* Basic_2A1: removed theorems 30:
+ frees_eq frees_be frees_inv
+ frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free
+ frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt
+ frees_inv_bind frees_inv_flat frees_inv_bind_O
+ frees_lref_eq frees_lref_be frees_weak
+ frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx
+ frees_lift_ge frees_inv_lift_be frees_inv_lift_ge
+ lreq_frees_trans frees_lreq_conf
+ llor_atom llor_skip llor_total
+ llor_tail_frees llor_tail_cofrees
+*)