feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities

[chris-anto-froeschl]

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. swap and permute) is welcome.

Files

AlphaEquivDefs.lean

Defines the α-equivalence relations studied in the paper. The definition corresponding to Definition 3.1 reuses the α-equivalence relation introduced in #458 (Basic.lean).

AlphaEquivEquiv.lean

Formalizes the main equivalence results between the different α-equivalence definitions.

SwapProperties.lean

Contains helper lemmas about swaps and permutations used throughout the proofs.

Notes

Early development used a custom implementation of swap. This has since been replaced by Equiv.swap from Mathlib.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.

[chris-anto-froeschl]

After the merge of #458, I took the liberty to refactor some operator-related properties into separate files. The current version therefore distinguishes between properties specific to swaps (SwapProperties.lean), renaming (RenameProperties.lean), and (main def) alpha equivalence (AlphaEquivProperties.lean).

I am open to discussion as to whether this is indeed the most elegant split. A single, larger Properties.lean could allow for some more elegant proofs. For example, in my local version of the follow-up PR, I prove reflexivity of AlphaEquiv using some swap properties. This is possible because the local Properties.lean freely mixes swap and AlphaEquiv properties as needed.

In general, however, most swap properties themselves depend on some AlphaEquiv properties, which prevents a cycle-free import structure. A more fine-grained separation of the files might be able to resolve this dependency issue.

On the other hand, collecting everything in Properties.lean would result in a rather large file.

[chris-anto-froeschl]

Furthermore, I'm considering cleaning up some of the proofs introduced in #458. Let me know whether you'd prefer me to leave those for a separate PR to avoid adding unnecessary noise to this one.