From c3700706466cb8fb9ed287ea066b656caacdc9c7 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Sat, 25 Oct 2025 01:07:56 +0200
Subject: start working on alpha equivalence proofs

---
 Nominal/Equivariance.lean          | 16 +++++++
 Nominal/Instances/Abstraction.lean | 86 ++++++++++++++++++++++++++++++++++----
 Nominal/Permutations.lean          |  5 +++
 3 files changed, 99 insertions(+), 8 deletions(-)

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 50cf7c2..57c6d11 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -161,6 +161,17 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Inj
 
 end Equivariant
 
+/-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/
+def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) (hequi : Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where
+  fin_supp := by
+    intro y
+    obtain ⟨x, hx⟩ := hsurj y
+    use (NominalSet.supp 𝔸 x)
+    constructor
+    · rw [← hx]
+      exact Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸)
+    · exact supp_finite 𝔸
+
 /-- supp is an equivariant function. -/
 lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by
   intro x π; ext a; constructor
@@ -182,6 +193,11 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
     · apply Set.Finite.smul_set
       exact hS.out.right
 
+/-- Freshness is an equivariant relation. -/
+lemma NominalSet.fresh_equivariant : EquivariantRelation 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by
+  intro x y π h
+  rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff]
+
 end Nominal
 
 /-!
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index d7fade9..508167e 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -22,15 +22,15 @@ This structure, along with the obvious permutation action, forms a nominal set w
 -/
 section RawStructure
 
-variable (X : Type) [NominalSet 𝔸 X]
-
 /-- The structure forming a name abstraction. -/
-structure NameAbstraction' where
+structure NameAbstraction' (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) [NominalSet 𝔸 X] where
   /-- The atom that is abstracted away. -/
   atom : 𝔸
   /-- The body from which the atom is abstracted. -/
   body : X
 
+variable (X : Type) [NominalSet 𝔸 X]
+
 attribute [ext] NameAbstraction'
 
 namespace NameAbstraction'
@@ -38,7 +38,7 @@ namespace NameAbstraction'
 instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where
   smul π x := .mk (π • x.atom) (π • x.body)
 
-@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π x.atom := rfl
+@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π • x.atom := rfl
 
 @[simp] lemma smul_body (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).body = π • x.body := rfl
 
@@ -46,10 +46,32 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
   one_smul := by intro _; ext <;> simp [one_smul]
   mul_smul := by intro _ _ _; ext <;> simp [mul_smul]
 
-instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) where
-  fin_supp := sorry
+private def ofPair (x : (𝔸 × X)) : NameAbstraction' 𝔸 X := ⟨x.fst, x.snd⟩
+
+private lemma ofPair_injective : Function.Injective (ofPair 𝔸 X) := by
+  intro x y hxy
+  simp only [ofPair, mk.injEq] at hxy
+  ext
+  · exact hxy.left
+  · exact hxy.right
+
+private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by
+  intro x
+  use ⟨x.atom, x.body⟩
+  simp [ofPair]
+
+private lemma ofPair_equivariant : Equivariant 𝔸 (ofPair 𝔸 X) := by
+  intro x π
+  ext <;> simp [ofPair]
+
+instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) :=
+  NominalSet.fromEquivariantSurjective 𝔸 (ofPair 𝔸 X) (ofPair_equivariant 𝔸 X) (ofPair_surjective 𝔸 X)
 
-@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by sorry
+@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by
+  have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) :=
+    Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X)
+  simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h
+  rwa [Set.union_comm] at h
 
 @[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by
   simp [NominalSet.IsFresh]
@@ -91,6 +113,7 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred
   simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h'
   simpa [smul_smul]
 
+/-- The freshness quantifier in the definition is equivalent to "there exists some c # (x, y)". -/
 lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
   suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEqPred c (x, y)) by
     rw [alpha_eq_iff_pred, this]
@@ -98,6 +121,7 @@ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred, @and_assoc]
 
+/-- The freshness quantifier in the definition is equivalent to "for all c # (x, y)". -/
 lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
   suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by
     rw [alpha_eq_iff_pred, this]
@@ -105,7 +129,53 @@ lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c,
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred]
 
-lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry
+/-- An alternative definition of α-equivalence:
+
+For ⟪a⟫ x = ⟪b⟫ y, we either have (a, x) = (b, y) or x is just (a b) y, requiring that a is not in the support of y. -/
+lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y.body ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by
+  by_cases h_eq : x.atom = y.atom
+  · constructor
+    · sorry
+    · sorry
+  · constructor
+    · rw [alpha_eq_iff_exists]
+      intro h; right
+      obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
+      constructor
+      · exact h_eq
+      · simp at hcx
+        simp at hcy
+        have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body :=
+          NominalSet.fresh_equivariant 𝔸 _ _ _ hcx.right
+        -- TODO: Refactor into lemma
+        have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by
+          ext a
+          simp [FPerm.swap]
+          by_cases h₁ : (a = c) <;> by_cases h₂ : (a = x.atom) <;> by_cases h₃ : (a = y.atom)
+          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
+          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
+          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
+          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
+          · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left]
+          · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left]
+          · simp [h₃, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
+          · simp [Equiv.swap_apply_of_ne_of_ne h₁ h₃, Equiv.swap_apply_of_ne_of_ne h₁ h₂, Equiv.swap_apply_of_ne_of_ne h₂ h₃]
+        rw [mul_smul, PermSet.atom_swap, PermSet.atom_swap, Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq] at h_atom
+        rw [mul_smul, hc, ← mul_smul, FPerm.swap_mul_self, one_smul] at h_atom
+        constructor
+        · exact h_atom
+        · calc
+            x.body = ⸨c, x.atom⸩ • ⸨c, x.atom⸩ • x.body      := by rw [← mul_smul, FPerm.swap_mul_self, one_smul]
+            _      = (⸨c, x.atom⸩ * ⸨c, y.atom⸩) • y.body    := by rw [mul_smul, hc]
+            _      = ⸨x.atom, y.atom⸩ • ⸨c, x.atom⸩ • y.body := by rw [← mul_smul, h_swap]
+            _      = ⸨x.atom, y.atom⸩ • y.body               := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom]
+    · rw [alpha_eq_iff_all]
+      intro h c ⟨hcx, hcy⟩
+      simp at hcy
+      simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h
+      -- TODO: Use new lemma from before
+      have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := sorry
+      rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left]
 
 private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry
 
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index b8d510e..62d7470 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -133,6 +133,11 @@ lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a,
   apply ext
   apply Equiv.mul_swap_eq_swap_mul
 
+/-- Lifting of Equiv.swap_mul_self to finite permutations. -/
+lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by
+  apply ext
+  simp [swap]
+
 /-- If c is not equal to a or b, then (a b) leaves c unchanged. -/
 lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by
   intro ha hb
-- 
cgit v1.3.1