File ApplicationContext

From MatchingLogic Require Export Pattern.

Section with_signature.
    Context {Σ : Signature}.

    (* TODO make Set ? *)
  Inductive Application_context : Type :=
  | box
  | ctx_app_l (cc : Application_context) (p : Pattern) (Prf : well_formed p)
  | ctx_app_r (p : Pattern) (cc : Application_context) (Prf : well_formed p)
  .

  Fixpoint AC_free_evars (AC : Application_context) : EVarSet :=
    match AC with
    | box ⇒ ∅
    | @ctx_app_l cc p _ ⇒ free_evars p ∪ AC_free_evars cc
    | @ctx_app_r p cc _ ⇒ free_evars p ∪ AC_free_evars cc
    end.

  Fixpoint subst_ctx (C : Application_context) (p : Pattern)
    : Pattern :=
    match C with
    | box ⇒ p
    | @ctx_app_l C' p' prf ⇒ patt_app (subst_ctx C' p) p'
    | @ctx_app_r p' C' prf ⇒ patt_app p' (subst_ctx C' p)
    end.

  (* TODO rewrite using wc_sctx *)
  Lemma wf_sctx (C : Application_context) (A : Pattern) :
    well_formed A = true → well_formed (subst_ctx C A) = true.

  Lemma wp_sctx (C : Application_context) (A : Pattern) :
    well_formed_positive A = true → well_formed_positive (subst_ctx C A) = true.

  Lemma wcex_sctx (C : Application_context) (A : Pattern) idx1 :
    well_formed_closed_ex_aux A idx1 = true → well_formed_closed_ex_aux (subst_ctx C A) idx1 = true.

  Lemma wcmu_sctx (C : Application_context) (A : Pattern) idx1 :
    well_formed_closed_mu_aux A idx1 = true → well_formed_closed_mu_aux (subst_ctx C A) idx1 = true.

  Fixpoint free_evars_ctx (C : Application_context)
    : (EVarSet) :=
    match C with
    | box ⇒ empty
    | @ctx_app_l cc p prf ⇒ union (free_evars_ctx cc) (free_evars p)
    | @ctx_app_r p cc prf ⇒ union (free_evars p) (free_evars_ctx cc)
    end.

  Definition ApplicationContext2Pattern (boxvar : evar) (AC : Application_context) :=
    subst_ctx AC (patt_free_evar boxvar).

  Lemma ApplicationContext2Pattern_one_occ (AC : Application_context) (boxvar : evar):
    boxvar ∉ free_evars_ctx AC →
    count_evar_occurrences boxvar (ApplicationContext2Pattern boxvar AC) = 1.

  End with_signature.

Module Notations.

Notation "□" := box.
Notation "p '$ₗ' C" := (@ctx_app_l _ p C _) (at level 65).
Notation "C '$ᵣ' p" := (@ctx_app_r _ C p _) (at level 65).
Notation "C .[ □ ↦ p ]" := (subst_ctx C p)
   (at level 2, format "C .[ □ ↦ p ]").

End Notations.

Lemma free_evars_subst_ctx {Σ : Signature} AC ϕ:
  free_evars (subst_ctx AC ϕ) = AC_free_evars AC ∪ free_evars ϕ.