Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst

source
@[reducible, inline]
abbrev Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Env (Var : Type u) :
Type u

An environment in context of multi substition is a list of pairs of variable targets and terms to be substituted for that target

Equations
Instances For
    source
    def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst {Var : Type u} [DecidableEq Var] (E : Env Var) (M : Term Var) :
    Term Var

    Multi-substitution substitutes all target variables in an environment by their corresponding terms

    Equations
    Instances For
      source
      def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Env.fv {Var : Type u} [DecidableEq Var] (E : Env Var) :
      Finset Var

      The free variables of an environment are the union of the free variables of all terms in the environment. The target variables are not necessarily included

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.env_LC {Var : Type u} (E : Env Var) :
        Prop

        An environment is locally closed if all terms in the environment are locally closed

        Equations
        Instances For
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.env_LC_cons {Var✝ : Type u_1} {sub : Term Var✝} {E : Env Var✝} {x : Var✝} (lc_sub : sub.LC) (lc_E : env_LC E) :
          env_LC (⟨x, sub⟩ :: E)

          Adding a locally closed term to an environment preserves local closure

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst_fvar_fresh {Var : Type u} [DecidableEq Var] (E : Env Var) (x : Var) :
          x ∉ Context.dom E → multiSubst E (fvar x) = fvar x

          Multi-substitution of a fresh variable does nothing

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst_preserves_not_fvar {Var : Type u} [DecidableEq Var] {x : Var} (M : Term Var) (E : Env Var) (nmem : x ∉ M.fv ∪ E.fv) :
          x ∉ (multiSubst E M).fv

          If x is neither a free variable of an environment Ns or a term M, then x is also not a free variable of the multi-substitution of Ns into M

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst_app {Var : Type u} [DecidableEq Var] (M N : Term Var) (E : Env Var) :
          multiSubst E (M.app N) = (multiSubst E M).app (multiSubst E N)

          Multi-substitution propagates recursively through an application

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst_abs {Var : Type u} [DecidableEq Var] (M : Term Var) (E : Env Var) :
          multiSubst E M.abs = (multiSubst E M).abs

          Multi-substitution propagates recursively through an abstraction

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.multiSubst_open_var {Var : Type u} [DecidableEq Var] [HasFresh Var] (M : Term Var) (E : Env Var) (x : Var) (h_ndom : x ∉ Context.dom E) (h_lc : env_LC E) :
          multiSubst E (M.open' (fvar x)) = (multiSubst E M).open' (fvar x)

          Multi-substitution commutes with opening a term with a fresh variable, provided that the variable is not in the domain of the environment and the environment is locally closed