β-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 Cslib.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 Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢βᶠ_» : Lean.TrailingParserDescr

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠βᶠ_» : Lean.TrailingParserDescr

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_lc_l {Var : Type u} {M M' : Term Var} (step : fullBetaRs.Red M M') : M.LC

The left side of a reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_l_cong {Var : Type u} {M M' N : Term Var} (redex : fullBetaRs.MRed M M') (lc_N : N.LC) : fullBetaRs.MRed (M.app N) (M'.app N)

Left congruence rule for application in multiple reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_r_cong {Var : Type u} {M M' N : Term Var} (redex : fullBetaRs.MRed M M') (lc_N : N.LC) : fullBetaRs.MRed (N.app M) (N.app M')

Right congruence rule for application in multiple reduction.

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

The right side of a reduction is locally closed.

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

Substitution respects a single reduction step.

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

Abstracting then closing preserves a single reduction.

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

Abstracting then closing preserves multiple reductions.

theorem Cslib.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, fullBetaRs.MRed (M.open' (fvar x)) (M'.open' (fvar x))) : fullBetaRs.MRed M.abs M'.abs

Multiple reduction of opening implies multiple reduction of abstraction.