(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "basic_2/notation/relations/cofreestar_4.ma".
include "basic_2/relocation/lift_neg.ma".
include "basic_2/substitution/cpys.ma".

(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)

definition cofrees: relation4 ynat nat lenv term ≝
                    λd,i,L,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶*[d, ∞] U2 → ∃T2. ⇧[i, 1] T2 ≡ U2.

interpretation
   "context-sensitive exclusion from free variables (term)"
   'CoFreeStar L i d T = (cofrees d i L T).

(* Basic forward lemmas *****************************************************)

lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
/2 width=1 by/ qed-.

lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
                           L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
#a #I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
qed-.

lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
                           L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
#a #I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
qed-.

lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
                           L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
#I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
qed-.

lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
                           L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
#I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
qed-.

(* Basic inversion lemmas ***************************************************)

lemma cofrees_inv_gen: ∀L,U,U0,d,i. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
                       L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥.
#L #U #U0 #d #i #HU0 #HnU0 #HU elim (HU … HU0) -L -U -d /2 width=2 by/
qed-.

lemma cofrees_inv_lref_eq: ∀L,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃#i⦄ → ⊥.
#L #d #i #H elim (H (#i)) -H //
#X #H elim (lift_inv_lref2_be … H) -H //
qed-. 

lemma cofrees_inv_bind: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
                        L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
/3 width=8 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.

lemma cofrees_inv_flat: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
                        L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
/3 width=7 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.

(* Basic Properties *********************************************************)

lemma cofrees_lsuby_conf: ∀L1,U,d,i. L1 ⊢ i ~ϵ 𝐅*[d]⦃U⦄ →
                          ∀L2. L1 ⊆[d, ∞] L2 → L2 ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
/3 width=3 by lsuby_cpys_trans/ qed-.

lemma cofrees_sort: ∀L,d,i,k. L ⊢ i ~ϵ 𝐅*[d]⦃⋆k⦄.
#L #d #i #k #X #H >(cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/
qed.

lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄.
#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/
qed.

lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ →
                    ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ →
                    ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄.
#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H
#W2 #U2 #HW12 #HU12 #H destruct
elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/
qed.

lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ →
                    ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄.
#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H
#W2 #U2 #HW12 #HU12 #H destruct
elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/
qed.

lemma cofrees_cpy_trans: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
                         ∀i. L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄.
/3 width=3 by cpys_strap2/ qed-.

axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄).

(* Basic negated properties *************************************************)

lemma frees_cpy_div: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 →
                     ∀i. (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → ⊥).
/3 width=7 by cofrees_cpy_trans/ qed-.

(* Basic negated inversion lemmas *******************************************)

lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) →
                      (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥).
#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i)
/4 width=9 by cofrees_bind, or_intror, or_introl/
qed-.

lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) →
                      (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥).
#I #L #W #U #d #H elim (cofrees_dec L W d)
/4 width=8 by cofrees_flat, or_intror, or_introl/
qed-.