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

Cslib.lean

@@ -157,8 +157,12 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivEquiv
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
-public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.RenameProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties
 public import Cslib.Languages.Mech.Choreography.Basic
 public import Cslib.Languages.Mech.LocalComputation
 public import Cslib.Languages.StatefulProcesses.Basic

Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean

@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+
+/-! # Definitions of α-equivalence
+
+Five definitions of α-equivalence from [Crole2012], each capturing the same equivalence
+relation on expressions:
+
+* `∼p`  (Definition 3.1): Permutation-based with non-occurrence side condition (`AlphaEquiv`)
+* `∼p#` (Definition 3.2): Permutation-based with freshness side condition (`AlphaEquivPFresh`)
+* `∼¹p` (Definition 3.3): Permutation-based with non-occurrence on bodies only (`AlphaEquivP1`)
+* `∼r`  (Definition 3.4): Traditional renaming axiom with non-occurrence (`AlphaEquivR`)
+* `∼r#` (Definition 3.5): Renaming axiom with freshness (`AlphaEquivRFresh`)
+
+The first three definitions use the notion of *atom swapping* (transposition), introduced in
+[Gabbay2002] (Section 2, page 3), as a primitive operation for defining α-equivalence. The
+key observation from [Gabbay2002] is that α-equivalence can be defined using the notion of
+atom swapping in lieu of the traditional renaming/substitution approach.
+
+The last two definitions use the traditional capture-avoiding substitution (renaming) axiom.
+
+## References
+
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012]
+* [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with Variable Binding*][Gabbay2002]
+
+## Notation
+
+Following the paper [Crole2012], we use the following correspondence between the paper's
+abstract syntax and the λ-calculus terms:
+
+| Paper         | Lean                |
+|---------------|---------------------|
+| `a`           | `Term.var x`        |
+| `P(E₁, E₂)`   | `Term.app m1 m2`    |
+| `B([a]E)`     | `Term.abs x m`      |
+| `(z a) · E`   | `m.swap x z`        |
+| `E{a'/a}`     | `m.subst a (var a')`|
+| `π · E`       | `m.permute π`       |
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.Named.Untyped.Term
+
+/-- **Definition 3.2** [Crole2012]: `∼p#` - α-equivalence via permutation with freshness
+side condition.
+
+The rule `pi#` uses the freshness condition `z # a, b, E, E'`
+(i.e., `z ∉ fv(E) ∪ fv(E') ∪ {a, b}`) instead of the non-occurrence condition
+`z ∉ vars(E) ∪ vars(E') ∪ {a, b}` used in Definition 3.1 (`AlphaEquiv`).
+-/
+inductive AlphaEquivPFresh : Term Var → Term Var → Prop where
+  | var {x : Var} : AlphaEquivPFresh (var x) (var x)
+  | abs {y x1 x2 : Var} {m1 m2 : Term Var} :
+    y ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv →
+    AlphaEquivPFresh (m1.swap x1 y) (m2.swap x2 y) →
+    AlphaEquivPFresh (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivPFresh m1 n1 → AlphaEquivPFresh m2 n2 →
+    AlphaEquivPFresh (app m1 m2) (app n1 n2)
+
+/-- **Definition 3.3** [Crole2012]: `∼¹p` - α-equivalence via permutation with non-occurrence
+restricted to the bodies only.
+
+This definition is analogous to the definition of α-equivalence for λ-expressions in
+[Gabbay1999a] (Theorem 2.1, page 216). The notation `∼¹p` arises from three variants `∼ⁱp`
+of `∼p` considered in Proposition 4.3 of [Crole2012].
+-/
+inductive AlphaEquivP1 : Term Var → Term Var → Prop where
+  | var {x : Var} : AlphaEquivP1 (var x) (var x)
+  | abs {y x1 x2 m1 m2} :
+    y ∉ m1.vars ∪ m2.vars →
+    AlphaEquivP1 (m1.rename x1 y) (m2.rename x2 y) →
+    AlphaEquivP1 (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivP1 m1 n1 → AlphaEquivP1 m2 n2 →
+    AlphaEquivP1 (app m1 m2) (app n1 n2)
+
+/-- **Definition 3.4** [Crole2012]: `∼r` - α-equivalence via the traditional renaming axiom
+with non-occurrence side condition.
+
+This definition is analogous to the definition of α-equivalence for λ-expressions most commonly
+found in the literature. One of the first formal presentations is in [Church1941] and the same,
+though rather less formal approach is taken by [Barendregt1985] (Definition 2.1.11).
+-/
+inductive AlphaEquivR : Term Var → Term Var → Prop where
+  | refl {m : Term Var} : AlphaEquivR m m
+  | symm {m1 m2 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m1
+  | trans {m1 m2 m3 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m3 → AlphaEquivR m1 m3
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivR m1 n1 → AlphaEquivR m2 n2 →
+    AlphaEquivR (app m1 m2) (app n1 n2)
+  | abs_congr {x : Var} {m m' : Term Var} :
+    AlphaEquivR m m' →
+    AlphaEquivR (abs x m) (abs x m')
+  | alpha {x x' : Var} {m : Term Var} :
+    x' ∉ ({x} : Finset Var) ∪ m.vars →
+    AlphaEquivR (abs x m) (abs x' (m.subst x (var x')))
+
+/-- **Definition 3.5** [Crole2012]: `∼r#` - α-equivalence via the renaming axiom with
+freshness side condition.
+
+Same as `∼r` (Definition 3.4), but the renaming axiom uses a freshness side condition
+(`a' ∉ {a} ∪ fv(E)`) instead of a non-occurrence condition (`a' ∉ {a} ∪ vars(E)`).
+
+This is analogous to the definition of α-equivalence for λ-expressions one finds in
+[Hindley1988] (Section 1B, page 9).
+-/
+inductive AlphaEquivRFresh : Term Var → Term Var → Prop where
+  | refl {m : Term Var} : AlphaEquivRFresh m m
+  | symm {m1 m2 : Term Var} :
+    AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m1
+  | trans {m1 m2 m3 : Term Var} :
+    AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m3 →
+    AlphaEquivRFresh m1 m3
+  | app {m1 m1' m2 m2' : Term Var} :
+    AlphaEquivRFresh m1 m1' → AlphaEquivRFresh m2 m2' →
+    AlphaEquivRFresh (app m1 m2) (app m1' m2')
+  | abs_congr {x : Var} {m m' : Term Var} :
+    AlphaEquivRFresh m m' →
+    AlphaEquivRFresh (abs x m) (abs x m')
+  | alpha {x x' : Var} {m : Term Var} :
+    x' ∉ ({x} : Finset Var) ∪ m.fv →
+    AlphaEquivRFresh (abs x m) (abs x' (m.subst x (var x')))
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib

Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.RenameProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties
+
+/-! # Equivalence of α-equivalence definitions
+
+Theorems showing equivalence of the five definitions of α-equivalence from [Crole2012]:
+
+* `∼p`  (Definition 3.1): permutation with non-occurrence side condition (`AlphaEquiv`)
+* `∼p#` (Definition 3.2): permutation with freshness side condition (`AlphaEquivPFresh`)
+* `∼¹p` (Definition 3.3): permutation with non-occurrence on bodies only (`AlphaEquivP1`)
+* `∼r`  (Definition 3.4): traditional renaming axiom with non-occurrence (`AlphaEquivR`)
+* `∼r#` (Definition 3.5): renaming axiom with freshness (`AlphaEquivRFresh`)
+
+The main results are:
+
+* **Theorem 4.1** [Crole2012]: `∼p = ∼p#` (`alphaEquiv_iff_alphaEquivPFresh`)
+* **Theorem 4.2** [Crole2012]: `∼p = ∼¹p` (`alphaEquiv_iff_alphaEquivP1`)
+* **Theorem 4.4** [Crole2012]: `∼p = ∼r`  (`alphaEquiv_iff_alphaEquivR`)
+* **Theorem 4.5** [Crole2012]: `∼p = ∼r#` (`alphaEquiv_iff_alphaEquivRFresh`)
+* **Theorem 4.6** [Crole2012]: `∼r = ∼r#` (`alphaEquivR_iff_alphaEquivRFresh`)
+
+## References
+
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012]
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.Named.Untyped.Term
+
+omit [HasFresh Var] in
+/-- Non-occurrence obviously implies freshness, and the `swap` operation coincides with
+`rename` when the target variable does not occur in the term.
+-/
+lemma alphaEquiv_of_alphaEquivPFresh {m n : Term Var} : AlphaEquiv m n → AlphaEquivPFresh m n := by
+  intro h
+  induction h with
+  | var => constructor
+  | abs z_h1 ih1 ih2 =>
+    rename_i x z x1 x2 m1 m2
+    have h1 : z ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv := by
+      simp_all [vars_either_fv_or_bv]
+    have h2 : AlphaEquivPFresh (m1.swap x1 z) (m2.swap x2 z) := by
+      grind [swap_eq_rename_of_not_mem_vars]
+    apply AlphaEquivPFresh.abs h1 h2
+  | app h1 h2 ih1 ih2 => exact AlphaEquivPFresh.app ih1 ih2
+
+lemma alphaEquivPFresh_of_alphaEquiv {m n : Term Var} : AlphaEquivPFresh m n → AlphaEquiv m n := by
+  intro h
+  induction h with
+  | var => constructor
+  | abs hy _h ih =>
+    rename_i u a b E E'
+    -- We have: (u a) · E ∼p (u b) · E' (by induction: ih) and u # a, b, E, E' (by hy).
+    -- Extract freshness conditions from hy.
+    have hu_E : u ∉ E.fv := by aesop
+    have hu_E' : u ∉ E'.fv := by aesop
+    -- Pick z ≠ u with z ∉ vars(E) ∪ vars(E') ∪ {a, b} (stronger than freshness).
+    obtain ⟨z, hz⟩ : ∃ z : Var, z ∉ E.vars ∪ E'.vars ∪ {a, b, u} := by
+      exact Infinite.exists_notMem_finset (E.vars ∪ E'.vars ∪ {a, b, u})
+    have hz_E : z ∉ E.vars := by aesop
+    have hz_E' : z ∉ E'.vars := by aesop
+    have hz_fv_E : z ∉ E.fv := by simp_all [vars_either_fv_or_bv]
+    have hz_fv_E' : z ∉ E'.fv := by simp_all [vars_either_fv_or_bv]
+    -- Using Lemma 6.1 we get
+    have h_swap : ((E.swap u a).swap z u) =α ((E'.swap u b).swap z u) := by
+      nth_rw 2 [swap_comm]
+      nth_rw 4 [swap_comm]
+      exact AlphaEquiv.swap_preserve ih
+    -- From Lemma 6.2 part 2 via agreement sets
+    have h_agree_E : ((E.swap u a).swap z u) =α (E.swap z a) :=
+      swap_comp_alphaEquiv_of_not_mem_fv hu_E hz_fv_E
+    have h_agree_E' : ((E'.swap u b).swap z u) =α (E'.swap z b) :=
+      swap_comp_alphaEquiv_of_not_mem_fv hu_E' hz_fv_E'
+    -- Chain by symmetry and transitivity of ∼p
+    -- (z a) · E ∼p (z u)·(u a)·E ∼p (z u)·(u b)·E' ∼p (z b) · E'
+    have h_chain : (E.swap z a) =α (E'.swap z b) :=
+      AlphaEquiv.trans (AlphaEquiv.symm h_agree_E) (AlphaEquiv.trans h_swap h_agree_E')
+    -- Convert swap to rename (since z ∉ vars) and apply the pi rule.
+    -- Since z ∉ vars(E), swap z a = rename a z (by swap_comm + swap_eq_rename).
+    rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E] at h_chain
+    rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E'] at h_chain
+    exact AlphaEquiv.abs (by aesop) h_chain
+  | app _ _ ih1 ih2 => exact AlphaEquiv.app ih1 ih2
+
+/-! ## Theorem 4.1 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivPFresh (m n : Term Var) : AlphaEquiv m n ↔ AlphaEquivPFresh m n :=
+  ⟨alphaEquiv_of_alphaEquivPFresh, alphaEquivPFresh_of_alphaEquiv⟩
+
+/-
+/-! ## Theorem 4.2 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivP1 (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivP1 m n := by
+  sorry
+
+/-! ## Theorem 4.4 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivR (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivR m n := by
+  sorry
+
+/-! ## Theorem 4.5 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivRFresh (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivRFresh m n := by
+  sorry
+
+/-! ## Theorem 4.6 [Crole2012] -/
+theorem alphaEquivR_iff_alphaEquivRFresh (m n : Term Var) :
+    AlphaEquivR m n ↔ AlphaEquivRFresh m n := by
+  sorry
+-/
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib