β-reduction for the λ-calculus

References

• [A. Chargueraud, The Locally Nameless Representation] [Cha12]
• See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which this is partially adapted

inductive LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta {Var : Type u} : Term Var → Term Var → Prop

A single β-reduction step.

• beta {Var : Type u} {M N : Term Var} : M.abs.LC → N.LC → (M.abs.app N).FullBeta (M.open' N)

  Reduce an application to a lambda term.

• appL {Var : Type u} {Z M N : Term Var} : Z.LC → M.FullBeta N → (Z.app M).FullBeta (Z.app N)

  Left congruence rule for application.

• appR {Var : Type u} {Z M N : Term Var} : Z.LC → M.FullBeta N → (M.app Z).FullBeta (N.app Z)

  Right congruence rule for application.

• abs {Var : Type u} {M N : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (M.open' (fvar x)).FullBeta (N.open' (fvar x))) → M.abs.FullBeta N.abs

  Congruence rule for lambda terms.

def «term_⭢βᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term_↠βᶠ_».«delab_app.ReductionSystem.MRed» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term_↠βᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term_⭢βᶠ_».«delab_app.ReductionSystem.Red» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_lc_l {Var : Type u} {M M' : Term Var} (step : M ⭢βᶠ M') : M.LC

The left side of a reduction is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_l_cong {Var : Type u} {M M' N : Term Var} (redex : M ↠βᶠ M') (lc_N : N.LC) : M.app N ↠βᶠ M'.app N

Left congruence rule for application in multiple reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_r_cong {Var : Type u} {M M' N : Term Var} (redex : M ↠βᶠ M') (lc_N : N.LC) : N.app M ↠βᶠ N.app M'

Right congruence rule for application in multiple reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_lc_r {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (step : M ⭢βᶠ M') : M'.LC

The right side of a reduction is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_subst_cong {Var : Type u} [HasFresh Var] [DecidableEq Var] (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') : s[x:=fvar y] ⭢βᶠ s'[x:=fvar y]

Substitution respects a single reduction step.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_abs_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (step : M ⭢βᶠ M') : (closeRec 0 x M).abs ⭢βᶠ (closeRec 0 x M').abs

Abstracting then closing preserves a single reduction.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_abs_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (step : M ↠βᶠ M') : (closeRec 0 x M).abs ↠βᶠ (closeRec 0 x M').abs

Abstracting then closing preserves multiple reductions.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_abs_cong {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (xs : Finset Var) (cofin : ∀ x ∉ xs, M.open' (fvar x) ↠βᶠ M'.open' (fvar x)) : M.abs ↠βᶠ M'.abs

Multiple reduction of opening implies multiple reduction of abstraction.