Lambda Calculus in Lean

3. Confluence and Normal Forms🔗

import LeanLambda.Untyped.Namednamespace Untyped.DB

3.1. Confluence🔗

Two reduction sequences starting from the same term should always be able to meet again:

\frac{t \to_\beta^* u \qquad t \to_\beta^* v} {\exists w.\ u \to_\beta^* w \land v \to_\beta^* w}.

We prove this through parallel reduction. A parallel step may reduce several redexes at once. Ordinary and parallel reduction will be related afterwards; we first prove that parallel reduction itself is confluent.

inductive Parallel : DB → DB → Prop where | bound : Parallel (.bound n) (.bound n) | free : Parallel (.free x) (.free x) | lam : Parallel body body' → Parallel (.lam body) (.lam body') | app : Parallel fn fn' → Parallel arg arg' → Parallel (.app fn arg) (.app fn' arg') | beta : Parallel body body' → Parallel arg arg' → Parallel (.app (.lam body) arg) (subst 0 arg' body')infix:50 " ⇉βᵇ " => Parallelabbrev ParallelStar := Relation.ReflTransGen Parallelinfix:50 " ⇉βᵇ* " => ParallelStar@[grind .] theorem Parallel.refl {t} : t ⇉βᵇ t := t:DB⊢ t ⇉βᵇ t index✝:ℕ⊢ DB.bound index✝ ⇉βᵇ DB.bound index✝x✝:String⊢ DB.free x✝ ⇉βᵇ DB.free x✝body✝:DBbody_ih✝:body✝ ⇉βᵇ body✝⊢ body✝.lam ⇉βᵇ body✝.lamfn✝:DBarg✝:DBfn_ih✝:fn✝ ⇉βᵇ fn✝arg_ih✝:arg✝ ⇉βᵇ arg✝⊢ fn✝.app arg✝ ⇉βᵇ fn✝.app arg✝ index✝:ℕ⊢ DB.bound index✝ ⇉βᵇ DB.bound index✝x✝:String⊢ DB.free x✝ ⇉βᵇ DB.free x✝body✝:DBbody_ih✝:body✝ ⇉βᵇ body✝⊢ body✝.lam ⇉βᵇ body✝.lamfn✝:DBarg✝:DBfn_ih✝:fn✝ ⇉βᵇ fn✝arg_ih✝:arg✝ ⇉βᵇ arg✝⊢ fn✝.app arg✝ ⇉βᵇ fn✝.app arg✝ All goals completed! 🐙

First, ordinary beta reduction and parallel reduction have the same finite reduction sequences. An ordinary step is a parallel step that happens to contract only one redex. Conversely, a parallel step can be serialized into ordinary steps. For the latter direction we use the familiar fact that a sequence of reductions may be performed beneath a lambda or in both parts of an application.

theorem BetaStep.to_parallel : (t →βᵇ t') → (t ⇉βᵇ t') := t:DBt':DB⊢ t →βᵇ t' → t ⇉βᵇ t' t:DBt':DBhstep:t →βᵇ t'⊢ t ⇉βᵇ t'; t:DBt':DBbody✝:DBarg✝:DB⊢ body✝.lam.app arg✝ ⇉βᵇ subst 0 arg✝ body✝t:DBt':DBf✝:DBf'✝:DBa✝¹:DBa✝:f✝ →βᵇ f'✝a_ih✝:f✝ ⇉βᵇ f'✝⊢ f✝.app a✝¹ ⇉βᵇ f'✝.app a✝¹t:DBt':DBa✝¹:DBa'✝:DBf✝:DBa✝:a✝¹ →βᵇ a'✝a_ih✝:a✝¹ ⇉βᵇ a'✝⊢ f✝.app a✝¹ ⇉βᵇ f✝.app a'✝t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ →βᵇ body'✝a_ih✝:body✝ ⇉βᵇ body'✝⊢ body✝.lam ⇉βᵇ body'✝.lam t:DBt':DBbody✝:DBarg✝:DB⊢ body✝.lam.app arg✝ ⇉βᵇ subst 0 arg✝ body✝t:DBt':DBf✝:DBf'✝:DBa✝¹:DBa✝:f✝ →βᵇ f'✝a_ih✝:f✝ ⇉βᵇ f'✝⊢ f✝.app a✝¹ ⇉βᵇ f'✝.app a✝¹t:DBt':DBa✝¹:DBa'✝:DBf✝:DBa✝:a✝¹ →βᵇ a'✝a_ih✝:a✝¹ ⇉βᵇ a'✝⊢ f✝.app a✝¹ ⇉βᵇ f✝.app a'✝t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ →βᵇ body'✝a_ih✝:body✝ ⇉βᵇ body'✝⊢ body✝.lam ⇉βᵇ body'✝.lam All goals completed! 🐙theorem Parallel.to_beta : (t ⇉βᵇ t') → (t →βᵇ* t') := t:DBt':DB⊢ t ⇉βᵇ t' → t →βᵇ* t' t:DBt':DBhstep:t ⇉βᵇ t'⊢ t →βᵇ* t'; t:DBt':DBn✝:ℕ⊢ DB.bound n✝ →βᵇ* DB.bound n✝t:DBt':DBx✝:String⊢ DB.free x✝ →βᵇ* DB.free x✝t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:body✝ →βᵇ* body'✝⊢ body✝.lam →βᵇ* body'✝.lamt:DBt':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:fn✝ →βᵇ* fn'✝a_ih✝:arg✝ →βᵇ* arg'✝⊢ fn✝.app arg✝ →βᵇ* fn'✝.app arg'✝t:DBt':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:body✝ →βᵇ* body'✝a_ih✝:arg✝ →βᵇ* arg'✝⊢ body✝.lam.app arg✝ →βᵇ* subst 0 arg'✝ body'✝ t:DBt':DBn✝:ℕ⊢ DB.bound n✝ →βᵇ* DB.bound n✝t:DBt':DBx✝:String⊢ DB.free x✝ →βᵇ* DB.free x✝t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:body✝ →βᵇ* body'✝⊢ body✝.lam →βᵇ* body'✝.lamt:DBt':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:fn✝ →βᵇ* fn'✝a_ih✝:arg✝ →βᵇ* arg'✝⊢ fn✝.app arg✝ →βᵇ* fn'✝.app arg'✝t:DBt':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:body✝ →βᵇ* body'✝a_ih✝:arg✝ →βᵇ* arg'✝⊢ body✝.lam.app arg✝ →βᵇ* subst 0 arg'✝ body'✝ All goals completed! 🐙theorem BetaStar.to_parallel : (t →βᵇ* t') → (t ⇉βᵇ* t') := t:DBt':DB⊢ t →βᵇ* t' → t ⇉βᵇ* t' t:DBt':DBhsteps:t →βᵇ* t'⊢ t ⇉βᵇ* t'; t:DBt':DB⊢ t ⇉βᵇ* tt:DBt':DBb✝:DBc✝:DBa✝¹:Relation.ReflTransGen BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:t ⇉βᵇ* b✝⊢ t ⇉βᵇ* c✝ t:DBt':DB⊢ t ⇉βᵇ* tt:DBt':DBb✝:DBc✝:DBa✝¹:Relation.ReflTransGen BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:t ⇉βᵇ* b✝⊢ t ⇉βᵇ* c✝ All goals completed! 🐙theorem ParallelStar.to_beta : (t ⇉βᵇ* t') → (t →βᵇ* t') := t:DBt':DB⊢ t ⇉βᵇ* t' → t →βᵇ* t' t:DBt':DBhsteps:t ⇉βᵇ* t'⊢ t →βᵇ* t'; t:DBt':DB⊢ t →βᵇ* tt:DBt':DBb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:t →βᵇ* b✝⊢ t →βᵇ* c✝ t:DBt':DB⊢ t →βᵇ* tt:DBt':DBb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:t →βᵇ* b✝⊢ t →βᵇ* c✝ All goals completed! 🐙

Second, parallel reduction has the diamond property. Its proof uses the complete development of a term, which contracts every redex already present in that term.

@[simp] def complete : DB → DB | .bound n => .bound n | .free x => .free x | .lam body => .lam (complete body) | .app (.lam body) arg => subst 0 (complete arg) (complete body) | .app fn arg => .app (complete fn) (complete arg)

Every parallel reduct of t takes one further parallel step to complete t. Its beta case uses the substitution lemma below: reducing the body and the argument in parallel also reduces their contracta in parallel.

theorem Parallel.shift (hstep : t ⇉βᵇ t') : shiftAbove cutoff t ⇉βᵇ shiftAbove cutoff t' := t:DBt':DBcutoff:ℕhstep:t ⇉βᵇ t'⊢ shiftAbove cutoff t ⇉βᵇ shiftAbove cutoff t' t:DBt':DBn✝:ℕcutoff:ℕ⊢ shiftAbove cutoff (DB.bound n✝) ⇉βᵇ shiftAbove cutoff (DB.bound n✝)t:DBt':DBx✝:Stringcutoff:ℕ⊢ shiftAbove cutoff (DB.free x✝) ⇉βᵇ shiftAbove cutoff (DB.free x✝)t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff body✝ ⇉βᵇ shiftAbove cutoff body'✝cutoff:ℕ⊢ shiftAbove cutoff body✝.lam ⇉βᵇ shiftAbove cutoff body'✝.lamt:DBt':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {cutoff : ℕ}, shiftAbove cutoff fn✝ ⇉βᵇ shiftAbove cutoff fn'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff arg✝ ⇉βᵇ shiftAbove cutoff arg'✝cutoff:ℕ⊢ shiftAbove cutoff (fn✝.app arg✝) ⇉βᵇ shiftAbove cutoff (fn'✝.app arg'✝)t:DBt':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {cutoff : ℕ}, shiftAbove cutoff body✝ ⇉βᵇ shiftAbove cutoff body'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff arg✝ ⇉βᵇ shiftAbove cutoff arg'✝cutoff:ℕ⊢ shiftAbove cutoff (body✝.lam.app arg✝) ⇉βᵇ shiftAbove cutoff (subst 0 arg'✝ body'✝) t:DBt':DBn✝:ℕcutoff:ℕ⊢ shiftAbove cutoff (DB.bound n✝) ⇉βᵇ shiftAbove cutoff (DB.bound n✝)t:DBt':DBx✝:Stringcutoff:ℕ⊢ shiftAbove cutoff (DB.free x✝) ⇉βᵇ shiftAbove cutoff (DB.free x✝)t:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff body✝ ⇉βᵇ shiftAbove cutoff body'✝cutoff:ℕ⊢ shiftAbove cutoff body✝.lam ⇉βᵇ shiftAbove cutoff body'✝.lamt:DBt':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {cutoff : ℕ}, shiftAbove cutoff fn✝ ⇉βᵇ shiftAbove cutoff fn'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff arg✝ ⇉βᵇ shiftAbove cutoff arg'✝cutoff:ℕ⊢ shiftAbove cutoff (fn✝.app arg✝) ⇉βᵇ shiftAbove cutoff (fn'✝.app arg'✝)t:DBt':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {cutoff : ℕ}, shiftAbove cutoff body✝ ⇉βᵇ shiftAbove cutoff body'✝a_ih✝:∀ {cutoff : ℕ}, shiftAbove cutoff arg✝ ⇉βᵇ shiftAbove cutoff arg'✝cutoff:ℕ⊢ shiftAbove cutoff (body✝.lam.app arg✝) ⇉βᵇ shiftAbove cutoff (subst 0 arg'✝ body'✝) All goals completed! 🐙theorem Parallel.subst (hbody : body ⇉βᵇ body') (harg : arg ⇉βᵇ arg') : subst j arg body ⇉βᵇ subst j arg' body' := body:DBbody':DBarg:DBarg':DBj:ℕhbody:body ⇉βᵇ body'harg:arg ⇉βᵇ arg'⊢ DB.subst j arg body ⇉βᵇ DB.subst j arg' body' body:DBbody':DBn✝:ℕarg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (DB.bound n✝) ⇉βᵇ DB.subst j arg' (DB.bound n✝)body:DBbody':DBx✝:Stringarg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (DB.free x✝) ⇉βᵇ DB.subst j arg' (DB.free x✝)body:DBbody':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg body✝ ⇉βᵇ DB.subst j arg' body'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg body✝.lam ⇉βᵇ DB.subst j arg' body'✝.lambody:DBbody':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg fn✝ ⇉βᵇ DB.subst j arg' fn'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg arg✝ ⇉βᵇ DB.subst j arg' arg'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (fn✝.app arg✝) ⇉βᵇ DB.subst j arg' (fn'✝.app arg'✝)body:DBbody':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg body✝ ⇉βᵇ DB.subst j arg' body'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg arg✝ ⇉βᵇ DB.subst j arg' arg'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (body✝.lam.app arg✝) ⇉βᵇ DB.subst j arg' (DB.subst 0 arg'✝ body'✝) body:DBbody':DBn✝:ℕarg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (DB.bound n✝) ⇉βᵇ DB.subst j arg' (DB.bound n✝)body:DBbody':DBx✝:Stringarg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (DB.free x✝) ⇉βᵇ DB.subst j arg' (DB.free x✝)body:DBbody':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg body✝ ⇉βᵇ DB.subst j arg' body'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg body✝.lam ⇉βᵇ DB.subst j arg' body'✝.lambody:DBbody':DBfn✝:DBfn'✝:DBarg✝:DBarg'✝:DBa✝¹:fn✝ ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg fn✝ ⇉βᵇ DB.subst j arg' fn'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg arg✝ ⇉βᵇ DB.subst j arg' arg'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (fn✝.app arg✝) ⇉βᵇ DB.subst j arg' (fn'✝.app arg'✝)body:DBbody':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg body✝ ⇉βᵇ DB.subst j arg' body'✝a_ih✝:∀ {arg arg' : DB} {j : ℕ}, arg ⇉βᵇ arg' → DB.subst j arg arg✝ ⇉βᵇ DB.subst j arg' arg'✝arg:DBarg':DBj:ℕharg:arg ⇉βᵇ arg'⊢ DB.subst j arg (body✝.lam.app arg✝) ⇉βᵇ DB.subst j arg' (DB.subst 0 arg'✝ body'✝) All goals completed! 🐙theorem Parallel.to_complete (hstep : t ⇉βᵇ t') : t' ⇉βᵇ complete t := t:DBt':DBhstep:t ⇉βᵇ t'⊢ t' ⇉βᵇ t.complete induction hstep with t:DBt':DBfn:DBfn'✝:DBarg✝:DBarg'✝:DBhfn:fn ⇉βᵇ fn'✝a✝:arg✝ ⇉βᵇ arg'✝ihfn:fn'✝ ⇉βᵇ fn.completea_ih✝:arg'✝ ⇉βᵇ arg✝.complete⊢ fn'✝.app arg'✝ ⇉βᵇ (fn.app arg✝).complete cases fn with t:DBt':DBfn'✝:DBarg✝:DBarg'✝:DBa✝:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completebody:DBhfn:body.lam ⇉βᵇ fn'✝ihfn:fn'✝ ⇉βᵇ body.lam.complete⊢ fn'✝.app arg'✝ ⇉βᵇ (body.lam.app arg✝).complete t:DBt':DBarg✝:DBarg'✝:DBa✝¹:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completebody:DBbody'✝:DBa✝:body ⇉βᵇ body'✝ihfn:body'✝.lam ⇉βᵇ body.lam.complete⊢ body'✝.lam.app arg'✝ ⇉βᵇ (body.lam.app arg✝).complete; t:DBt':DBarg✝:DBarg'✝:DBa✝²:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completebody:DBbody'✝:DBa✝¹:body ⇉βᵇ body'✝a✝:body'✝ ⇉βᵇ body.complete⊢ body'✝.lam.app arg'✝ ⇉βᵇ (body.lam.app arg✝).complete; All goals completed! 🐙 t:DBt':DBfn'✝:DBarg✝¹:DBarg'✝:DBa✝:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completefn✝:DBarg✝:DBhfn:fn✝.app arg✝ ⇉βᵇ fn'✝ihfn:fn'✝ ⇉βᵇ (fn✝.app arg✝).complete⊢ fn'✝.app arg'✝ ⇉βᵇ ((fn✝.app arg✝).app arg✝¹).completet:DBt':DBfn'✝:DBarg✝:DBarg'✝:DBa✝:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completex✝:Stringhfn:DB.free x✝ ⇉βᵇ fn'✝ihfn:fn'✝ ⇉βᵇ (DB.free x✝).complete⊢ fn'✝.app arg'✝ ⇉βᵇ ((DB.free x✝).app arg✝).completet:DBt':DBfn'✝:DBarg✝:DBarg'✝:DBa✝:arg✝ ⇉βᵇ arg'✝a_ih✝:arg'✝ ⇉βᵇ arg✝.completeindex✝:ℕhfn:DB.bound index✝ ⇉βᵇ fn'✝ihfn:fn'✝ ⇉βᵇ (DB.bound index✝).complete⊢ fn'✝.app arg'✝ ⇉βᵇ ((DB.bound index✝).app arg✝).complete All goals completed! 🐙 t:DBt':DBbody✝:DBbody'✝:DBarg✝:DBarg'✝:DBa✝¹:body✝ ⇉βᵇ body'✝a✝:arg✝ ⇉βᵇ arg'✝a_ih✝¹:body'✝ ⇉βᵇ body✝.completea_ih✝:arg'✝ ⇉βᵇ arg✝.complete⊢ DB.subst 0 arg'✝ body'✝ ⇉βᵇ (body✝.lam.app arg✝).completet:DBt':DBbody✝:DBbody'✝:DBa✝:body✝ ⇉βᵇ body'✝a_ih✝:body'✝ ⇉βᵇ body✝.complete⊢ body'✝.lam ⇉βᵇ body✝.lam.completet:DBt':DBx✝:String⊢ DB.free x✝ ⇉βᵇ (DB.free x✝).completet:DBt':DBn✝:ℕ⊢ DB.bound n✝ ⇉βᵇ (DB.bound n✝).complete All goals completed! 🐙theorem parallel_diamond (hleft : t ⇉βᵇ left) (hright : t ⇉βᵇ right) : ∃ join, left ⇉βᵇ join ∧ right ⇉βᵇ join := t:DBleft:DBright:DBhleft:t ⇉βᵇ lefthright:t ⇉βᵇ right⊢ ∃ join, left ⇉βᵇ join ∧ right ⇉βᵇ join t:DBleft:DBright:DBhleft:t ⇉βᵇ lefthright:t ⇉βᵇ right⊢ left ⇉βᵇ t.complete ∧ right ⇉βᵇ t.complete; All goals completed! 🐙

The strip lemma extends the one-step diamond to a finite sequence.

theorem parallel_strip (hleft : t ⇉βᵇ left) (hright : t ⇉βᵇ* right) : ∃ join, left ⇉βᵇ* join ∧ right ⇉βᵇ join := t:DBleft:DBright:DBhleft:t ⇉βᵇ lefthright:t ⇉βᵇ* right⊢ ∃ join, left ⇉βᵇ* join ∧ right ⇉βᵇ join t:DBleft:DBright:DBhleft:t ⇉βᵇ left⊢ ∃ join, left ⇉βᵇ* join ∧ t ⇉βᵇ joint:DBleft:DBright:DBhleft:t ⇉βᵇ leftb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:∃ join, left ⇉βᵇ* join ∧ b✝ ⇉βᵇ join⊢ ∃ join, left ⇉βᵇ* join ∧ c✝ ⇉βᵇ join t:DBleft:DBright:DBhleft:t ⇉βᵇ left⊢ ∃ join, left ⇉βᵇ* join ∧ t ⇉βᵇ joint:DBleft:DBright:DBhleft:t ⇉βᵇ leftb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:∃ join, left ⇉βᵇ* join ∧ b✝ ⇉βᵇ join⊢ ∃ join, left ⇉βᵇ* join ∧ c✝ ⇉βᵇ join All goals completed! 🐙theorem parallel_confluence (hleft : t ⇉βᵇ* left) (hright : t ⇉βᵇ* right) : ∃ join, left ⇉βᵇ* join ∧ right ⇉βᵇ* join := t:DBleft:DBright:DBhleft:t ⇉βᵇ* lefthright:t ⇉βᵇ* right⊢ ∃ join, left ⇉βᵇ* join ∧ right ⇉βᵇ* join t:DBleft:DBright:DBhright:t ⇉βᵇ* right⊢ ∃ join, t ⇉βᵇ* join ∧ right ⇉βᵇ* joint:DBleft:DBright:DBhright:t ⇉βᵇ* rightb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:∃ join, b✝ ⇉βᵇ* join ∧ right ⇉βᵇ* join⊢ ∃ join, c✝ ⇉βᵇ* join ∧ right ⇉βᵇ* join t:DBleft:DBright:DBhright:t ⇉βᵇ* right⊢ ∃ join, t ⇉βᵇ* join ∧ right ⇉βᵇ* joint:DBleft:DBright:DBhright:t ⇉βᵇ* rightb✝:DBc✝:DBa✝¹:Relation.ReflTransGen Parallel t b✝a✝:b✝ ⇉βᵇ c✝a_ih✝:∃ join, b✝ ⇉βᵇ* join ∧ right ⇉βᵇ* join⊢ ∃ join, c✝ ⇉βᵇ* join ∧ right ⇉βᵇ* join All goals completed! 🐙

The desired theorem now follows immediately: translate both reductions to parallel reductions, join them there, and translate the two joining reductions back to ordinary beta reduction.

theorem confluence (hleft : t →βᵇ* left) (hright : t →βᵇ* right) : ∃ join, left →βᵇ* join ∧ right →βᵇ* join := t:DBleft:DBright:DBhleft:t →βᵇ* lefthright:t →βᵇ* right⊢ ∃ join, left →βᵇ* join ∧ right →βᵇ* join All goals completed! 🐙

3.1.1. Uniqueness of Normal Forms🔗

Confluence implies that normal forms are unique. First observe that a normal form cannot reduce to a different term: a nonempty reduction sequence would have to begin with a beta step, but by definition no such step exists.

@[grind .] theorem Normal.eq_of_steps (hnormal : Normal t) (hsteps : t →βᵇ* u) : u = t := t:DBu:DBhnormal:t.Normalhsteps:t →βᵇ* u⊢ u = t t:DBu:DBhnormal:t.Normal⊢ t = tt:DBu:DBhnormal:t.Normalb✝:DBc✝:DBa✝¹:Relation.ReflTransGen BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:b✝ = t⊢ c✝ = t t:DBu:DBhnormal:t.Normal⊢ t = tt:DBu:DBhnormal:t.Normalb✝:DBc✝:DBa✝¹:Relation.ReflTransGen BetaStep t b✝a✝:b✝ →βᵇ c✝a_ih✝:b✝ = t⊢ c✝ = t All goals completed! 🐙

Now suppose that two normal forms are reachable from the same term. Confluence gives them a common reduct. Since neither normal form can reduce any further, that common reduct must be both of them.

theorem normal_form_unique : t →βᵇ* left → Normal left → t →βᵇ* right → Normal right → left = right := t:DBleft:DBright:DB⊢ t →βᵇ* left → left.Normal → t →βᵇ* right → right.Normal → left = right All goals completed! 🐙end Untyped.DBnamespace Untyped.Term

Named normal forms are unique up to alpha-equivalence rather than literal equality: changing the names of bound variables does not change the term's de Bruijn representation.

theorem normal_form_unique : e →β* left → Normal left → e →β* right → Normal right → left =α right := DB.normal_form_uniqueend Untyped.Term