Untyped λ-calculus

Note that we are not using simp or aesop in this file, even though our code is written in a style that is compatible with these tactics. This is because we want to keep the proofs as explicit as possible, for educational purposes.

inductive Untyped.Λ : Type

• var: Name → Untyped.Λ
• app: Untyped.Λ → Untyped.Λ → Untyped.Λ
• abs: Name → Untyped.Λ → Untyped.Λ

instance Untyped.instReprΛ : Repr Untyped.Λ

Equations

• Untyped.instReprΛ = { reprPrec := Untyped.reprΛ✝ }

instance Untyped.instOrdΛ : Ord Untyped.Λ

Equations

• Untyped.instOrdΛ = { compare := Untyped.ordΛ✝ }

instance Untyped.instDecidableEqΛ : DecidableEq Untyped.Λ

Equations

• Untyped.instDecidableEqΛ = Untyped.decEqΛ✝

def Untyped.Λ.toString : Untyped.Λ → String

Equations

• (Untyped.Λ.var a).toString = a
• (a ∙ a_1).toString = toString "(" ++ toString a.toString ++ toString " " ++ toString a_1.toString ++ toString ")"
• (Untyped.Λ.abs a a_1).toString = toString "(λ" ++ toString a ++ toString ". " ++ toString a_1.toString ++ toString ")"

instance Untyped.Λ.instToString : ToString Untyped.Λ

Equations

• Untyped.Λ.instToString = { toString := Untyped.Λ.toString }

instance Untyped.Λ.instCoeName : Coe Name Untyped.Λ

Equations

• Untyped.Λ.instCoeName = { coe := Untyped.Λ.var }

def Untyped.Λ.«termLam_↦_» : Lean.ParserDescr

Equations

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

def Untyped.Λ.«term_∙_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_∙_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_∙_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 101))

def Untyped.Λ.size : Untyped.Λ → ℕ

Equations

• (Untyped.Λ.var a).size = 1
• (a ∙ a_1).size = 1 + a.size + a_1.size
• (Untyped.Λ.abs a a_1).size = 1 + a_1.size

instance Untyped.Λ.instSizeOf : SizeOf Untyped.Λ

Equations

• Untyped.Λ.instSizeOf = { sizeOf := Untyped.Λ.size }

def Untyped.Λ.Sub (t : Untyped.Λ) : Multiset Untyped.Λ

Equations

• (Untyped.Λ.var a).Sub = {Untyped.Λ.var a}
• (a ∙ a_1).Sub = a ∙ a_1 ::ₘ (a.Sub + a_1.Sub)
• (Untyped.Λ.abs a a_1).Sub = Untyped.Λ.abs a a_1 ::ₘ a_1.Sub

def Untyped.Λ.Subterm (L : Untyped.Λ) (M : Untyped.Λ) : Prop

Equations

• L.Subterm M = (L ∈ M.Sub)

instance Untyped.Λ.instHasSubset : HasSubset Untyped.Λ

Equations

• Untyped.Λ.instHasSubset = { Subset := Untyped.Λ.Subterm }

instance Untyped.Λ.instIsReflMemMultisetSub : IsRefl Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 ∈ x2.Sub

Equations

• Untyped.Λ.instIsReflMemMultisetSub = ⋯

instance Untyped.Λ.instIsReflSubterm : IsRefl Untyped.Λ Untyped.Λ.Subterm

Equations

• Untyped.Λ.instIsReflSubterm = ⋯

instance Untyped.Λ.instIsReflSubset : IsRefl Untyped.Λ Subset

Equations

• Untyped.Λ.instIsReflSubset = ⋯

instance Untyped.Λ.instIsTransMemMultisetSub : IsTrans Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 ∈ x2.Sub

Equations

• Untyped.Λ.instIsTransMemMultisetSub = ⋯

instance Untyped.Λ.instIsTransSubterm : IsTrans Untyped.Λ Untyped.Λ.Subterm

Equations

• Untyped.Λ.instIsTransSubterm = ⋯

instance Untyped.Λ.instIsTransSubset : IsTrans Untyped.Λ Subset

Equations

• Untyped.Λ.instIsTransSubset = ⋯

instance Untyped.Λ.instDecidableSubterm {M : Untyped.Λ} {N : Untyped.Λ} : Decidable (M.Subterm N)

Equations

• Untyped.Λ.instDecidableSubterm = inferInstanceAs (Decidable (M ∈ N.Sub))

instance Untyped.Λ.instDecidableSubset {M : Untyped.Λ} {N : Untyped.Λ} : Decidable (M ⊆ N)

Equations

• Untyped.Λ.instDecidableSubset = inferInstanceAs (Decidable (M ∈ N.Sub))

def Untyped.Λ.ProperSubterm (L : Untyped.Λ) (M : Untyped.Λ) : Prop

Equations

• L.ProperSubterm M = (L ≠ M ∧ L ⊆ M)

instance Untyped.Λ.instHasSSubset : HasSSubset Untyped.Λ

Equations

• Untyped.Λ.instHasSSubset = { SSubset := Untyped.Λ.ProperSubterm }

instance Untyped.Λ.instDecidableProperSubterm {M : Untyped.Λ} {N : Untyped.Λ} : Decidable (M.ProperSubterm N)

Equations

• Untyped.Λ.instDecidableProperSubterm = inferInstanceAs (Decidable (M ≠ N ∧ M ⊆ N))

instance Untyped.Λ.instDecidableSSubset {M : Untyped.Λ} {N : Untyped.Λ} : Decidable (M ⊂ N)

Equations

• Untyped.Λ.instDecidableSSubset = inferInstanceAs (Decidable (M ≠ N ∧ M ⊆ N))

def Untyped.Λ.FV : Untyped.Λ → Finset Name

Equations

• (Untyped.Λ.var a).FV = {a}
• (a ∙ a_1).FV = a.FV ∪ a_1.FV
• (Untyped.Λ.abs a a_1).FV = a_1.FV \ {a}

def Untyped.Λ.Closed (M : Untyped.Λ) : Prop

Equations

• M.Closed = (M.FV = ∅)

instance Untyped.Λ.instDecidableClosed {M : Untyped.Λ} : Decidable M.Closed

Equations

• Untyped.Λ.instDecidableClosed = inferInstanceAs (Decidable (M.FV = ∅))

def Untyped.Λ.hasBindingVar (t : Untyped.Λ) (x : Name) : Prop

Equations

• (Untyped.Λ.var a).hasBindingVar x = False
• (a ∙ a_1).hasBindingVar x = (a.hasBindingVar x ∨ a_1.hasBindingVar x)
• (Untyped.Λ.abs a a_1).hasBindingVar x = (x = a ∨ a_1.hasBindingVar x)

def Untyped.Λ.hasDecHasBindingVar (M : Untyped.Λ) (x : Name) : Decidable (M.hasBindingVar x)

Equations

• (Untyped.Λ.var a).hasDecHasBindingVar x = isFalse ⋯
• (a ∙ a_1).hasDecHasBindingVar x = match a.hasDecHasBindingVar x, a_1.hasDecHasBindingVar x with | isTrue hP, x_1 => isTrue ⋯ | x_1, isTrue hQ => isTrue ⋯ | isFalse hP, isFalse hQ => isFalse ⋯
• (Untyped.Λ.abs a a_1).hasDecHasBindingVar x = if h : x = a then isTrue ⋯ else match a_1.hasDecHasBindingVar x with | isTrue hQ => isTrue ⋯ | isFalse hQ => isFalse ⋯

instance Untyped.Λ.instDecidableHasBindingVar {M : Untyped.Λ} {x : Name} : Decidable (M.hasBindingVar x)

Equations

• Untyped.Λ.instDecidableHasBindingVar = M.hasDecHasBindingVar x

def Untyped.Λ.rename (t : Untyped.Λ) (x : Name) (y : Name) : Untyped.Λ

Equations

• (Untyped.Λ.var a).rename x y = if a = x then Untyped.Λ.var y else Untyped.Λ.var a
• (a ∙ a_1).rename x y = a.rename x y ∙ a_1.rename x y
• (Untyped.Λ.abs a a_1).rename x y = if a_1.hasBindingVar y ∨ y ∈ a_1.FV then Untyped.Λ.abs a a_1 else if a = x then Untyped.Λ.abs y (a_1.rename x y) else Untyped.Λ.abs a (a_1.rename x y)

@[simp]

theorem Untyped.Λ.rename_size_eq {M : Untyped.Λ} {x : Name} {y : Name} : (M.rename x y).size = M.size

inductive Untyped.Λ.Renaming : Untyped.Λ → Untyped.Λ → Prop

• rename: ∀ (x y : Name) (M : Untyped.Λ), y ∉ M.FV → ¬M.hasBindingVar y → (Untyped.Λ.abs x M).Renaming (Untyped.Λ.abs y (M.rename x y))

@[simp]

theorem Untyped.Λ.renaming_rename {x : Name} {y : Name} {M : Untyped.Λ} {hfv : y ∉ M.FV} {hnb : ¬M.hasBindingVar y} : (Untyped.Λ.abs x M).Renaming (Untyped.Λ.abs y (M.rename x y))

inductive Untyped.Λ.AlphaEq : Untyped.Λ → Untyped.Λ → Prop

• rename: ∀ {M N : Untyped.Λ}, M.Renaming N → M =α N
• compatAppLeft: ∀ {L M N : Untyped.Λ}, M =α N → M ∙ L =α N ∙ L
• compatAppRight: ∀ {L M N : Untyped.Λ}, M =α N → L ∙ M =α L ∙ N
• compatAbs: ∀ {z : Name} {M N : Untyped.Λ}, M =α N → Untyped.Λ.abs z M =α Untyped.Λ.abs z N
• refl: ∀ (M : Untyped.Λ), M =α M
• symm: ∀ {M N : Untyped.Λ}, M =α N → N =α M
• trans: ∀ {L M N : Untyped.Λ}, L =α M → M =α N → L =α N

instance Untyped.Λ.instCoeRenamingAlphaEq {M : Untyped.Λ} {N : Untyped.Λ} : Coe (M.Renaming N) (M =α N)

Equations

• Untyped.Λ.instCoeRenamingAlphaEq = { coe := ⋯ }

def Untyped.Λ.«term_=α_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_=α_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_=α_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =α ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Untyped.Λ.alpha_eq_rename {M : Untyped.Λ} {N : Untyped.Λ} : M.Renaming N → M =α N

@[simp]

theorem Untyped.Λ.alpha_eq_compat_app_left {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (h : M =α N) : M ∙ L =α N ∙ L

@[simp]

theorem Untyped.Λ.alpha_eq_compat_app_right {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (h : M =α N) : L ∙ M =α L ∙ N

@[simp]

theorem Untyped.Λ.alpha_eq_compat_abs {M : Untyped.Λ} {N : Untyped.Λ} {z : Name} (h : M =α N) : Untyped.Λ.abs z M =α Untyped.Λ.abs z N

theorem Untyped.Λ.alpha_eq_refl (M : Untyped.Λ) : M =α M

theorem Untyped.Λ.alpha_eq_symm {M : Untyped.Λ} {N : Untyped.Λ} (h : M =α N) : N =α M

theorem Untyped.Λ.alpha_eq_trans {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (hlm : L =α M) (hmn : M =α N) : L =α N

theorem Untyped.Λ.eq_imp_alpha_eq {M : Untyped.Λ} {N : Untyped.Λ} (h : M = N) : M =α N

instance Untyped.Λ.instIsReflAlphaEq : IsRefl Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =α x2

Equations

• Untyped.Λ.instIsReflAlphaEq = ⋯

instance Untyped.Λ.instIsSymmAlphaEq : IsSymm Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =α x2

Equations

• Untyped.Λ.instIsSymmAlphaEq = ⋯

instance Untyped.Λ.instIsTransAlphaEq : IsTrans Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =α x2

Equations

• Untyped.Λ.instIsTransAlphaEq = ⋯

@[reducible, inline]

abbrev Untyped.Λ.AlphaVariant : Untyped.Λ → Untyped.Λ → Prop

Equations

• Untyped.Λ.AlphaVariant = Untyped.Λ.AlphaEq

def Untyped.Λ.gensym : StateM ℕ Name

Equations

• Untyped.Λ.gensym = getModify Nat.succ <&> toString

def Untyped.Λ.gensymNotIn (fv : Finset Name) : StateM ℕ Name

Equations

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

@[irreducible]

def Untyped.Λ.substGensym (t : Untyped.Λ) (x : Name) (N : Untyped.Λ) : StateM ℕ Untyped.Λ

Equations

• One or more equations did not get rendered due to their size.
• (Untyped.Λ.var a).substGensym x N = pure (if x = a then N else Untyped.Λ.var a)
• (a ∙ a_1).substGensym x N = Seq.seq (Untyped.Λ.app <$> a.substGensym x N) fun (x_1 : Unit) => a_1.substGensym x N

def Untyped.Λ.substGensym' (t : Untyped.Λ) (x : Name) (N : Untyped.Λ) : Untyped.Λ

Equations

• t.substGensym' x N = StateT.run' (t.substGensym x N) 0

def Untyped.Λ.subst (t : Untyped.Λ) (x : Name) (N : Untyped.Λ) : Untyped.Λ

Equations

• (Untyped.Λ.var a).subst x N = if x = a then N else Untyped.Λ.var a
• (a ∙ a_1).subst x N = a.subst x N ∙ a_1.subst x N
• (Untyped.Λ.abs a a_1).subst x N = if x = a ∨ a ∈ N.FV then Untyped.Λ.abs a a_1 else Untyped.Λ.abs a (a_1.subst x N)

def Untyped.Λ.«term_[_:=_,_]» : Lean.TrailingParserDescr

Equations

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

theorem Untyped.Λ.subst_noop {M : Untyped.Λ} {N : Untyped.Λ} {x : Name} (h : x ∉ M.FV) : M.subst x N = M

theorem Untyped.Λ.subst_sequence {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} {x : Name} {y : Name} (h : x ≠ y) (hxm : x ∉ L.FV) : (M.subst x N).subst y L = (M.subst y L).subst x (N.subst y L)

theorem Untyped.Λ.modulo_alpha_eq_app {M : Untyped.Λ} {N : Untyped.Λ} {P : Untyped.Λ} {Q : Untyped.Λ} (hmn : M =α N) (hpq : P =α Q) : M ∙ P =α N ∙ Q

theorem Untyped.Λ.modulo_alpha_eq_abs {M : Untyped.Λ} {N : Untyped.Λ} {x : Name} (h : M =α N) : Untyped.Λ.abs x M =α Untyped.Λ.abs x N

theorem Untyped.Λ.modulo_alpha_eq_subst {M : Untyped.Λ} {N : Untyped.Λ} {P : Untyped.Λ} {Q : Untyped.Λ} {x : Name} (hmn : M =α N) (hpq : P =α Q) : M.subst x P =α N.subst x Q

def Untyped.Λ.reduceβ (t : Untyped.Λ) : Untyped.Λ

Equations

• (Untyped.Λ.abs x M ∙ N).reduceβ = M.subst x N
• (M ∙ N).reduceβ = M.reduceβ ∙ N.reduceβ
• (Untyped.Λ.abs y N).reduceβ = Untyped.Λ.abs y N.reduceβ
• (Untyped.Λ.var name).reduceβ = Untyped.Λ.var name

inductive Untyped.Λ.Beta : Untyped.Λ → Untyped.Λ → Prop

• redex: ∀ {x : Name} (M N : Untyped.Λ), Untyped.Λ.abs x M ∙ N →β M.subst x N
• compatAppLeft: ∀ {L M N : Untyped.Λ}, M →β N → M ∙ L →β N ∙ L
• compatAppRight: ∀ {L M N : Untyped.Λ}, M →β N → L ∙ M →β L ∙ N
• compatAbs: ∀ {x : Name} {M N : Untyped.Λ}, M →β N → Untyped.Λ.abs x M →β Untyped.Λ.abs x N

def Untyped.Λ.«term_→β_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_→β_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_→β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →β ") (Lean.ParserDescr.cat `term 51))

def Untyped.Λ.«term_←β_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_←β_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_←β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ←β ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Untyped.Λ.beta_redex {x : Name} {M : Untyped.Λ} {N : Untyped.Λ} : Untyped.Λ.abs x M ∙ N →β M.subst x N

@[simp]

theorem Untyped.Λ.beta_compat_app_left {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (h : M →β N) : M ∙ L →β N ∙ L

@[simp]

theorem Untyped.Λ.beta_compat_app_right {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (h : M →β N) : L ∙ M →β L ∙ N

@[simp]

theorem Untyped.Λ.beta_compat_abs {x : Name} {M : Untyped.Λ} {N : Untyped.Λ} (h : M →β N) : Untyped.Λ.abs x M →β Untyped.Λ.abs x N

@[reducible, inline]

abbrev Untyped.Λ.BetaChain (a : Untyped.Λ) : Untyped.Λ → Prop

Equations

• Untyped.Λ.BetaChain = Relation.ReflTransGen Untyped.Λ.Beta

def Untyped.Λ.«term_↠β_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_↠β_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_↠β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↠β ") (Lean.ParserDescr.cat `term 51))

def Untyped.Λ.«term_↞β_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_↞β_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_↞β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↞β ") (Lean.ParserDescr.cat `term 51))

theorem Untyped.Λ.BetaChain.extension {M : Untyped.Λ} {N : Untyped.Λ} : M →β N → M ↠β N

instance Untyped.Λ.instCoeBetaBetaChain {M : Untyped.Λ} {N : Untyped.Λ} : Coe (M →β N) (M ↠β N)

Equations

• Untyped.Λ.instCoeBetaBetaChain = { coe := ⋯ }

inductive Untyped.Λ.BetaEq : Untyped.Λ → Untyped.Λ → Prop

• beta: ∀ {M N : Untyped.Λ}, M →β N → M =β N
• betaInv: ∀ {M N : Untyped.Λ}, N →β M → M =β N
• refl: ∀ (M : Untyped.Λ), M =β M
• symm: ∀ {M N : Untyped.Λ}, M =β N → N =β M
• trans: ∀ {L M N : Untyped.Λ}, L =β M → M =β N → L =β N

def Untyped.Λ.«term_=β_» : Lean.TrailingParserDescr

Equations

• Untyped.Λ.«term_=β_» = Lean.ParserDescr.trailingNode `Untyped.Λ.term_=β_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =β ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Untyped.Λ.beta_eq_beta {M : Untyped.Λ} {N : Untyped.Λ} (h : M →β N) : M =β N

@[simp]

theorem Untyped.Λ.beta_eq_beta_inv {M : Untyped.Λ} {N : Untyped.Λ} (h : N →β M) : M =β N

theorem Untyped.Λ.beta_eq_refl (M : Untyped.Λ) : M =β M

theorem Untyped.Λ.beta_eq_symm {M : Untyped.Λ} {N : Untyped.Λ} (h : M =β N) : N =β M

theorem Untyped.Λ.beta_eq_trans {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (hlm : L =β M) (hmn : M =β N) : L =β N

theorem Untyped.Λ.eq_imp_beta_eq {M : Untyped.Λ} {N : Untyped.Λ} (h : M = N) : M =β N

theorem Untyped.Λ.BetaEq.extension {M : Untyped.Λ} {N : Untyped.Λ} : M ↠β N → M =β N

theorem Untyped.Λ.BetaEq.extensionInv {M : Untyped.Λ} {N : Untyped.Λ} : N ↠β M → M =β N

instance Untyped.Λ.instIsReflBetaEq : IsRefl Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =β x2

Equations

• Untyped.Λ.instIsReflBetaEq = ⋯

instance Untyped.Λ.instIsSymmBetaEq : IsSymm Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =β x2

Equations

• Untyped.Λ.instIsSymmBetaEq = ⋯

instance Untyped.Λ.instIsTransBetaEq : IsTrans Untyped.Λ fun (x1 x2 : Untyped.Λ) => x1 =β x2

Equations

• Untyped.Λ.instIsTransBetaEq = ⋯

def Untyped.Λ.isRedex : Untyped.Λ → Prop

Equations

• (Untyped.Λ.abs param body ∙ arg).isRedex = True
• x.isRedex = False

instance Untyped.Λ.instDecidableIsRedex {M : Untyped.Λ} : Decidable M.isRedex

Equations

• Untyped.Λ.instDecidableIsRedex = isFalse ⋯
• Untyped.Λ.instDecidableIsRedex = isFalse ⋯
• Untyped.Λ.instDecidableIsRedex = isFalse ⋯
• Untyped.Λ.instDecidableIsRedex = isTrue ⋯
• Untyped.Λ.instDecidableIsRedex = isFalse ⋯

def Untyped.Λ.inNormalForm : Untyped.Λ → Prop

Equations

• (Untyped.Λ.var a).inNormalForm = True
• (a ∙ a_1).inNormalForm = (¬(a ∙ a_1).isRedex ∧ a.inNormalForm ∧ a_1.inNormalForm)
• (Untyped.Λ.abs a a_1).inNormalForm = a_1.inNormalForm

def Untyped.Λ.hasDecIsNormalForm (M : Untyped.Λ) : Decidable M.inNormalForm

Equations

• One or more equations did not get rendered due to their size.
• (Untyped.Λ.var a).hasDecIsNormalForm = isTrue ⋯
• (Untyped.Λ.abs a a_1).hasDecIsNormalForm = a_1.hasDecIsNormalForm

instance Untyped.Λ.instDecidableInNormalForm {M : Untyped.Λ} : Decidable M.inNormalForm

Equations

• Untyped.Λ.instDecidableInNormalForm = M.hasDecIsNormalForm

def Untyped.Λ.hasNormalForm (M : Untyped.Λ) : Prop

Equations

• M.hasNormalForm = ∃ (N : Untyped.Λ), N.inNormalForm ∧ M =β N

def Untyped.Λ.reduceβAll (t : Untyped.Λ) : Untyped.Λ

Equations

• t.reduceβAll = Untyped.Λ.reduceβAll.loop t t.size

def Untyped.Λ.reduceβAll.loop : Untyped.Λ → ℕ → Untyped.Λ

Equations

• Untyped.Λ.reduceβAll.loop x 0 = x
• Untyped.Λ.reduceβAll.loop x n.succ = if x.reduceβ.inNormalForm then x.reduceβ else Untyped.Λ.reduceβAll.loop x.reduceβ n

@[simp]

theorem Untyped.Λ.nf_beta_imp_eq {M : Untyped.Λ} {N : Untyped.Λ} (h : M.inNormalForm) (hmn : M →β N) : M = N

@[simp]

theorem Untyped.Λ.nf_beta_chain_imp_eq {M : Untyped.Λ} {N : Untyped.Λ} (h : M.inNormalForm) (hmn : M ↠β N) : M = N

theorem Untyped.Λ.nf_beta_chain_imp_alpha_eq {M : Untyped.Λ} {N : Untyped.Λ} (h : M.inNormalForm) (hmn : M ↠β N) : M =α N

@[reducible, inline]

abbrev Untyped.Λ.FiniteReductionPath (a : Untyped.Λ) : Untyped.Λ → Prop

Equations

• Untyped.Λ.FiniteReductionPath = Relation.ReflTransGen Untyped.Λ.Beta

instance Untyped.Λ.instIsReflFiniteReductionPath : IsRefl Untyped.Λ Untyped.Λ.FiniteReductionPath

Equations

• Untyped.Λ.instIsReflFiniteReductionPath = ⋯

instance Untyped.Λ.instIsTransFiniteReductionPath : IsTrans Untyped.Λ Untyped.Λ.FiniteReductionPath

Equations

• Untyped.Λ.instIsTransFiniteReductionPath = ⋯

def Untyped.Λ.isWeaklyNormalizing (M : Untyped.Λ) : Prop

Equations

• M.isWeaklyNormalizing = ∃ (N : Untyped.Λ), N.inNormalForm ∧ M ↠β N

def Untyped.Λ.isStronglyNormalizing (M : Untyped.Λ) : Prop

Equations

• M.isStronglyNormalizing = Acc Untyped.Λ.Beta M

theorem Untyped.Λ.church_rosser {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (hmn : L ↠β M) (hmp : L ↠β N) : ∃ (P : Untyped.Λ), M ↠β P ∧ N ↠β P

theorem Untyped.Λ.church_rosser_corollary {L : Untyped.Λ} {M : Untyped.Λ} {N : Untyped.Λ} (hmn : M =β N) : ∃ (L : Untyped.Λ), M ↠β L ∧ N ↠β L

theorem Untyped.Λ.fixpoint {x : Name} (L : Untyped.Λ) (h : x ∉ L.FV) : ∃ (M : Untyped.Λ), L ∙ M =β M

def Untyped.Λ.toNat? : Untyped.Λ → Option ℕ

Equations

• (Untyped.Λ.abs param (Untyped.Λ.abs param_1 t)).toNat? = Untyped.Λ.toNat?.loop t
• x.toNat? = none

def Untyped.Λ.toNat?.loop (e : Untyped.Λ) : Option ℕ

Equations

• Untyped.Λ.toNat?.loop (Untyped.Λ.var name) = some 0
• Untyped.Λ.toNat?.loop (Untyped.Λ.var name ∙ e') = match Untyped.Λ.toNat?.loop e' with | some n => some (n + 1) | none => none
• Untyped.Λ.toNat?.loop e = none

def Untyped.Λ.toNat! (M : Untyped.Λ) : ℕ

Equations

• M.toNat! = M.toNat?.getD default

def Untyped.Λ.toBool? : Untyped.Λ → Option Bool

Equations

• (Untyped.Λ.abs x_1 (Untyped.Λ.abs y (Untyped.Λ.var z))).toBool? = if x_1 = z then some true else if y = z then some false else none
• x.toBool? = none

def Untyped.Λ.toBool! (M : Untyped.Λ) : Bool

Equations

• M.toBool! = M.toBool?.getD default

def Untyped.Λ.Combinators.Ω : Untyped.Λ

Equations

• Untyped.Λ.Combinators.Ω = Untyped.Λ.abs "x" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "x") ∙ Untyped.Λ.abs "x" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "x")

def Untyped.Λ.Combinators.Δ : Untyped.Λ

Equations

• Untyped.Λ.Combinators.Δ = Untyped.Λ.abs "x" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "x" ∙ Untyped.Λ.var "x")

def Untyped.Λ.Combinators.Y : Untyped.Λ

Equations

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

def Untyped.Λ.Combinators.S : Untyped.Λ

Equations

• Untyped.Λ.Combinators.S = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.abs "z" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "z" ∙ (Untyped.Λ.var "y" ∙ Untyped.Λ.var "z"))))

def Untyped.Λ.Combinators.K : Untyped.Λ

Equations

• Untyped.Λ.Combinators.K = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.var "x"))

def Untyped.Λ.Combinators.I : Untyped.Λ

Equations

• Untyped.Λ.Combinators.I = Untyped.Λ.abs "x" (Untyped.Λ.var "x")

def Untyped.Λ.Combinators.B : Untyped.Λ

Equations

• Untyped.Λ.Combinators.B = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.abs "z" (Untyped.Λ.var "x" ∙ (Untyped.Λ.var "y" ∙ Untyped.Λ.var "z"))))

def Untyped.Λ.Combinators.C : Untyped.Λ

Equations

• Untyped.Λ.Combinators.C = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.abs "z" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "z" ∙ Untyped.Λ.var "y")))

def Untyped.Λ.Combinators.W : Untyped.Λ

Equations

• Untyped.Λ.Combinators.W = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.var "x" ∙ Untyped.Λ.var "y" ∙ Untyped.Λ.var "y"))

def Untyped.Λ.Combinators.zero : Untyped.Λ

Equations

• Untyped.Λ.Combinators.zero = Untyped.Λ.abs "f" (Untyped.Λ.abs "x" (Untyped.Λ.var "x"))

def Untyped.Λ.Combinators.one : Untyped.Λ

Equations

• Untyped.Λ.Combinators.one = Untyped.Λ.abs "f" (Untyped.Λ.abs "x" (Untyped.Λ.var "f" ∙ Untyped.Λ.var "x"))

def Untyped.Λ.Combinators.two : Untyped.Λ

Equations

• Untyped.Λ.Combinators.two = Untyped.Λ.abs "f" (Untyped.Λ.abs "x" (Untyped.Λ.var "f" ∙ (Untyped.Λ.var "f" ∙ Untyped.Λ.var "x")))

def Untyped.Λ.Combinators.three : Untyped.Λ

Equations

• Untyped.Λ.Combinators.three = Untyped.Λ.abs "f" (Untyped.Λ.abs "x" (Untyped.Λ.var "f" ∙ (Untyped.Λ.var "f" ∙ (Untyped.Λ.var "f" ∙ Untyped.Λ.var "x"))))

def Untyped.Λ.Combinators.add : Untyped.Λ

Equations

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

def Untyped.Λ.Combinators.mul : Untyped.Λ

Equations

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

def Untyped.Λ.Combinators.suc : Untyped.Λ

Equations

• Untyped.Λ.Combinators.suc = Untyped.Λ.abs "m" (Untyped.Λ.abs "f" (Untyped.Λ.abs "x" (Untyped.Λ.var "f" ∙ (Untyped.Λ.var "m" ∙ Untyped.Λ.var "f" ∙ Untyped.Λ.var "x"))))

def Untyped.Λ.Combinators.true : Untyped.Λ

Equations

• Untyped.Λ.Combinators.true = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.var "x"))

def Untyped.Λ.Combinators.false : Untyped.Λ

Equations

• Untyped.Λ.Combinators.false = Untyped.Λ.abs "x" (Untyped.Λ.abs "y" (Untyped.Λ.var "y"))

def Untyped.Λ.Combinators.not : Untyped.Λ

Equations

• Untyped.Λ.Combinators.not = Untyped.Λ.abs "z" (Untyped.Λ.var "z" ∙ Untyped.Λ.Combinators.false ∙ Untyped.Λ.Combinators.true)