From 6b8b43eedf972cbfff8c97657a0a6a1300dcb140 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Tue, 28 Oct 2025 14:56:12 +0100
Subject: more wip

---
 Nominal/Instances/Abstraction.lean | 83 +++++++++++++++++++++++++++++++-------
 1 file changed, 68 insertions(+), 15 deletions(-)

(limited to 'Nominal/Instances/Abstraction.lean')

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index b4a6cee..76cb360 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -243,31 +243,84 @@ instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
 def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid
 
+namespace NameAbstraction
+
 /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
-def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
+def mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
   Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x)
 
 /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
-notation "⟪" a "⟫ " t => NameAbstraction.mk a t
+notation "⟪" a "⟫ " t => mk a t
 
 instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
 
 @[simp]
-lemma NameAbstraction.smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr
+lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr
+
+/-- Two name abstractions are equal iff they are alpha-equivalent. -/
+lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by
+  rw [mk, mk, Quotient.eq_iff_equiv]
+  rfl
+
+/-- Lifting of alpha_eq_iff_exists to name abstractions. -/
+lemma eq_iff_exists {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by
+  simp only [eq_iff_alpha_eq, alpha_eq_iff_exists, NameAbstraction'.fresh, ne_eq]
+  ac_nf
+
+/-- Lifting of alpha_eq_iff_exists to name abstractions. -/
+lemma eq_iff_all  {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by
+  simp only [eq_iff_alpha_eq, alpha_eq_iff_all, NameAbstraction'.fresh, ne_eq]
+  ac_nf
+
+/-- Lifting of alpha_eq_iff_cases to name abstractions. -/
+lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by
+  simp [eq_iff_alpha_eq, alpha_eq_iff_cases]
 
 @[simp]
-lemma NameAbstraction.supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by
-  sorry
-  -- ext b; constructor
-  -- · apply NominalSet.support_subset_supp 𝔸
-  --   · intro π hπ
-  --     simp [PermSet.fix']
-
-  --     sorry
-  --   · exact Set.Finite.diff (NominalSet.supp_finite 𝔸)
-  -- · rw [mk, Quotient.supp]
-  --   intro hb x' hx'
-  --   sorry
+lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by
+  have hswap : ∀ (b : 𝔸) (y : X), (⟪a⟫ x) = (⟪b⟫ y) → NominalSet.supp 𝔸 (⟨b, y⟩ : NameAbstraction' 𝔸 X) = {b} ∪ (NominalSet.supp 𝔸 x \ {a}) := by
+    intro b y heq
+    rw [eq_iff_cases] at heq
+    cases heq with
+    | inl h =>
+      rw [h.left, h.right]
+      simp only [NameAbstraction'.supp, Set.union_singleton, Set.union_diff_self, Set.singleton_union]
+    | inr h =>
+      simp only [NameAbstraction'.supp, Set.union_comm]
+      rw [h.right.right, NominalSet.supp_equivariant 𝔸 y ⸨a, b⸩]
+      ext c
+      by_cases h₁ : c = b
+      · simp [h₁]
+      · by_cases h₂ : c = a
+        · simp [h₂, show a ∉ NominalSet.supp 𝔸 y by exact h.right.left]
+        · simp [h₁, h₂, ← PermSet.atom_set_swap_ne_ne]
+  rw [mk, Quotient.supp]
+  ext b
+  constructor
+  · contrapose; intro h
+    simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, Classical.not_imp, not_forall, not_or]
+    have hfin : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸
+    obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin.toFinset ∪ {a, b})
+    simp only [Finset.union_insert, Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc
+    use ⟨c, ⸨a, c⸩ • x⟩
+    constructor
+    · apply Quotient.exact
+      rw [← mk, ← mk, eq_iff_cases]
+      right
+      exact ⟨hc.left, hc.right.right, by rw [FPerm.swap_comm]⟩
+    · constructor
+      · exact Ne.symm hc.right.left
+      · simp
+        sorry
+  · intro h x' hx'
+    suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by
+      rw [this]
+      exact Set.mem_union_right {x'.atom} h
+    apply hswap
+    apply Quotient.sound
+    exact (Setoid.symm hx')
+
+end NameAbstraction
 
 end Quotient
 
-- 
cgit v1.3.1