feat(CombinatoryLogic): add Church-encoded list infrastructure for SKI terms#331
Merged
chenson2018 merged 5 commits intoleanprover:mainfrom Feb 17, 2026
Merged
Conversation
jessealama
force-pushed
the
ski-church-encoding
branch
from
437f9de to
fc0777e
Compare
thomaskwaring
approved these changes
Feb 17, 2026
Contributor
thomaskwaring
left a comment
thomaskwaring
left a comment
There was a problem hiding this comment.
Looks great to me :-)
jessealama
force-pushed
the
ski-church-encoding
branch
from
3194025 to
4620803
Compare
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.
jessealama
force-pushed
the
ski-church-encoding
branch
2 times, most recently
from
07eb042 to
7920a16
Compare
…I 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.
jessealama
force-pushed
the
ski-church-encoding
branch
from
7920a16 to
ba119cd
Compare
chenson2018
requested changes
Feb 17, 2026
Collaborator
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Some small style reviews, but this looks good to me.
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Thanks to chenson2018 for the feedback.
Contributor
Author
Thank you! I took a look. Nice idea about the structure for Church pair verification. |
chenson2018
approved these changes
Feb 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds Church-encoded list operations (nil, cons, head, tail) for SKI combinatory logic, along with conversions to/from Church numerals and helper combinators (PrependZero, SuccHead).
Head is defined via a general HeadD that takes an arbitrary default value; Head specializes to default 0.
This is a stepping stone toward proving the equivalence of SKI combinatory logic with Mathlib's Turing machines.