feat(CombinatoryLogic): Partrec → SKI computability

[jessealama]

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.

[thomaskwaring]

Looks pretty good to me! The title should probably say that only one direction of the equivalence is proven here (Partrec -> SKI). If I have time I can do a more thorough review but my only real concern would be whether the new version of primitive recursion could use the original one in Recursion.lean any more (though I would believe that the pair/unpair dance makes that impossible)

[jessealama]

Looks pretty good to me! The title should probably say that only one direction of the equivalence is proven here (Partrec -> SKI). If I have time I can do a more thorough review but my only real concern would be whether the new version of primitive recursion could use the original one in Recursion.lean any more (though I would believe that the pair/unpair dance makes that impossible)

In an earlier version of this proof, I tried to apply the original recursor directly but gave up because it was getting too bulky. The new PrecTrans is essentially a custom wrapper around Rec for this proof. I'm happy to try to resurrect that earlier approach, or "hide" the PrecTrans if we don't want to expose it. At a minimum, I'll add more documentation to clarify what's going on with the new recursor.

[thomaskwaring]

In an earlier version of this proof, I tried to apply the original recursor directly but gave up because it was getting too bulky. The new PrecTrans is essentially a custom wrapper around Rec for this proof. I'm happy to try to resurrect that earlier approach, or "hide" the PrecTrans if we don't want to expose it. At a minimum, I'll add more documentation to clarify what's going on with the new recursor.

Makes sense! happy for you to leave as-is and/or hide the definition as you & the maintainers prefer. I suppose the ideal outcome would be for the definition of the term to mirror what the function looks like in Nat.Partrec, but that uses the monad structure on Part/PFun — once we have more API for encodings of datatypes I might try to update it, but that will be a way-away.