Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta

η-reduction for the λ-calculus #

source
inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Eta {Var : Type u} :
Term Var → Term Var → Prop

A single η-reduction step.

  • eta {Var : Type u} {M : Term Var} : M.LC → (M.app (bvar 0)).abs.Eta M

    The eta rule: λx. M x ⟶ M, provided x is not free in M.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta {Var : Type u} :
    Term Var → Term Var → Prop

    Full η-reduction, defined as the congruence closure of the base η-rule.

    Equations
    Instances For
      source
      def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠ηᶠ_» :
      Lean.TrailingParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢ηᶠ_» :
        Lean.TrailingParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_lc_r {Var : Type u} {M M' : Term Var} (step : M.FullEta M') :
          M'.LC

          The right side of an η-reduction is locally closed.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_lc_l {Var : Type u} {M M' : Term Var} [HasFresh Var] (step : M.FullEta M') :
          M.LC

          The left side of an η-reduction is locally closed.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.redex_app_l_cong {Var : Type u} {M M' N : Term Var} (redex : Relation.ReflTransGen FullEta M M') (lc_N : N.LC) :
          Relation.ReflTransGen FullEta (M.app N) (M'.app N)

          Left congruence rule for application in multiple reduction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.redex_app_r_cong {Var : Type u} {M M' N : Term Var} (redex : Relation.ReflTransGen FullEta M M') (lc_N : N.LC) :
          Relation.ReflTransGen FullEta (N.app M) (N.app M')

          Right congruence rule for application in multiple reduction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.invert_step_app_fvar {Var : Type u} {M N : Term Var} {x : Var} (step : (M.app (fvar x)).FullEta N) :
          ∃ (M' : Term Var), N = M'.app (fvar x) ∧ M.FullEta M'
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_not_fv {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (step : M.FullEta M') :
          M.fv = M'.fv

          An η-reduction step does not introduce new free variables.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.steps_fv {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (steps : Relation.ReflTransGen FullEta M M') :
          M.fv = M'.fv
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_subst_cong_l {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s s' N : Term Var) (step : s.FullEta s') (lc_N : N.LC) :
          s[x := N].FullEta s'[x := N]
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.steps_subst_cong_l {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s s' N : Term Var) (steps : Relation.ReflTransGen FullEta s s') (lc_N : N.LC) :
          Relation.ReflTransGen FullEta s[x := N] s'[x := N]
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_abs_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (step : M.FullEta M') :
          (M.close x).abs.FullEta (M'.close x).abs

          Abstracting then closing preserves a single η-reduction step.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.redex_abs_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (steps : Relation.ReflTransGen FullEta M M') :
          Relation.ReflTransGen FullEta (M.close x).abs (M'.close x).abs

          Abstracting then closing preserves multiple reductions.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.redex_abs_cong {Var : Type u} [HasFresh Var] [DecidableEq Var] {M M' : Term Var} (xs : Finset Var) (cofin : ∀ x ∉ xs, Relation.ReflTransGen FullEta (M.open' (fvar x)) (M'.open' (fvar x))) :
          Relation.ReflTransGen FullEta M.abs M'.abs

          Multiple reduction of opening implies multiple reduction of abstraction.

          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_subst_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s t t' : Term Var) (st : t.FullEta t') (lc_s : s.LC) :
          Relation.ReflTransGen FullEta s[x := t] s[x := t']
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.steps_subst_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s t t' : Term Var) (st : Relation.ReflTransGen FullEta t t') (lc_s : s.LC) :
          Relation.ReflTransGen FullEta s[x := t] s[x := t']
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_open_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {s t t' : Term Var} (lc_s : s.abs.LC) (step : t.FullEta t') :
          Relation.ReflTransGen FullEta (s.open' t) (s.open' t')
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.steps_open_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {s t t' : Term Var} (lc_s : s.abs.LC) (steps : Relation.ReflTransGen FullEta t t') :
          Relation.ReflTransGen FullEta (s.open' t) (s.open' t')
          source
          theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.close_eta_steps {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (hx_M : x ∉ M.fv) (st_M : Relation.ReflGen FullEta (M.open' (fvar x)) N) :
          Relation.ReflGen FullEta M.abs (N.close x).abs