(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
inductive frees: relation3 lenv term pr_map ≝
-| frees_sort: â\88\80f,L,s. ð\9d\90\88â\9dªfâ\9d« → frees L (⋆s) f
-| frees_atom: â\88\80f,i. ð\9d\90\88â\9dªfâ\9d« → frees (⋆) (#i) (⫯*[i]↑f)
+| frees_sort: â\88\80f,L,s. ð\9d\90\88â\9d¨fâ\9d© → frees L (⋆s) f
+| frees_atom: â\88\80f,i. ð\9d\90\88â\9d¨fâ\9d© → frees (⋆) (#i) (⫯*[i]↑f)
| frees_pair: ∀f,I,L,V. frees L V f →
frees (L.ⓑ[I]V) (#0) (↑f)
-| frees_unit: â\88\80f,I,L. ð\9d\90\88â\9dªfâ\9d« → frees (L.ⓤ[I]) (#0) (↑f)
+| frees_unit: â\88\80f,I,L. ð\9d\90\88â\9d¨fâ\9d© → frees (L.ⓤ[I]) (#0) (↑f)
| frees_lref: ∀f,I,L,i. frees L (#i) f →
frees (L.ⓘ[I]) (#↑i) (⫯f)
-| frees_gref: â\88\80f,L,l. ð\9d\90\88â\9dªfâ\9d« → frees L (§l) f
+| frees_gref: â\88\80f,L,l. ð\9d\90\88â\9d¨fâ\9d© → 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 →
(* Basic inversion lemmas ***************************************************)
-fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80x. X = â\8b\86x â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© â\89\98 f â\86\92 â\88\80x. X = â\8b\86x â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
#L #X #f #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
]
qed-.
-lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85+â\9dªâ\8b\86sâ\9d« â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85+â\9d¨â\8b\86sâ\9d© â\89\98 f â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
/2 width=5 by frees_inv_sort_aux/ qed-.
fact frees_inv_atom_aux:
- â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀i. L = ⋆ → X = #i →
- â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ⫯*[i]↑g.
+ â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀i. L = ⋆ → X = #i →
+ â\88\83â\88\83g. ð\9d\90\88â\9d¨gâ\9d© & 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/
]
qed-.
-lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ⫯*[i]↑g.
+lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9d¨#iâ\9d© â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â\9d¨gâ\9d© & f = ⫯*[i]↑g.
/2 width=5 by frees_inv_atom_aux/ qed-.
fact frees_inv_pair_aux:
- â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀I,K,V. L = K.ⓑ[I]V → X = #0 →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dªVâ\9d« ≘ g & f = ↑g.
+ â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀I,K,V. L = K.ⓑ[I]V → X = #0 →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© ≘ g & f = ↑g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #X #_ #H destruct
| #f #i #_ #Z #Y #X #H destruct
]
qed-.
-lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dª#0â\9d« â\89\98 f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dªVâ\9d« ≘ g & f = ↑g.
+lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9d¨#0â\9d© â\89\98 f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© ≘ g & f = ↑g.
/2 width=6 by frees_inv_pair_aux/ qed-.
fact frees_inv_unit_aux:
- â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀I,K. L = K.ⓤ[I] → X = #0 →
- â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ↑g.
+ â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀I,K. L = K.ⓤ[I] → X = #0 →
+ â\88\83â\88\83g. ð\9d\90\88â\9d¨gâ\9d© & f = ↑g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #_ #H destruct
| #f #i #_ #Z #Y #H destruct
]
qed-.
-lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤[I] â\8a¢ ð\9d\90\85+â\9dª#0â\9d« â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ↑g.
+lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤[I] â\8a¢ ð\9d\90\85+â\9d¨#0â\9d© â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â\9d¨gâ\9d© & f = ↑g.
/2 width=7 by frees_inv_unit_aux/ qed-.
fact frees_inv_lref_aux:
- â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀I,K,j. L = K.ⓘ[I] → X = #(↑j) →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dª#jâ\9d« ≘ g & f = ⫯g.
+ â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀I,K,j. L = K.ⓘ[I] → X = #(↑j) →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9d¨#jâ\9d© ≘ g & f = ⫯g.
#f #L #X * -f -L -X
[ #f #L #s #_ #Z #Y #j #_ #H destruct
| #f #i #_ #Z #Y #j #H destruct
qed-.
lemma frees_inv_lref:
- â\88\80f,I,K,i. K.â\93\98[I] â\8a¢ ð\9d\90\85+â\9dª#(â\86\91i)â\9d« ≘ f →
- â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« ≘ g & f = ⫯g.
+ â\88\80f,I,K,i. K.â\93\98[I] â\8a¢ ð\9d\90\85+â\9d¨#(â\86\91i)â\9d© ≘ f →
+ â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9d¨#iâ\9d© ≘ g & f = ⫯g.
/2 width=6 by frees_inv_lref_aux/ qed-.
-fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80x. X = §x â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© â\89\98 f â\86\92 â\88\80x. X = §x â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
#f #L #X #H elim H -f -L -X //
[ #f #i #_ #x #H destruct
| #f #_ #L #V #_ #_ #x #H destruct
]
qed-.
-lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85+â\9dªÂ§lâ\9d« â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85+â\9d¨Â§lâ\9d© â\89\98 f â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
/2 width=5 by frees_inv_gref_aux/ qed-.
fact frees_inv_bind_aux:
- â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
+ â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ 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
qed-.
lemma frees_inv_bind:
- â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9dªâ\93\91[p,I]V.Tâ\9d« ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
+ â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9d¨â\93\91[p,I]V.Tâ\9d© ≘ f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
/2 width=4 by frees_inv_bind_aux/ qed-.
-fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ f2 ≘ f.
+fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9d¨Xâ\9d© ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ 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
qed-.
lemma frees_inv_flat:
- â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9dªâ\93\95[I]V.Tâ\9d« ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ f2 ≘ f.
+ â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9d¨â\93\95[I]V.Tâ\9d© ≘ f →
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9d¨Vâ\9d© â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f2 & f1 ⋓ f2 ≘ f.
/2 width=4 by frees_inv_flat_aux/ qed-.
(* Basic properties ********************************************************)
-lemma frees_eq_repl_back: â\88\80L,T. pr_eq_repl_back â\80¦ (λf. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f).
+lemma frees_eq_repl_back: â\88\80L,T. pr_eq_repl_back â\80¦ (λf. L â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f).
#L #T #f1 #H elim H -f1 -L -T
[ /3 width=3 by frees_sort, pr_isi_eq_repl_back/
| #f1 #i #Hf1 #g2 #H
]
qed-.
-lemma frees_eq_repl_fwd: â\88\80L,T. pr_eq_repl_fwd â\80¦ (λf. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f).
+lemma frees_eq_repl_fwd: â\88\80L,T. pr_eq_repl_fwd â\80¦ (λf. L â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f).
#L #T @pr_eq_repl_sym /2 width=3 by frees_eq_repl_back/
qed-.
-lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#â\86\91iâ\9d« ≘ ⫯f.
+lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9d¨#iâ\9d© â\89\98 f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85+â\9d¨#â\86\91iâ\9d© ≘ ⫯f.
#f #i #H
elim (frees_inv_atom … H) -H #g #Hg #H destruct
/2 width=1 by frees_atom/
(* Forward lemmas with test for finite colength *****************************)
-lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© â\89\98 f â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
#f #L #T #H elim H -f -L -T
/4 width=5 by pr_sor_inv_isf_bi, pr_isf_isi, pr_isf_tl, pr_isf_pushs, pr_isf_push, pr_isf_next/
qed-.