feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities - #741
Open
chris-anto-froeschl wants to merge 12 commits into
Open
feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities#741chris-anto-froeschl wants to merge 12 commits into
chris-anto-froeschl wants to merge 12 commits into
Conversation
…operty helper lemmas, updates references.bib to include alpha equivalence definition sources
…d, introduces agreement sets
chris-anto-froeschl
requested review from
chenson2018 and
fmontesi
as code owners
July 22, 2026 08:34
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
2 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.
Formalizes the definitions and proofs from Roy L. Crole's paper Alpha equivalence equalities.
This PR currently contains the formalization of Theorem 4.1 and its prerequisites to keep the review manageable. The remaining results are intended as follow-up PRs.
Status: blocked-by-other-PR. This PR depends on the open Basics of named representation PR and currently targets an intermediate revision that will need rebasing once that PR is merged.
The overall structure closely follows the original paper to simplify cross-referencing between the formalization and the published proofs. Feedback on the organization of the files and the placement of helper definitions (e.g.
swapandpermute) is welcome.Files
AlphaEquivDefs.leanDefines the α-equivalence relations studied in the paper. The definition corresponding to Definition 3.1 reuses the α-equivalence relation introduced in #458 (
Basic.lean).AlphaEquivEquiv.leanFormalizes the main equivalence results between the different α-equivalence definitions.
SwapProperties.leanContains helper lemmas about swaps and permutations used throughout the proofs.
Notes
Early development used a custom implementation of
swap. This has since been replaced byEquiv.swapfromMathlib.Logic.Equiv.Basic. I think the current version should be preferred.AI usage
Aristotle was used during exploration of alternative definitions and auxiliary swap lemmas. The final proofs were substantially rewritten, manually verified, and checked against the original paper.