From 201c68cf0a70ae2f6b04a15929547fde7226cc3b Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Tue, 17 Feb 2026 16:41:50 +0100
Subject: [PATCH 1/5] chore(CombinatoryLogic): scope grind attributes and add
 helper lemmas
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add B_tail_mred and C_head_mred convenience lemmas.
Scope grind attributes; use forward mode (→) where appropriate.
Remove grind from isChurch_trans to avoid cascading instantiations.
---
 Cslib/Languages/CombinatoryLogic/Basic.lean   | 12 +++++++
 .../Languages/CombinatoryLogic/Recursion.lean | 32 +++++++++++++++++--
 2 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean
index daad3035..4d1d8310 100644
--- a/Cslib/Languages/CombinatoryLogic/Basic.lean
+++ b/Cslib/Languages/CombinatoryLogic/Basic.lean
@@ -172,6 +172,10 @@ def B : SKI := BPoly.toSKI
 theorem B_def (f g x : SKI) : (B ⬝ f ⬝ g ⬝ x) ↠ f ⬝ (g ⬝ x) :=
   BPoly.toSKI_correct [f, g, x] (by simp)
 
+/-- B followed by tail reduction -/
+lemma B_tail_mred (f g x y : SKI) (h : (g ⬝ x) ↠ y) : (B ⬝ f ⬝ g ⬝ x) ↠ f ⬝ y :=
+  Trans.trans (B_def f g x) (MRed.tail f h)
+
 /-- C := λ f x y. f y x -/
 def CPoly : SKI.Polynomial 3 := &0 ⬝' &2 ⬝' &1
 /-- A SKI term representing C -/
@@ -179,6 +183,10 @@ def C : SKI := CPoly.toSKI
 theorem C_def (f x y : SKI) : (C ⬝ f ⬝ x ⬝ y) ↠ f ⬝ y ⬝ x :=
   CPoly.toSKI_correct [f, x, y] (by simp)
 
+/-- C followed by head reduction -/
+lemma C_head_mred (f x y z : SKI) (h : (f ⬝ y) ↠ z) : (C ⬝ f ⬝ x ⬝ y) ↠ z ⬝ x :=
+  Trans.trans (C_def f x y) (MRed.head x h)
+
 /-- Rotate right: RotR := λ x y z. z x y -/
 def RotRPoly : SKI.Polynomial 3 := &2 ⬝' &0 ⬝' &1
 /-- A SKI term representing RotR -/
@@ -259,10 +267,12 @@ theorem isBool_trans (u : Bool) (a a' : SKI) (h : a ↠ a') (ha' : IsBool u a')
 
 /-- Standard true: TT := λ x y. x -/
 def TT : SKI := K
+@[scoped grind .]
 theorem TT_correct : IsBool true TT := fun x y ↦ MRed.K x y
 
 /-- Standard false: FF := λ x y. y -/
 def FF : SKI := K ⬝ I
+@[scoped grind .]
 theorem FF_correct : IsBool false FF :=
   fun x y ↦ calc
     (FF ⬝ x ⬝ y) ↠ I ⬝ y := by apply Relation.ReflTransGen.single; apply red_head; exact red_K I x
@@ -336,10 +346,12 @@ def Fst : SKI := R ⬝ TT
 /-- Second projection -/
 def Snd : SKI := R ⬝ FF
 
+@[scoped grind .]
 theorem fst_correct (a b : SKI) : (Fst ⬝ (MkPair ⬝ a ⬝ b)) ↠ a := by calc
   _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ TT := R_def _ _
   _ ↠ a := cond_correct TT a b true TT_correct
 
+@[scoped grind .]
 theorem snd_correct (a b : SKI) : (Snd ⬝ (MkPair ⬝ a ⬝ b)) ↠ b := by calc
   _ ↠ SKI.Cond ⬝ a ⬝ b ⬝ FF := R_def _ _
   _ ↠ b := cond_correct FF a b false FF_correct
diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean
index f8b63d61..898d139e 100644
--- a/Cslib/Languages/CombinatoryLogic/Recursion.lean
+++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean
@@ -63,6 +63,9 @@ match n with
 | 0 => x
 | n+1 => f ⬝ (Church n f x)
 
+@[simp] lemma Church_zero (f x : SKI) : Church 0 f x = x := rfl
+@[simp] lemma Church_succ (n : Nat) (f x : SKI) : Church (n+1) f x = f ⬝ Church n f x := rfl
+
 /-- `church` commutes with reduction. -/
 lemma church_red (n : Nat) (f f' x x' : SKI) (hf : f ↠ f') (hx : x ↠ x') :
     Church n f x ↠ Church n f' x' := by
@@ -75,7 +78,9 @@ def IsChurch (n : Nat) (a : SKI) : Prop :=
     ∀ f x :SKI, (a ⬝ f ⬝ x) ↠ (Church n f x)
 
 /-- To show `IsChurch n a` it suffices to show the same for a reduct of `a`. -/
-theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') : IsChurch n a' → IsChurch n a := by
+-- not a grind rule: triggers too many instantiations (#grind_lint)
+theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') :
+    IsChurch n a' → IsChurch n a := by
   simp_rw [IsChurch]
   intro ha' f x
   calc
@@ -87,6 +92,7 @@ theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') : IsChurch n a' →
 
 /-- Church zero := λ f x. x -/
 protected def Zero : SKI := K ⬝ I
+@[scoped grind .]
 theorem zero_correct : IsChurch 0 SKI.Zero := by
   unfold IsChurch SKI.Zero Church
   intro f x
@@ -96,6 +102,7 @@ theorem zero_correct : IsChurch 0 SKI.Zero := by
 
 /-- Church one := λ f x. f x -/
 protected def One : SKI := I
+@[scoped grind .]
 theorem one_correct : IsChurch 1 SKI.One := by
   intro f x
   apply head
@@ -103,13 +110,32 @@ theorem one_correct : IsChurch 1 SKI.One := by
 
 /-- Church succ := λ a f x. f (a f x) ~ λ a f. B f (a f) ~ λ a. S B a ~ S B -/
 protected def Succ : SKI := S ⬝ B
-theorem succ_correct (n : Nat) (a : SKI) (h : IsChurch n a) : IsChurch (n+1) (SKI.Succ ⬝ a) := by
+@[scoped grind →]
+theorem succ_correct (n : Nat) (a : SKI) (h : IsChurch n a) :
+    IsChurch (n+1) (SKI.Succ ⬝ a) := by
   intro f x
   calc
   _ ⭢ B ⬝ f ⬝ (a ⬝ f) ⬝ x := by apply red_head; apply red_S
   _ ↠ f ⬝ (a ⬝ f ⬝ x) := by apply B_def
   _ ↠ f ⬝ (Church n  f x) := by apply MRed.tail; exact h f x
 
+/-- Build the canonical SKI Church numeral for `n`. -/
+def toChurch : ℕ → SKI
+  | 0 => SKI.Zero
+  | n + 1 => SKI.Succ ⬝ (toChurch n)
+
+/-- `toChurch 0 = Zero`. -/
+@[simp] lemma toChurch_zero : toChurch 0 = SKI.Zero := rfl
+/-- `toChurch (n + 1) = Succ ⬝ toChurch n`. -/
+@[simp] lemma toChurch_succ (n : ℕ) : toChurch (n + 1) = SKI.Succ ⬝ (toChurch n) := rfl
+
+/-- `toChurch n` correctly represents `n`. -/
+@[scoped grind .]
+theorem toChurch_correct (n : ℕ) : IsChurch n (toChurch n) := by
+  induction n with
+  | zero => exact zero_correct
+  | succ n ih => exact succ_correct n (toChurch n) ih
+
 /--
 To define the predecessor, iterate the function `PredAux` ⟨i, j⟩ ↦ ⟨j, j+1⟩ on ⟨0,0⟩, then take
 the  first component.
@@ -155,7 +181,7 @@ theorem predAux_correct' (n : Nat) :
       · exact fst_correct _ _
       · exact snd_correct _ _
     | succ n ih =>
-      simp_rw [Church]
+      simp_rw [Church_succ]
       apply predAux_correct (ns := ⟨n.pred, n⟩) (h := ih)
 
 /-- Predecessor := λ n. Fst ⬝ (n ⬝ PredAux ⬝ (MkPair ⬝ Zero ⬝ Zero)) -/

From ba119cd4e6d6323298368b3d3700bc313e8b5d01 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Tue, 17 Feb 2026 16:41:57 +0100
Subject: [PATCH 2/5] feat(CombinatoryLogic): add Church-encoded list
 infrastructure for SKI terms

Adds Church-encoded list operations (nil, cons, head, tail) along with
conversions to/from Church numerals and helper combinators (PrependZero,
SuccHead). Head is defined via a general HeadD with arbitrary default.

Thanks to @thomaskwaring for suggesting the HeadD generalization.
---
 Cslib.lean                                    |   1 +
 Cslib/Languages/CombinatoryLogic/List.lean    | 282 ++++++++++++++++++
 .../Languages/CombinatoryLogic/Recursion.lean |   1 -
 3 files changed, 283 insertions(+), 1 deletion(-)
 create mode 100644 Cslib/Languages/CombinatoryLogic/List.lean

diff --git a/Cslib.lean b/Cslib.lean
index 432290df..df238d73 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -71,6 +71,7 @@ public import Cslib.Languages.CombinatoryLogic.Basic
 public import Cslib.Languages.CombinatoryLogic.Confluence
 public import Cslib.Languages.CombinatoryLogic.Defs
 public import Cslib.Languages.CombinatoryLogic.Evaluation
+public import Cslib.Languages.CombinatoryLogic.List
 public import Cslib.Languages.CombinatoryLogic.Recursion
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean
new file mode 100644
index 00000000..8b58be7d
--- /dev/null
+++ b/Cslib/Languages/CombinatoryLogic/List.lean
@@ -0,0 +1,282 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Languages.CombinatoryLogic.Recursion
+
+@[expose] public section
+
+/-!
+# Church-Encoded Lists in SKI Combinatory Logic
+
+Church-encoded lists for proving SKI ≃ TM equivalence. A list is encoded as
+`λ c n. c a₀ (c a₁ (... (c aₖ n)...))` where each `aᵢ` is a Church numeral.
+-/
+
+namespace Cslib
+
+namespace SKI
+
+open Red MRed
+
+/-! ### Church List Representation -/
+
+/-- A term correctly Church-encodes a list of natural numbers. -/
+def IsChurchList : List ℕ → SKI → Prop
+  | [], cns => ∀ c n : SKI, (cns ⬝ c ⬝ n) ↠ n
+  | x :: xs, cns => ∀ c n : SKI,
+      ∃ cx cxs : SKI, IsChurch x cx ∧ IsChurchList xs cxs ∧
+        (cns ⬝ c ⬝ n) ↠ c ⬝ cx ⬝ (cxs ⬝ c ⬝ n)
+
+/-- `IsChurchList` is preserved under multi-step reduction of the term. -/
+theorem isChurchList_trans {ns : List ℕ} {cns cns' : SKI} (h : cns ↠ cns')
+    (hcns' : IsChurchList ns cns') : IsChurchList ns cns := by
+  match ns with
+  | [] =>
+    intro c n
+    exact Trans.trans (parallel_mRed (MRed.head c h) .refl) (hcns' c n)
+  | x :: xs =>
+    intro c n
+    obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns' c n
+    exact ⟨cx, cxs, hcx, hcxs,
+      Trans.trans (parallel_mRed (MRed.head c h) .refl) hred⟩
+
+/-- Both components of a pair are Church lists. -/
+def IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop :=
+  IsChurchList prev (Fst ⬝ p) ∧ IsChurchList curr (Snd ⬝ p)
+
+/-- IsChurchListPair is preserved under reduction. -/
+@[scoped grind →]
+theorem isChurchListPair_trans {prev curr : List ℕ} {p p' : SKI} (hp : p ↠ p')
+    (hp' : IsChurchListPair prev curr p') : IsChurchListPair prev curr p := by
+  constructor
+  · apply isChurchList_trans (MRed.tail Fst hp)
+    exact hp'.1
+  · apply isChurchList_trans (MRed.tail Snd hp)
+    exact hp'.2
+
+namespace List
+
+/-! ### Nil: The empty list -/
+
+/-- nil = λ c n. n -/
+def NilPoly : SKI.Polynomial 2 := &1
+
+/-- The SKI term for the empty list. -/
+def Nil : SKI := NilPoly.toSKI
+
+/-- Reduction: `Nil ⬝ c ⬝ n ↠ n`. -/
+theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n :=
+  NilPoly.toSKI_correct [c, n] (by simp)
+
+/-- The empty list term correctly represents `[]`. -/
+theorem nil_correct : IsChurchList [] Nil := fun c n => nil_def c n
+
+/-! ### Cons: Consing an element onto a list -/
+
+/-- cons = λ x xs c n. c x (xs c n) -/
+def ConsPoly : SKI.Polynomial 4 := &2 ⬝' &0 ⬝' (&1 ⬝' &2 ⬝' &3)
+
+/-- The SKI term for list cons. -/
+def Cons : SKI := ConsPoly.toSKI
+
+/-- Reduction: `Cons ⬝ x ⬝ xs ⬝ c ⬝ n ↠ c ⬝ x ⬝ (xs ⬝ c ⬝ n)`. -/
+theorem cons_def (x xs c n : SKI) :
+    (Cons ⬝ x ⬝ xs ⬝ c ⬝ n) ↠ c ⬝ x ⬝ (xs ⬝ c ⬝ n) :=
+  ConsPoly.toSKI_correct [x, xs, c, n] (by simp)
+
+/-- Cons preserves Church list representation. -/
+theorem cons_correct {x : ℕ} {xs : List ℕ} {cx cxs : SKI}
+    (hcx : IsChurch x cx) (hcxs : IsChurchList xs cxs) :
+    IsChurchList (x :: xs) (Cons ⬝ cx ⬝ cxs) := by
+  intro c n
+  use cx, cxs, hcx, hcxs
+  exact cons_def cx cxs c n
+
+/-- Singleton list correctness. -/
+theorem singleton_correct {x : ℕ} {cx : SKI} (hcx : IsChurch x cx) :
+    IsChurchList [x] (Cons ⬝ cx ⬝ Nil) :=
+  cons_correct hcx nil_correct
+
+/-- The canonical SKI term for a Church-encoded list. -/
+def toChurch : List ℕ → SKI
+  | [] => Nil
+  | x :: xs => Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs)
+
+/-- `toChurch [] = Nil`. -/
+@[simp]
+lemma toChurch_nil : toChurch [] = Nil := rfl
+/-- `toChurch (x :: xs) = Cons ⬝ SKI.toChurch x ⬝ toChurch xs`. -/
+@[simp]
+lemma toChurch_cons (x : ℕ) (xs : List ℕ) :
+    toChurch (x :: xs) = Cons ⬝ (SKI.toChurch x) ⬝ (toChurch xs) := rfl
+
+/-- `toChurch ns` correctly represents `ns`. -/
+theorem toChurch_correct (ns : List ℕ) : IsChurchList ns (toChurch ns) := by
+  induction ns with
+  | nil => exact nil_correct
+  | cons x xs ih => exact cons_correct (SKI.toChurch_correct x) ih
+
+/-! ### Head: Extract the head of a list -/
+
+/-- headD d xs = xs K d (returns d for empty list) -/
+def HeadDPoly : SKI.Polynomial 2 := &1 ⬝' K ⬝' &0
+
+/-- The SKI term for list head with default. -/
+def HeadD : SKI := HeadDPoly.toSKI
+
+/-- Reduction: `HeadD ⬝ d ⬝ xs ↠ xs ⬝ K ⬝ d`. -/
+theorem headD_def (d xs : SKI) : (HeadD ⬝ d ⬝ xs) ↠ xs ⬝ K ⬝ d :=
+  HeadDPoly.toSKI_correct [d, xs] (by simp)
+
+/-- General head-with-default correctness. -/
+theorem headD_correct {d : ℕ} {cd : SKI} (hcd : IsChurch d cd)
+    {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) :
+    IsChurch (ns.headD d) (HeadD ⬝ cd ⬝ cns) := by
+  match ns with
+  | [] =>
+    simp only [List.headD_nil]
+    apply isChurch_trans d (headD_def cd cns)
+    apply isChurch_trans d (hcns K cd)
+    exact hcd
+  | x :: xs =>
+    simp only [List.headD_cons]
+    apply isChurch_trans x (headD_def cd cns)
+    obtain ⟨cx, cxs, hcx, _, hred⟩ := hcns K cd
+    exact isChurch_trans x hred (isChurch_trans x (MRed.K cx _) hcx)
+
+/-- The SKI term for list head (default 0). -/
+def Head : SKI := HeadD ⬝ SKI.Zero
+
+/-- Reduction: `Head ⬝ xs ↠ xs ⬝ K ⬝ Zero`. -/
+theorem head_def (xs : SKI) : (Head ⬝ xs) ↠ xs ⬝ K ⬝ SKI.Zero :=
+  headD_def SKI.Zero xs
+
+/-- Head correctness (default 0). -/
+theorem head_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
+    IsChurch (ns.headD 0) (Head ⬝ cns) :=
+  headD_correct zero_correct hcns
+
+/-! ### Tail: Extract the tail of a list -/
+
+/-- Step function for tail: (prev, curr) → (curr, cons h curr) -/
+def TailStepPoly : SKI.Polynomial 2 :=
+  MkPair ⬝' (Snd ⬝' &1) ⬝' (Cons ⬝' &0 ⬝' (Snd ⬝' &1))
+
+/-- The step function for computing list tail. -/
+def TailStep : SKI := TailStepPoly.toSKI
+
+/-- Reduction of the tail step function. -/
+theorem tailStep_def (h p : SKI) :
+    (TailStep ⬝ h ⬝ p) ↠ MkPair ⬝ (Snd ⬝ p) ⬝ (Cons ⬝ h ⬝ (Snd ⬝ p)) :=
+  TailStepPoly.toSKI_correct [h, p] (by simp)
+
+/-- tail xs = Fst (xs TailStep (MkPair Nil Nil)) -/
+def TailPoly : SKI.Polynomial 1 :=
+  Fst ⬝' (&0 ⬝' TailStep ⬝' (MkPair ⬝ Nil ⬝ Nil))
+
+/-- The tail of a Church-encoded list. -/
+def Tail : SKI := TailPoly.toSKI
+
+/-- Reduction: `Tail ⬝ xs ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil))`. -/
+theorem tail_def (xs : SKI) :
+    (Tail ⬝ xs) ↠ Fst ⬝ (xs ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) :=
+  TailPoly.toSKI_correct [xs] (by simp)
+
+/-- The initial pair (nil, nil) satisfies the invariant. -/
+@[simp]
+theorem tail_init : IsChurchListPair [] [] (MkPair ⬝ Nil ⬝ Nil) := by
+  constructor
+  · apply isChurchList_trans (fst_correct _ _); exact nil_correct
+  · apply isChurchList_trans (snd_correct _ _); exact nil_correct
+
+/-- The step function preserves the tail-computing invariant. -/
+theorem tailStep_correct {x : ℕ} {xs : List ℕ} {cx p : SKI}
+    (hcx : IsChurch x cx) (hp : IsChurchListPair xs.tail xs p) :
+    IsChurchListPair xs (x :: xs) (TailStep ⬝ cx ⬝ p) := by
+  apply isChurchListPair_trans (tailStep_def cx p)
+  exact ⟨isChurchList_trans (fst_correct _ _) hp.2,
+         isChurchList_trans (snd_correct _ _) (cons_correct hcx hp.2)⟩
+
+theorem tailFold_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
+    ∃ p, (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil)) ↠ p ∧
+         IsChurchListPair ns.tail ns p := by
+  induction ns generalizing cns with
+  | nil =>
+    -- For empty list, the fold returns the initial pair
+    use MkPair ⬝ Nil ⬝ Nil
+    constructor
+    · exact hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
+    · simp only [List.tail_nil]
+      exact tail_init
+  | cons x xs ih =>
+    -- For x :: xs, first fold xs, then apply step
+    -- cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init)
+    simp only [List.tail_cons]
+    -- Get the Church representations for x and xs
+    obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
+    -- By IH, folding xs gives a pair representing (xs.tail, xs)
+    obtain ⟨p_xs, hp_xs_red, hp_xs_pair⟩ := ih cxs hcxs
+    -- After step, we get a pair representing (xs, x :: xs)
+    have hstep := tailStep_correct hcx hp_xs_pair
+    -- The full fold: cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init)
+    --                                         ↠ TailStep ⬝ cx ⬝ p_xs
+    use TailStep ⬝ cx ⬝ p_xs
+    constructor
+    · exact Trans.trans hred (MRed.tail _ hp_xs_red)
+    · exact hstep
+
+/-- Tail correctness. -/
+theorem tail_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
+    IsChurchList ns.tail (Tail ⬝ cns) := by
+  -- Tail ⬝ cns ↠ Fst ⬝ (cns ⬝ TailStep ⬝ (MkPair ⬝ Nil ⬝ Nil))
+  apply isChurchList_trans (tail_def cns)
+  -- Get the fold result
+  obtain ⟨p, hp_red, hp_pair⟩ := tailFold_correct ns cns hcns
+  -- Fst ⬝ (cns ⬝ TailStep ⬝ init) ↠ Fst ⬝ p
+  apply isChurchList_trans (MRed.tail Fst hp_red)
+  -- Fst ⬝ p represents ns.tail (from hp_pair)
+  exact hp_pair.1
+
+/-! ### Prepending zero to a list (for Code.zero') -/
+
+/-- PrependZero xs = cons 0 xs = Cons ⬝ Zero ⬝ xs -/
+def PrependZeroPoly : SKI.Polynomial 1 := Cons ⬝' SKI.Zero ⬝' &0
+
+/-- Prepend zero to a Church-encoded list. -/
+def PrependZero : SKI := PrependZeroPoly.toSKI
+
+/-- Reduction: `PrependZero ⬝ xs ↠ Cons ⬝ Zero ⬝ xs`. -/
+theorem prependZero_def (xs : SKI) : (PrependZero ⬝ xs) ↠ Cons ⬝ SKI.Zero ⬝ xs :=
+  PrependZeroPoly.toSKI_correct [xs] (by simp)
+
+/-- Prepending zero preserves Church list representation. -/
+theorem prependZero_correct {ns : List ℕ} {cns : SKI} (hcns : IsChurchList ns cns) :
+    IsChurchList (0 :: ns) (PrependZero ⬝ cns) := by
+  apply isChurchList_trans (prependZero_def cns)
+  exact cons_correct zero_correct hcns
+
+/-! ### Successor on list head (for Code.succ) -/
+
+/-- SuccHead xs = cons (succ (head xs)) nil -/
+def SuccHead : SKI := B ⬝ (C ⬝ Cons ⬝ Nil) ⬝ (B ⬝ SKI.Succ ⬝ Head)
+
+/-- `SuccHead` correctly computes a singleton containing `succ(head ns)`. -/
+theorem succHead_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns) :
+    IsChurchList [ns.headD 0 + 1] (SuccHead ⬝ cns) := by
+  have hhead := head_correct ns cns hcns
+  have hsucc := succ_correct (ns.headD 0) (Head ⬝ cns) hhead
+  apply isChurchList_trans
+    (Trans.trans (B_tail_mred _ _ _ _ (B_def SKI.Succ Head cns))
+                 (C_def Cons Nil _))
+  exact cons_correct hsucc nil_correct
+
+end List
+
+end SKI
+
+end Cslib
diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean
index 898d139e..4dda851c 100644
--- a/Cslib/Languages/CombinatoryLogic/Recursion.lean
+++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean
@@ -78,7 +78,6 @@ def IsChurch (n : Nat) (a : SKI) : Prop :=
     ∀ f x :SKI, (a ⬝ f ⬝ x) ↠ (Church n f x)
 
 /-- To show `IsChurch n a` it suffices to show the same for a reduct of `a`. -/
--- not a grind rule: triggers too many instantiations (#grind_lint)
 theorem isChurch_trans (n : Nat) {a a' : SKI} (h : a ↠ a') :
     IsChurch n a' → IsChurch n a := by
   simp_rw [IsChurch]

From 1449b9193c99988b860cc3b815fd07afcdde7e78 Mon Sep 17 00:00:00 2001
From: Jesse Alama <jessealama@users.noreply.github.com>
Date: Tue, 17 Feb 2026 19:19:11 +0100
Subject: [PATCH 3/5] Update Cslib/Languages/CombinatoryLogic/List.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Languages/CombinatoryLogic/List.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean
index 8b58be7d..065bbcf4 100644
--- a/Cslib/Languages/CombinatoryLogic/List.lean
+++ b/Cslib/Languages/CombinatoryLogic/List.lean
@@ -270,9 +270,7 @@ theorem succHead_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns
     IsChurchList [ns.headD 0 + 1] (SuccHead ⬝ cns) := by
   have hhead := head_correct ns cns hcns
   have hsucc := succ_correct (ns.headD 0) (Head ⬝ cns) hhead
-  apply isChurchList_trans
-    (Trans.trans (B_tail_mred _ _ _ _ (B_def SKI.Succ Head cns))
-                 (C_def Cons Nil _))
+  apply isChurchList_trans (.trans (B_tail_mred _ _ _ _ (B_def .Succ Head cns)) (C_def Cons Nil _))
   exact cons_correct hsucc nil_correct
 
 end List

From 47ed8eb37ed6b21523f545b1e1c1c9da8ca043a4 Mon Sep 17 00:00:00 2001
From: Jesse Alama <jessealama@users.noreply.github.com>
Date: Tue, 17 Feb 2026 19:19:24 +0100
Subject: [PATCH 4/5] Update Cslib/Languages/CombinatoryLogic/List.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Languages/CombinatoryLogic/List.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean
index 065bbcf4..d3f70a6e 100644
--- a/Cslib/Languages/CombinatoryLogic/List.lean
+++ b/Cslib/Languages/CombinatoryLogic/List.lean
@@ -74,7 +74,7 @@ theorem nil_def (c n : SKI) : (Nil ⬝ c ⬝ n) ↠ n :=
   NilPoly.toSKI_correct [c, n] (by simp)
 
 /-- The empty list term correctly represents `[]`. -/
-theorem nil_correct : IsChurchList [] Nil := fun c n => nil_def c n
+theorem nil_correct : IsChurchList [] Nil := nil_def
 
 /-! ### Cons: Consing an element onto a list -/
 

From e04d76453b9f4c6deccee6971db36de5f33e163a Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Tue, 17 Feb 2026 19:40:12 +0100
Subject: [PATCH 5/5] Style fixes in List.lean

Thanks to chenson2018 for the feedback.
---
 Cslib/Languages/CombinatoryLogic/List.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Cslib/Languages/CombinatoryLogic/List.lean b/Cslib/Languages/CombinatoryLogic/List.lean
index d3f70a6e..c71721da 100644
--- a/Cslib/Languages/CombinatoryLogic/List.lean
+++ b/Cslib/Languages/CombinatoryLogic/List.lean
@@ -42,12 +42,12 @@ theorem isChurchList_trans {ns : List ℕ} {cns cns' : SKI} (h : cns ↠ cns')
   | x :: xs =>
     intro c n
     obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns' c n
-    exact ⟨cx, cxs, hcx, hcxs,
-      Trans.trans (parallel_mRed (MRed.head c h) .refl) hred⟩
+    exact ⟨cx, cxs, hcx, hcxs, Trans.trans (parallel_mRed (MRed.head c h) .refl) hred⟩
 
 /-- Both components of a pair are Church lists. -/
-def IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop :=
-  IsChurchList prev (Fst ⬝ p) ∧ IsChurchList curr (Snd ⬝ p)
+structure IsChurchListPair (prev curr : List ℕ) (p : SKI) : Prop where
+  fst : IsChurchList prev (Fst ⬝ p)
+  snd : IsChurchList curr (Snd ⬝ p)
 
 /-- IsChurchListPair is preserved under reduction. -/
 @[scoped grind →]
@@ -110,6 +110,7 @@ def toChurch : List ℕ → SKI
 /-- `toChurch [] = Nil`. -/
 @[simp]
 lemma toChurch_nil : toChurch [] = Nil := rfl
+
 /-- `toChurch (x :: xs) = Cons ⬝ SKI.toChurch x ⬝ toChurch xs`. -/
 @[simp]
 lemma toChurch_cons (x : ℕ) (xs : List ℕ) :
@@ -211,12 +212,10 @@ theorem tailFold_correct (ns : List ℕ) (cns : SKI) (hcns : IsChurchList ns cns
     use MkPair ⬝ Nil ⬝ Nil
     constructor
     · exact hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
-    · simp only [List.tail_nil]
-      exact tail_init
+    · exact tail_init
   | cons x xs ih =>
     -- For x :: xs, first fold xs, then apply step
     -- cns ⬝ TailStep ⬝ init ↠ TailStep ⬝ cx ⬝ (cxs ⬝ TailStep ⬝ init)
-    simp only [List.tail_cons]
     -- Get the Church representations for x and xs
     obtain ⟨cx, cxs, hcx, hcxs, hred⟩ := hcns TailStep (MkPair ⬝ Nil ⬝ Nil)
     -- By IH, folding xs gives a pair representing (xs.tail, xs)