wip: name abstractions form a nominal set

1 files changed, 24 insertions, 5 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index bb654ed..b4a6cee 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -207,8 +207,7 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y →
   · intro c ⟨hxy, hyz⟩
     rw [hxy, hyz]
 
-/-- Alpha-equivalence is an equivariant relation. -/
-lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by
+private lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by
   intro x y π h
   rw [alpha_eq_iff_exists] at *
   obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
@@ -236,20 +235,40 @@ section Quotient
 variable (X : Type) [NominalSet 𝔸 X]
 
 /-- Associate the name abstraction structure with alpha-equivalence. -/
-instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where
+instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸 X) where
   r := AlphaEq
   iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩
+  equivariant := alpha_eq_equivariant
 
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
-def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
+def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid
 
 /-- 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 :=
-  Quotient.mk (setoid 𝔸 X) (.mk a 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
 
+instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
+
+@[simp]
+lemma NameAbstraction.smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr
+
+@[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
+
 end Quotient
 
 /-!