β-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.Beta {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).Beta (M.open' N)

  Reduce an application to a lambda term.

@[reducible, inline]

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

Full β-reduction.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta = Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Xi Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Beta

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 : M.FullBeta 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 : Relation.ReflTransGen FullBeta M M') (lc_N : N.LC) : Relation.ReflTransGen FullBeta (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 : Relation.ReflTransGen FullBeta M M') (lc_N : N.LC) : Relation.ReflTransGen FullBeta (N.app M) (N.app M')

Right congruence rule for application in multiple reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.invert_step_app_fvar {Var : Type u} {M N : Term Var} {x : Var} (step : (M.app (fvar x)).FullBeta N) : (∃ (M' : Term Var), N = M'.app (fvar x) ∧ M.FullBeta M') ∨ ∃ (M1 : Term Var), M = M1.abs ∧ N = M1.open' (fvar x)

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

The right side of a reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.steps_lc_or_rfl {Var : Type u} [HasFresh Var] [DecidableEq Var] {M M' : Term Var} (redex : Relation.ReflTransGen FullBeta M M') : M.LC ∧ M'.LC ∨ M = M'

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_subst_cong_lc {Var : Type u} [HasFresh Var] [DecidableEq Var] (s s' t : Term Var) (x : Var) (step : s.FullBeta s') (h_lc : t.LC) : s[x := t].FullBeta s'[x := t]

Substitution of a locally closed term respects a single reduction step.

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 : s.FullBeta s') : s[x := fvar y].FullBeta s'[x := fvar y]

Substitution respects a single reduction step of a free variable.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_not_fv {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (step : M.FullBeta N) : N.fv ⊆ M.fv

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

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_abs_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {x : Var} (step : M.FullBeta M') : (closeRec 0 x M).abs.FullBeta (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 : Relation.ReflTransGen FullBeta M M') : Relation.ReflTransGen FullBeta (closeRec 0 x M).abs (closeRec 0 x M').abs

Abstracting then closing preserves multiple reductions.

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

Multiple reduction of opening implies multiple reduction of abstraction.

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, Relation.ReflTransGen FullBeta (M.open' (fvar x)) (M'.open' (fvar x))) : Relation.ReflTransGen FullBeta M.abs M'.abs

Multiple reduction of opening implies multiple reduction of abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_open_cong_l {Var : Type u} [HasFresh Var] [DecidableEq Var] (s s' t : Term Var) (L : Finset Var) (step : ∀ x ∉ L, (s.open' (fvar x)).FullBeta (s'.open' (fvar x))) (h_lc : t.LC) : (s.open' t).FullBeta (s'.open' t)

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.invert_steps_abs {Var : Type u} [HasFresh Var] [DecidableEq Var] {s t : Term Var} (step : Relation.ReflTransGen FullBeta s.abs t) : ∃ (s' : Term Var), Relation.ReflTransGen FullBeta s.abs s'.abs ∧ t = s'.abs

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.steps_open_cong_l_abs {Var : Type u} [HasFresh Var] [DecidableEq Var] (s s' t : Term Var) (steps : Relation.ReflTransGen FullBeta s.abs s'.abs) (lc_t : t.LC) : Relation.ReflTransGen FullBeta (s.open' t) (s'.open' t)

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.step_subst_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s t t' : Term Var) (step : t.FullBeta t') (h_lc : s.LC) : Relation.ReflTransGen FullBeta s[x := t] s[x := t']

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.steps_subst_cong_r {Var : Type u} [HasFresh Var] [DecidableEq Var] {x : Var} (s t t' : Term Var) (step : Relation.ReflTransGen FullBeta t t') (h_lc : s.LC) : Relation.ReflTransGen FullBeta s[x := t] s[x := t']

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.steps_open_cong_abs {Var : Type u} [HasFresh Var] [DecidableEq Var] (s s' t t' : Term Var) (step1 : Relation.ReflTransGen FullBeta t t') (step2 : Relation.ReflTransGen FullBeta s.abs s'.abs) (lc_t : t.LC) (lc_s : s.abs.LC) : Relation.ReflTransGen FullBeta (s.open' t) (s'.open' t')