feat(CombinatoryLogic): SKI ↔ Partrec equivalence

Prove that every Nat.Partrec function on ℕ is SKI-computable
(nat_partrec_ski_computable). Translates all eight Nat.Partrec.Code
constructors to SKI terms and proves correctness, exercising the
Recursion.lean infrastructure: primitive recursion (Rec), μ-recursion
(RFind/RFindAbove), Nat pairing/unpairing, and integer square root.

Author: jessealama

Cslib.lean

@@ -76,6 +76,7 @@ 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.PartrecEquivalence
 public import Cslib.Languages.CombinatoryLogic.Recursion
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic

Cslib/Languages/CombinatoryLogic/Basic.lean

@@ -288,6 +288,7 @@ theorem cond_correct (a x y : SKI) (u : Bool) (h : IsBool u a) :
 
 /-- Neg := λ a. Cond FF TT a -/
 protected def Neg : SKI := SKI.Cond ⬝ FF ⬝ TT
+@[scoped grind →]
 theorem neg_correct (a : SKI) (ua : Bool) (h : IsBool ua a) : IsBool (¬ ua) (SKI.Neg ⬝ a) := by
   apply isBool_trans (a' := if ua then FF else TT)
   · apply cond_correct (h := h)

Cslib/Languages/CombinatoryLogic/List.lean

@@ -74,6 +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 `[]`. -/
+@[scoped grind .]
 theorem nil_correct : IsChurchList [] Nil := nil_def
 
 /-! ### Cons: Consing an element onto a list -/