/-- Untyped λ-terms with **de Bruijn indices**: `var n` refers to the variable bound by the`n`-th enclosing `lam`, counting outwards from `0`. So `λx. λy. x` is `lam (lam (var 1))`, andα-equivalent terms such as `λx. x` and `λy. y` are the same term `lam (var 0)`. -/inductive Term where | var : Nat → Term | app : Term → Term → Term | lam : Term → Term deriving DecidableEq, Repr
/-- Lift a renaming `ξ` of variables under one binder: index `0` (the new bound variable) stays,and every other index `n + 1` goes to `ξ n + 1`. -/def upRen (ξ : Nat → Nat) : Nat → Nat | 0 => 0 | n + 1 => ξ n + 1
/-- Rename the free variables of a term by `ξ`. -/def rename (ξ : Nat → Nat) : Term → Term | var n => var (ξ n) | app s t => app (rename ξ s) (rename ξ t) | lam t => lam (rename (upRen ξ) t)
/-- Lift a substitution `σ` (a term for each free variable) under one binder: the new boundvariable stays put, and the substituted terms are shifted so that their free variables skip thenew binder. This shift is exactly what makes substitution **capture-avoiding**. -/def up (σ : Nat → Term) : Nat → Term | 0 => var 0 | n + 1 => rename Nat.succ (σ n)
/-- Simultaneous capture-avoiding substitution: replace each free variable `n` by `σ n`. -/def subst (σ : Nat → Term) : Term → Term | var n => σ n | app s t => app (subst σ s) (subst σ t) | lam t => lam (subst (up σ) t)
/-- `inst t s` is `t[s/x]` for the variable `x` bound by an enclosing `λ`: index `0` becomes`s`, and the other free indices drop by one because that `λ` has disappeared. -/def inst (t s : Term) : Term := subst (scons s var) t
rename_renametheoremProved here from basic factspropext, Quot.sound
rename_renameLean 4Proved here from basic factsFormally verified
/-- Renaming twice is renaming once by the composite. -/theorem rename_rename (t : Term) : ∀ (ξ ζ : Nat → Nat), rename ξ (rename ζ t) = rename (ξ ∘ ζ) t := by induction t with | var n => intro ξ ζ; rfl | app s t ihs iht => intro ξ ζ; simp [rename, ihs, iht] | lam t ih => intro ξ ζ simp only [rename, ih] congr 2 funext n cases n <;> rfl
subst_vartheoremProved here from basic factspropext
subst_varLean 4Proved here from basic factsFormally verified
/-- Substituting every variable by itself does nothing. -/theorem subst_var (t : Term) : ∀ (σ : Nat → Term), (∀ n, σ n = var n) → subst σ t = t := by induction t with | var n => intro σ h; exact h n | app s t ihs iht => intro σ h; simp [subst, ihs σ h, iht σ h] | lam t ih => intro σ h simp only [subst] rw [ih] intro n cases n with | zero => rfl | succ k => simp [up, h k, rename]
rename_insttheoremProved here from basic factspropext, Quot.sound
rename_instLean 4Proved here from basic factsFormally verified
/-- Renaming commutes with instantiation (renaming under the binder on the left). -/theorem rename_inst (ξ : Nat → Nat) (t s : Term) : rename ξ (inst t s) = inst (rename (upRen ξ) t) (rename ξ s) := by simp only [inst, rename_subst, subst_rename] congr 1 funext n cases n <;> rfl
/-- One step of **β-reduction**, anywhere in a term: `(λx. t) s → t[s/x]`, also insideapplications and under λ. -/inductive Step : Term → Term → Prop where | beta (t s : Term) : Step (app (lam t) s) (inst t s) | appL {s s' : Term} (t : Term) : Step s s' → Step (app s t) (app s' t) | appR (s : Term) {t t' : Term} : Step t t' → Step (app s t) (app s t') | lam {t t' : Term} : Step t t' → Step (lam t) (lam t')
steps_apptheoremProved here from basic factsNo axioms
steps_appLean 4Proved here from basic factsFormally verified
/-- Many-step reduction `↠` (the reflexive–transitive closure `ReflTransGen Step`) is acongruence for application. -/theorem steps_app {s s' t t' : Term} (hs : ReflTransGen Step s s') (ht : ReflTransGen Step t t') : ReflTransGen Step (app s t) (app s' t') := (hs.lift (fun x => app x t) fun _ _ h => Step.appL t h).trans (ht.lift (fun y => app s' y) fun _ _ h => Step.appR s' h)
omega_normaltheoremProved here from basic factsNo axioms
omega_normalLean 4Proved here from basic factsFormally verified
/-- `ω = λx. x x` itself is in normal form: its body `x x` is an application of a variable,which is not a redex. -/theorem omega_normal : Normal omega := by intro u h cases h with | lam h' => cases h' with | appL _ h'' => cases h'' | appR _ h'' => cases h''
bigOmega_steptheoremProved here from basic factsNo axioms
bigOmega_stepLean 4Proved here from basic factsFormally verified
/-- **Ω reduces to itself and to nothing else.** The only redex is the whole term, andcontracting it substitutes `ω` for `x` in `x x`, giving `ω ω` back. -/theorem bigOmega_step (u : Term) : Step bigOmega u ↔ u = bigOmega := by constructor · intro h cases h with | beta => rfl | appL _ h' => exact absurd h' (omega_normal _) | appR _ h' => exact absurd h' (omega_normal _) · rintro rfl exact Step.beta _ _
bigOmega_no_normal_formtheoremProved here from basic factsNo axioms
bigOmega_no_normal_formLean 4Proved here from basic factsFormally verified
/-- **Ω has no normal form**: everything it reduces to is Ω, and Ω is not normal. So the untypedλ-calculus has non-terminating computations. -/theorem bigOmega_no_normal_form : ¬ ∃ u, ReflTransGen Step bigOmega u ∧ Normal u := by rintro ⟨u, hu, hn⟩ have only : ∀ w, ReflTransGen Step bigOmega w → w = bigOmega := by intro w hw induction hw with | refl => rfl | tail _ hstep ih => subst ih exact (bigOmega_step _).1 hstep have := only u hu subst this exact hn bigOmega ((bigOmega_step bigOmega).2 rfl)
theta_fixed_pointtheoremProved here from basic factsNo axioms
theta_fixed_pointLean 4Proved here from basic factsFormally verified
/-- **`Θ F ↠ F (Θ F)` for every term `F`** — in two β-steps. This is how the untyped calculusdefines recursive functions: a solution of `f = F f`. -/theorem theta_fixed_point (F : Term) : ReflTransGen Step (app theta F) (app F (app theta F)) := by refine ReflTransGen.head (Step.appL F (Step.beta _ _)) ?_ exact ReflTransGen.single (Step.beta _ _)
curryY_fixed_pointtheoremProved here from basic factspropext, Quot.sound
curryY_fixed_pointLean 4Proved here from basic factsFormally verified
/-- **`Y F` and `F (Y F)` reduce to a common term**, so they are β-equal. (Unlike `Θ`, `Y F`does not reduce to `F (Y F)` itself.) With `W = λx. F (x x)`: `Y F → W W → F (W W)` and`F (Y F) → F (W W)`. -/theorem curryY_fixed_point (F : Term) : ∃ N, ReflTransGen Step (app curryY F) N ∧ ReflTransGen Step (app F (app curryY F)) N := by let W : Term := lam (app (rename Nat.succ F) (app (var 0) (var 0))) have h1 : Step (app curryY F) (app W W) := Step.beta _ _ have h2 : Step (app W W) (app F (app W W)) := by have e : inst (app (rename Nat.succ F) (app (var 0) (var 0))) W = app F (app W W) := by simp only [inst, subst] rw [subst_rename, subst_var] · rfl · intro n rfl rw [← e] exact Step.beta _ _ exact ⟨app F (app W W), ReflTransGen.head h1 (ReflTransGen.single h2), ReflTransGen.single (Step.appR F h1)⟩
/-- `iterate n = f (f (… (f x)))` with `n` copies of `f`, where `f` is index `1` and `x` isindex `0`. -/def iterate : Nat → Term | 0 => var 0 | n + 1 => app (var 1) (iterate n)
/-- One step of **normal-order** (leftmost-outermost) reduction, or `none` if the term isnormal: contract the head redex if there is one, otherwise reduce inside, left to right. -/def stepNO : Term → Option Term | var _ => none | lam t => (stepNO t).map lam | app (lam t) s => some (inst t s) | app (var n) t => (stepNO t).map (app (var n)) | app (app s₁ s₂) t => match stepNO (app s₁ s₂) with | some s' => some (app s' t) | none => (stepNO t).map (app (app s₁ s₂))
/-- Run normal-order reduction for at most `fuel` steps. -/def normalize : Nat → Term → Term | 0, t => t | fuel + 1, t => match stepNO t with | some u => normalize fuel u | none => t
stepNO_soundtheoremProved here from basic factspropext, Quot.sound
stepNO_soundLean 4Proved here from basic factsFormally verified
/-- **The evaluator is sound**: every step it takes is a β-step. -/theorem stepNO_sound (t : Term) : ∀ u, stepNO t = some u → Step t u := by induction t with | var n => intro u h; cases h | lam t ih => intro u h simp only [stepNO, Option.map_eq_some_iff] at h obtain ⟨t', ht', rfl⟩ := h exact Step.lam (ih t' ht') | app s t ihs iht => intro u h cases s with | var n => simp only [stepNO, Option.map_eq_some_iff] at h obtain ⟨t', ht', rfl⟩ := h exact Step.appR _ (iht t' ht') | lam s₀ => simp only [stepNO, Option.some.injEq] at h subst h exact Step.beta _ _ | app s₁ s₂ => simp only [stepNO] at h split at h · rename_i s' hs' simp only [Option.some.injEq] at h subst h exact Step.appL _ (ihs s' hs') · simp only [Option.map_eq_some_iff] at h obtain ⟨t', ht', rfl⟩ := h exact Step.appR _ (iht t' ht')
stepNO_nonetheoremProved here from basic factspropext
stepNO_noneLean 4Proved here from basic factsFormally verified
/-- **When the evaluator stops, the term is normal**: if normal order finds no redex, there isno redex at all. -/theorem stepNO_none (t : Term) : stepNO t = none → Normal t := by induction t with | var n => intro _ u h; cases h | lam t ih => intro h u hu simp only [stepNO, Option.map_eq_none_iff] at h cases hu with | lam h' => exact ih h _ h' | app s t ihs iht => intro h u hu cases s with | var n => simp only [stepNO, Option.map_eq_none_iff] at h cases hu with | appL _ h' => cases h' | appR _ h' => exact iht h _ h' | lam s₀ => simp [stepNO] at h | app s₁ s₂ => simp only [stepNO] at h split at h · cases h · rename_i hs simp only [Option.map_eq_none_iff] at h cases hu with | appL _ h' => exact ihs hs _ h' | appR _ h' => exact iht h _ h'
normalize_stepstheoremProved here from basic factspropext, Quot.sound
normalize_stepsLean 4Proved here from basic factsFormally verified
/-- Whatever the evaluator returns is a β-reduct of the input. -/theorem normalize_steps (fuel : Nat) : ∀ t, ReflTransGen Step t (normalize fuel t) := by induction fuel with | zero => intro t; exact ReflTransGen.refl | succ fuel ih => intro t simp only [normalize] split · rename_i u hu exact ReflTransGen.head (stepNO_sound t u hu) (ih u) · exact ReflTransGen.refl
church_normaltheoremProved here from basic factspropext
church_normalLean 4Proved here from basic factsFormally verified
/-- Church numerals are in normal form. -/theorem church_normal (n : Nat) : Normal (church n) := by apply stepNO_none have h : ∀ k, stepNO (iterate k) = none := by intro k induction k with | zero => rfl | succ k ih => simp [iterate, stepNO, ih] simp [church, stepNO, h]
two_plus_threetheoremProved here from basic factspropext, Quot.sound
two_plus_threeLean 4Proved here from basic factsFormally verified
/-- **`plus 2̄ 3̄ ↠ 5̄`**. The kernel runs the evaluator (6 normal-order steps) and checks thatthe result is the Church numeral `5̄`; soundness turns the run into a β-reduction. -/theorem two_plus_three : ReflTransGen Step (app (app plus (church 2)) (church 3)) (church 5) := by have h : normalize 20 (app (app plus (church 2)) (church 3)) = church 5 := by decide rw [← h] exact normalize_steps 20 _
/-- A relation has the **diamond property** if any two one-step reducts of a term can bejoined by one more step on each side. -/def Diamond : Prop := ∀ a b c, r a b → r a c → ∃ d, r b d ∧ r c d
stripLean 4Proved here from basic factsFormally verified
/-- **The strip lemma**: if `r` has the diamond property, a single `r`-step and a many-step`r`-reduction from the same term can be joined (one step on the far side, many on the other).Induction along the many-step reduction, tiling one diamond at a time. -/theorem strip (hd : Diamond r) {a b c : α} (hab : r a b) (hac : ReflTransGen r a c) : ∃ d, ReflTransGen r b d ∧ r c d := by induction hac with | refl => exact ⟨b, ReflTransGen.refl, hab⟩ | tail _ hcc' ih => obtain ⟨d, hbd, hcd⟩ := ih obtain ⟨e, hde, hc'e⟩ := hd _ _ _ hcd hcc' exact ⟨e, hbd.tail hde, hc'e⟩
diamond_confluenttheoremProved here from basic factsNo axioms
diamond_confluentLean 4Proved here from basic factsFormally verified
/-- **Diamond implies confluence**: if `r` has the diamond property, then any two many-stepreducts of a term have a common many-step reduct. Induction along one reduction, using thestrip lemma for each of its steps. -/theorem diamond_confluent (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d := by induction hab with | refl => exact ⟨c, hac, ReflTransGen.refl⟩ | tail _ hbb' ih => obtain ⟨d, hbd, hcd⟩ := ih obtain ⟨e, hb'e, hde⟩ := strip hd hbb' hbd exact ⟨e, hb'e, hcd.tail hde⟩
church_rosser_librarytheoremApplies a library theoremNo axioms
church_rosser_libraryLean 4Applies a library theoremFormally verified
/-- The same abstract fact from Mathlib, in a slightly stronger form (Mathlib's`Relation.church_rosser` only needs the joining step on one side to be optional). -/theorem church_rosser_library (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c := Relation.church_rosser (fun a b c hab hac => let ⟨d, hbd, hcd⟩ := hd a b c hab hac ⟨d, ReflGen.single hbd, ReflTransGen.single hcd⟩) hab hac
/-- **Parallel reduction** `t ⇒ t'` (Tait, Martin-Löf): contract any set of redexes alreadypresent in `t`, all at once. Unlike `→`, it has the diamond property. -/inductive Par : Term → Term → Prop where | var (n : Nat) : Par (var n) (var n) | app {s s' t t' : Term} : Par s s' → Par t t' → Par (app s t) (app s' t') | lam {t t' : Term} : Par t t' → Par (lam t) (lam t') | beta {t t' s s' : Term} : Par t t' → Par s s' → Par (app (lam t) s) (inst t' s')
par_refltheoremProved here from basic factsNo axioms
par_reflLean 4Proved here from basic factsFormally verified
/-- Parallel reduction is reflexive (contract no redexes). -/theorem par_refl (t : Term) : Par t t := by induction t with | var n => exact Par.var n | app s t ihs iht => exact Par.app ihs iht | lam t ih => exact Par.lam ih
par_of_steptheoremProved here from basic factsNo axioms
par_of_stepLean 4Proved here from basic factsFormally verified
/-- A single β-step is a parallel reduction. -/theorem par_of_step {t u : Term} (h : Step t u) : Par t u := by induction h with | beta t s => exact Par.beta (par_refl t) (par_refl s) | appL t _ ih => exact Par.app ih (par_refl t) | appR s _ ih => exact Par.app (par_refl s) ih | lam _ ih => exact Par.lam ih
steps_of_partheoremProved here from basic factsNo axioms
steps_of_parLean 4Proved here from basic factsFormally verified
/-- A parallel reduction can be done one β-step at a time. -/theorem steps_of_par {t u : Term} (h : Par t u) : ReflTransGen Step t u := by induction h with | var n => exact ReflTransGen.refl | app _ _ ihs iht => exact steps_app ihs iht | lam _ ih => exact steps_lam ih | beta _ _ iht ihs => exact (steps_app (steps_lam iht) ihs).tail (Step.beta _ _)
par_insttheoremProved here from basic factspropext, Quot.sound
par_instLean 4Proved here from basic factsFormally verified
/-- If `t ⇒ t'` and `s ⇒ s'`, then `t[s/x] ⇒ t'[s'/x]`. -/theorem par_inst {t t' s s' : Term} (ht : Par t t') (hs : Par s s') : Par (inst t s) (inst t' s') := by apply par_subst ht intro n cases n with | zero => exact hs | succ k => exact Par.var k
triangletheoremProved here from basic factspropext, Quot.sound
triangleLean 4Proved here from basic factsFormally verified
/-- **The triangle property**: if `t ⇒ u`, then `u ⇒ t*`. Every parallel reduct of `t` cancatch up with the complete development of `t` in one more parallel step. -/theorem triangle {t u : Term} (h : Par t u) : Par u (cd t) := by induction h with | var n => exact Par.var n | lam _ ih => exact Par.lam ih | beta _ _ iht ihs => exact par_inst iht ihs | @app s s' t t' hs _ ihs iht => cases s with | var n => exact Par.app ihs iht | app s₁ s₂ => exact Par.app ihs iht | lam s₀ => cases hs with | lam hs₀ => cases ihs with | lam ih₀ => exact Par.beta ih₀ iht
par_diamondtheoremProved here from basic factspropext, Quot.sound
par_diamondLean 4Proved here from basic factsFormally verified
/-- Parallel reduction has the **diamond property**: two parallel reducts of `t` both reduce inone parallel step to the complete development `t*`. -/theorem par_diamond : Diamond Par := fun t _ _ hu hv => ⟨cd t, triangle hu, triangle hv⟩
steps_iff_par_stepstheoremProved here from basic factsNo axioms
steps_iff_par_stepsLean 4Proved here from basic factsFormally verified
/-- Many β-steps and many parallel steps are the same relation, since`→ ⊆ ⇒ ⊆ ↠`. -/theorem steps_iff_par_steps {t u : Term} : ReflTransGen Step t u ↔ ReflTransGen Par t u := by constructor · intro h exact h.lift id fun _ _ hs => par_of_step hs · intro h induction h with | refl => exact ReflTransGen.refl | tail _ hp ih => exact ih.trans (steps_of_par hp)
church_rossertheoremProved here from basic factspropext, Quot.sound
church_rosserLean 4Proved here from basic factsFormally verified
/-- **The Church–Rosser theorem** (Church and Rosser, 1936): β-reduction is confluent. If`t ↠ u` and `t ↠ v`, there is a `w` with `u ↠ w` and `v ↠ w`. Proof: confluence of parallelreduction (diamond ⇒ confluence), transported along `↠ = ⇒*`. -/theorem church_rosser {t u v : Term} (hu : ReflTransGen Step t u) (hv : ReflTransGen Step t v) : ∃ w, ReflTransGen Step u w ∧ ReflTransGen Step v w := by obtain ⟨w, huw, hvw⟩ := diamond_confluent par_diamond (steps_iff_par_steps.1 hu) (steps_iff_par_steps.1 hv) exact ⟨w, steps_iff_par_steps.2 huw, steps_iff_par_steps.2 hvw⟩
normal_form_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
normal_form_uniqueLean 4Proved here from basic factsFormally verified
/-- **Normal forms are unique**: a term has at most one normal form. By Church–Rosser two normalforms `u, v` of `t` reduce to a common `w`; a normal term reduces only to itself, so`u = w = v`. -/theorem normal_form_unique {t u v : Term} (hu : ReflTransGen Step t u) (hv : ReflTransGen Step t v) (nu : Normal u) (nv : Normal v) : u = v := by have stuck : ∀ {x y : Term}, Normal x → ReflTransGen Step x y → x = y := by intro x y nx hxy cases hxy.cases_head with | inl h => exact h | inr h => obtain ⟨z, hxz, _⟩ := h exact absurd hxz (nx z) obtain ⟨w, huw, hvw⟩ := church_rosser hu hv rw [stuck nu huw, stuck nv hvw]
plus_unique_valuetheoremProved here from basic factspropext, Classical.choice, Quot.sound
plus_unique_valueLean 4Proved here from basic factsFormally verified
/-- Consequently `5̄` is *the* normal form of `plus 2̄ 3̄`: no reduction strategy can produce adifferent normal form. -/theorem plus_unique_value {v : Term} (hv : ReflTransGen Step (app (app plus (church 2)) (church 3)) v) (nv : Normal v) : v = church 5 := (normal_form_unique two_plus_three hv (church_normal 5) nv).symm
/-- Turing's combinator reaches `F (Θ F)` in two β-steps. Hint: the first step is a β-step inthe function position (`Step.appL`), the second a β-step at the top; combine them with`ReflTransGen.head` and `ReflTransGen.single`. -/theorem theta_fixed_point (F : Term) : ReflTransGen Step (Term.app theta F) (Term.app F (Term.app theta F)) := by sorry
Show the compiled solution
theta_fixed_pointLean 4Proved here from basic factsFormally verified
/-- **`Θ F ↠ F (Θ F)` for every term `F`** — in two β-steps. This is how the untyped calculusdefines recursive functions: a solution of `f = F f`. -/theorem theta_fixed_point (F : Term) : ReflTransGen Step (app theta F) (app F (app theta F)) := by refine ReflTransGen.head (Step.appL F (Step.beta _ _)) ?_ exact ReflTransGen.single (Step.beta _ _)
/-- Diamond implies confluence. Hint: induct on `hab`, and use the strip lemma`Lumenary.LambdaCalculus.strip` for each step. -/theorem diamond_confluent {α : Type*} {r : α → α → Prop} (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d := by sorry
Show the compiled solution
diamond_confluentLean 4Proved here from basic factsFormally verified
/-- **Diamond implies confluence**: if `r` has the diamond property, then any two many-stepreducts of a term have a common many-step reduct. Induction along one reduction, using thestrip lemma for each of its steps. -/theorem diamond_confluent (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d := by induction hab with | refl => exact ⟨c, hac, ReflTransGen.refl⟩ | tail _ hbb' ih => obtain ⟨d, hbd, hcd⟩ := ih obtain ⟨e, hb'e, hde⟩ := strip hd hbb' hbd exact ⟨e, hb'e, hcd.tail hde⟩