β-confluence for the λ-calculus

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

A parallel β-reduction step.

• fvar {Var : Type u} (x : Var) : (Term.fvar x).Parallel (Term.fvar x)

  Free variables parallel step to themselves.

• app {Var : Type u} {L L' M M' : Term Var} : L.Parallel L' → M.Parallel M' → (L.app M).Parallel (L'.app M')

  A parallel left and right congruence rule for application.

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

  Congruence rule for lambda terms.

• beta {Var : Type u} {m m' n n' : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (m.open' (Term.fvar x)).Parallel (m'.open' (Term.fvar x))) → n.Parallel n' → (m.abs.app n).Parallel (m'.open' n')

  A parallel β-reduction.

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.para_lc_l {Var : Type u} {M N : Term Var} (step : paraRs.Red M N) : M.LC

The left side of a parallel reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Parallel.lc_refl {Var : Type u} (M : Term Var) (lc : M.LC) : paraRs.Red M M

Parallel reduction is reflexive for locally closed terms.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_lc_r {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (step : paraRs.Red M N) : N.LC

The right side of a parallel reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_to_para {Var : Type u} {M N : Term Var} (step : fullBetaRs.Red M N) : paraRs.Red M N

A single β-reduction implies a single parallel reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_to_redex {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] (para : paraRs.Red M N) : fullBetaRs.MRed M N

A single parallel reduction implies a multiple β-reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.parachain_iff_redex {Var : Type u} {M N : Term Var} [HasFresh Var] [DecidableEq Var] : paraRs.MRed M N ↔ fullBetaRs.MRed M N

Multiple parallel reduction is equivalent to multiple β-reduction.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_subst {Var : Type u} {M M' N N' : Term Var} [HasFresh Var] [DecidableEq Var] (x : Var) (pm : paraRs.Red M M') (pn : paraRs.Red N N') : paraRs.Red (M[x:=N]) (M'[x:=N'])

Parallel reduction respects substitution.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_open_close {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] (x y : Var) (z : ℕ) (para : paraRs.Red M M') : paraRs.Red (openRec z (fvar y) (closeRec z x M)) (openRec z (fvar y) (closeRec z x M'))

Parallel substitution respects closing and opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_open_out {Var : Type u} {M M' N N' : Term Var} [HasFresh Var] [DecidableEq Var] (L : Finset Var) (mem : ∀ x ∉ L, paraRs.Red (M.open' (fvar x)) (N.open' (fvar x))) (para : paraRs.Red M' N') : paraRs.Red (M.open' M') (N.open' N')

Parallel substitution respects fresh opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_diamond {Var : Type u} [HasFresh Var] [DecidableEq Var] : Diamond Parallel

Parallel reduction has the diamond property.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_confluence {Var : Type u} [HasFresh Var] [DecidableEq Var] : Confluence Parallel

Parallel reduction is confluent.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluence_beta {Var : Type u} [HasFresh Var] [DecidableEq Var] : Confluence FullBeta

β-reduction is confluent.