fix(LambdaCalculus): change from rename to swap in alpha equivalence

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

@@ -61,7 +61,9 @@ inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term
   | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
   | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
 
-/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
+/-- Renaming, or variable substitution. `m.rename x y` renames the free occurrences of `x` into
+`y` in `m`. This operation is not capture-avoiding, so callers must ensure that `y` is fresh when
+capture matters. -/
 def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
   match m with
   | var z => if z = x then (var y) else (var z)
@@ -73,6 +75,21 @@ def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
       abs z (m'.rename x y)
   | app n1 n2 => app (n1.rename x y) (n2.rename x y)
 
+/-- Structurally swap the variable names `x` and `y`, including abstraction binders. Unlike
+`Term.rename`, swapping preserves the binding structure even when one of the names already occurs
+bound in the term. -/
+def Term.swap [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
+  match m with
+  | var z => var (Equiv.swap x y z)
+  | abs z m' => abs (Equiv.swap x y z) (m'.swap x y)
+  | app n₁ n₂ => app (n₁.swap x y) (n₂.swap x y)
+
+/-- Swapping the same two variable names twice leaves a term unchanged. -/
+@[simp]
+theorem Term.swap_swap [DecidableEq Var] (m : Term Var) (x y : Var) :
+    (m.swap x y).swap x y = m := by
+  induction m <;> simp [Term.swap, *]
+
 /-- Renaming preserves size. -/
 @[simp]
 theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
@@ -146,9 +163,9 @@ open Term
 
 /-- α-equivalence. -/
 inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
--- The α-axiom
+-- The α-axiom, using nominal swapping to preserve binding structure.
 | ax {m : Term Var} {x y : Var} :
-  y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.rename x y))
+  y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.swap x y))
 -- Equivalence relation rules
 | refl : AlphaEquiv m m
 | symm : AlphaEquiv m n → AlphaEquiv n m

CslibTests/LambdaCalculus.lean

@@ -20,6 +20,35 @@ example : (abs 0 (var 0)) =α (abs 1 (var 1)) := by
   constructor
   simp [Term.fv]
 
+-- Swapping also renames the colliding inner binder, preserving which abstraction binds each
+-- variable occurrence.
+example :
+    (abs 0 (abs 1 (var 0)) : NatTerm) =α (abs 1 (abs 0 (var 1))) := by
+  apply AlphaEquiv.ax
+  simp [Term.fv]
+
+-- The old one-way renaming axiom instead produced this captured term.
+example : True := by
+  fail_if_success
+    exact (AlphaEquiv.ax
+      (m := abs 1 (var 0))
+      (x := 0)
+      (y := 1)
+      (by simp [Term.fv]) :
+      (abs 0 (abs 1 (var 0)) : NatTerm) =α (abs 1 (abs 1 (var 1))))
+  trivial
+
+-- Unlike requiring freshness for every variable name, nominal swapping permits a new binder name
+-- that already occurs bound in the body.
+example :
+    (abs 0 (abs 1 (var 1)) : NatTerm) =α (abs 1 (abs 1 (var 1))) := by
+  apply AlphaEquiv.trans (m2 := abs 1 (abs 0 (var 0)))
+  · apply AlphaEquiv.ax
+    simp [Term.fv]
+  · apply AlphaEquiv.ctx (c := Context.abs 1 Context.hole)
+    apply AlphaEquiv.ax
+    simp [Term.fv]
+
 example : (abs 1 (var 0)).subst 0 (app (var 1) (var 2)) = (abs 3 (app (var 1) (var 2))) := by
   simp +instances [subst, fv, bv, vars, rename, instHasFreshNat, HasFresh.ofSucc]