feat(LambdaCalculus): basics of named representation (alpha equivalence and capture-avoiding substitution)

[yinhaoxuan]

Named representation of untyped lambda calculus.

Basic.lean

First, we define a naive variable renaming.
Second, we define alpha-equivalence according to "Gabbay and Pitts, A New Approach to Abstract Syntax with Variable Binding, 2002".
Third, we define capture-avoiding substitution.

Properties.lean

AlphaEquiv.refl: reflexivity of alpha-equivalence
AlphaEquiv.symm: symmetry of alpha-equivalence
AlphaEquiv.trans: transitivity of alpha-equivalence
Subst.relation_iff_function: the relational and functional definition of capture-avoiding substitution are equivalent, modulo alpha-equivalence
subst.commutativity: commutativity of substitution, more commonly known as "substitution lemma (e.g. in Barendregt 1984)"

[Copilot]

Pull request overview

Adds the first core results for a named untyped lambda-calculus development in CSLib, including α-equivalence and capture-avoiding substitution properties, complementing the existing Basic definitions.

Changes:

• Extend Named.Untyped.Basic with α-equivalence (AlphaEquiv), renaming utilities, and capture-avoiding substitution (subst / Subst).
• Add Named.Untyped.Properties proving key metatheory: α-equivalence is an equivalence relation and substitution lemmas (incl. commutativity/substitution lemma).
• Introduce supporting lemmas about variables, renaming, contexts, and preservation results.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean	Defines the syntax and core operations (fv/bv/vars, rename, α-equivalence, substitution + notation support).
Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean	Adds theorems establishing α-equivalence properties and capture-avoiding substitution metatheory.

[chenson2018]

I think the biggest things here are

• extracting out a well founded induction principle
• fixing the places where you have long simp only [...]; grind. To me these are mostly an indication of missing annotations
• some formatting style that I didn't comprehensively review and clutter up the PR with. It's mostly good, so if you could just take one more pass at thigns like indentation that would be appreciated.
• seeing if there's any way to split up some of these very large proofs, but maybe this is inherently difficult

It's also generally a bit hard to make sure there aren't errors with the substitution definition until this has more usage. I've had the thought that it would be nice to have a larger set of tests to safeguard around any incorrect definitions, based on something like https://github.com/sweirich/lambda-n-ways/. (Not asking you to do this, just a thought for a future PR)