feat(CombinatoryLogic): Partrec → SKI computability - #403
Conversation
There was a problem hiding this comment.
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)
50924e4 to
c31c74d
Compare
jessealama
changed the title
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 |
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 |
|
Converting to draft — splitting out the Sqrt/NatPair/NatUnpair layer as a smaller PR first: #445. |
|
@jessealama Can you resolve the merge conflicts here please? |
23e7a99 to
6d3692c
Compare
Done! I'd like to leave this as a draft for now; I'm a bit unhappy with a couple of the proofs and will spend some time cleaning them up. I'm open to any suggestions, of course, but just as a matter of review priority, I'm happy to put this on your backburner. |
|
@thomaskwaring I've done a bit of refactoring here that touches on Recursion.lean. I added a |
…air (leanprover#445) Implement SKI combinator terms for Nat.sqrt, Nat.pair, and Nat.unpair with correctness proofs against Mathlib definitions. Split out from leanprover#403 to make review easier. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…air (leanprover#445) Implement SKI combinator terms for Nat.sqrt, Nat.pair, and Nat.unpair with correctness proofs against Mathlib definitions. Split out from leanprover#403 to make review easier. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
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.
…ntions Shorten verbose docstrings, collapse rw/have/subst patterns to obtain rfl, extract inline calc blocks, and rename to camelCase (natPartrec_skiComputable, rfindAbove_induction).
Only one direction (Partrec → SKI) is proven; rename file and section header to avoid overclaiming equivalence. Remove unrelated SKIPartrec stub (converse direction) to a separate branch.
Add computes_of_total and RFindAbove_unfold helpers to eliminate repeated proof patterns. Simplify comp/pair_computes Part.mem chains and rfindAbove_induction via early subst + local helper. Remove dormant @[scoped grind] attributes from nil_correct and neg_correct.
Split the conjunction into `rfind_eval_root` (f evaluates to 0 at the root) and `rfind_eval_pos_below` (f evaluates to nonzero below k).
Add RFindAbove_correct' which works with pointwise Church encoding properties rather than requiring a total function. Restate the original RFindAbove_correct as a corollary.
- Extract prec_computes and rfind_computes as standalone lemmas, making codeToSKINat_correct a uniform 1-2 line per case induction. - Delete rfindAbove_induction (40 lines) by using the generalized RFindAbove_correct' from Recursion.lean. - Add bind_eq_some helper to simplify Part.mem_bind_iff extraction boilerplate in comp_computes and prec_rec_correct.
Promote the private helper to Part.eq_some_of_bind_eq_some in a new shared foundations file, making it available to other modules.
CI checkInitImports requires all Cslib modules to import Cslib.Init.
Place module docstrings before `@[expose] public section` per the style.header linter, restore upstream's 4-space continuation indent in rec_def, and update the Part.lean note now that mathlib4#37521 has merged (it is not yet in CSLib's Mathlib pin).
Collapse definitionally-true eval side conditions to rfl, drop eta-expansions, replace omega index-shuffling with grind per project convention, and use Nat.succ_pred_eq_of_ne_zero where the old proof already did. Net -21 lines, no statement changes.
Match the exact name and statement of the lemma added in mathlib4#37521 so that, once CSLib's Mathlib pin includes it, removing this file is a pure deletion with no call-site churn.
….lean Move the Computes predicate and the generic closure lemmas (computes_of_total, comp_computes, pair_computes) out of PartrecToSKI into a new Computable.lean, mirroring the URM Computes/Computable layout. Add a named SKI.Computable and restate natPartrec_skiComputable in terms of it. Generalize computes_of_total from Code.eval to any partial function, and make the Code-specific per-constructor lemmas private. This lets future files (e.g. the SKI → Partrec converse planned in Recursion.lean's TODO) use the computability notion without importing Mathlib.Computability.PartrecCode.
4efedc0 to
a001c4d
Compare
…air (leanprover#445) Implement SKI combinator terms for Nat.sqrt, Nat.pair, and Nat.unpair with correctness proofs against Mathlib definitions. Split out from leanprover#403 to make review easier. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
# Conflicts: # Cslib.lean
CSLib's Mathlib pin now includes leanprover-community/mathlib4#37521, which adds Part.bind_eq_some_iff. Delete the verbatim stopgap copy in Cslib/Foundations/Data/Part.lean and its imports; call sites in Computable.lean and PartrecToSKI.lean now resolve the lemma from Mathlib.Data.Part (pulled in transitively via Mathlib.Data.PFun).
… in Computes - Add reusable rec_correct' to Recursion.lean (primitive-recursion mirror of RFindAbove_correct') - State Computes via m ∈ f n, simplifying comp/pair_computes and rfind plumbing - Factor shared rfind extraction into rfind_eval_aux
|
I've iterated on this a bit and did some refactoring. There was a Mathlib PR we were depending on for a long time, but that's been resolved. I'd love it if this could get another look! |
3 participants
Prove that every
Nat.Partrecfunction on ℕ is SKI-computable (natPartrec_skiComputable). Translates all eightNat.Partrec.Codeconstructors to SKI terms and proves correctness, exercising the Recursion.lean infrastructure: primitive recursion (Rec), μ-recursion (RFind/RFindAbove), Nat pairing/unpairing, and integer square root.The general computability notions (
SKI.Computes,SKI.Computable) live in a newComputable.lean, mirroring the existingURM.Computes/URM.Computablelayout, so future files (e.g. the SKI → Partrec converse sketched in Recursion.lean's TODO) can use them without importingMathlib.Computability.PartrecCode.