refactor equivariance namespaces

3 files changed, 50 insertions, 50 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 3166e71..7087076 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -20,23 +20,19 @@ section Definition
 variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
 
 /-- A function is equivariant if it is invariant to applying a permutation before or after the function. -/
-def Equivariant (f : X β†’ Y) : Prop :=
+def Function.Equivariant (f : X β†’ Y) : Prop :=
   βˆ€ (x : X) (Ο€ : FPerm 𝔸), f (Ο€ β€’ x) = Ο€ β€’ f x
 
 /-- A set is equivariant if it is closed under permutations. -/
-def EquivariantSet (S : Set X) : Prop :=
+def Set.Equivariant (S : Set X) : Prop :=
   βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S β†’ Ο€ β€’ x ∈ S
 
 /-- A binary relation is equivariant if it is closed under permutations. -/
-def EquivariantRelation (R : Rel X Y) : Prop :=
+def Rel.Equivariant (R : Rel X Y) : Prop :=
   βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y β†’ R (Ο€ β€’ x) (Ο€ β€’ y)
 
-/-- Extended setoid definition that also requires the relation to be equivariant. -/
-class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where
-  equivariant : EquivariantRelation 𝔸 r
-
 /-- For equivariant sets, we even have "if and only if". -/
-lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S ↔ Ο€ β€’ x ∈ S := by
+lemma Set.Equivariant.iff {S : Set X} : Set.Equivariant 𝔸 S ↔ βˆ€ (x : X) (Ο€ : FPerm 𝔸), x ∈ S ↔ Ο€ β€’ x ∈ S := by
   constructor
   Β· intro h x Ο€; constructor
     Β· intro hx; exact h x Ο€ hx
@@ -48,7 +44,7 @@ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ βˆ€ (x : X) (Ο
     exact (h x Ο€).mp hx
 
 /-- For equivariant relations, we even have "if and only if". -/
-lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𝔸 R ↔ βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y ↔ R (Ο€ β€’ x) (Ο€ β€’ y) := by
+lemma Rel.Equivariant.iff {R : Rel X Y} : Rel.Equivariant 𝔸 R ↔ βˆ€ (x : X) (y : Y) (Ο€ : FPerm 𝔸), R x y ↔ R (Ο€ β€’ x) (Ο€ β€’ y) := by
   constructor
   Β· intro h x y Ο€; constructor
     Β· intro hxy; exact h x y Ο€ hxy
@@ -71,18 +67,18 @@ section Trivial
 variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z]
 
 /-- The identity function is equivariant. -/
-lemma id_equivariant : Equivariant 𝔸 (id : X β†’ X) := by
-  simp [Equivariant]
+lemma id_equivariant : Function.Equivariant 𝔸 (id : X β†’ X) := by
+  simp [Function.Equivariant]
 
 /-- The composition of two equivariant functions is equivariant. -/
-lemma comp_equivariant {f : Y β†’ Z} {g : X β†’ Y} : Equivariant 𝔸 f β†’ Equivariant 𝔸 g β†’ Equivariant 𝔸 (f ∘ g) := by
+lemma comp_equivariant {f : Y β†’ Z} {g : X β†’ Y} : Function.Equivariant 𝔸 f β†’ Function.Equivariant 𝔸 g β†’ Function.Equivariant 𝔸 (f ∘ g) := by
   intro hf hg x Ο€
   calc
     f (g (Ο€ β€’ x)) = f (Ο€ β€’ g x)   := by rw [hg]
     _             = Ο€ β€’ (f (g x)) := by rw [hf]
 
 /-- The subset relation is equivariant. -/
-lemma subset_equivariant : EquivariantRelation 𝔸 (Set.Subset : Set X β†’ Set X β†’ Prop) := by
+lemma Set.subset_equivariant : Rel.Equivariant 𝔸 (Set.Subset : Set X β†’ Set X β†’ Prop) := by
   intro S T Ο€ hST x hx
   rw [Set.mem_smul_set_iff_inv_smul_mem] at hx
   rw [Set.mem_smul_set_iff_inv_smul_mem]
@@ -99,7 +95,7 @@ section Support
 
 variable {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y]
 
-namespace Equivariant
+namespace Function.Equivariant
 
 /-- Equivariant functions preserve supports. -/
 lemma preserve_support {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant 𝔸 f β†’ PermSet.HasSupport 𝔸 x S β†’ PermSet.HasSupport 𝔸 (f x) S := by
@@ -118,10 +114,10 @@ lemma preserve_support_inj {x : X} {f : X β†’ Y} {S : Set 𝔸} : Equivariant π
     have : Ο€ β€’ f x = f x := hsupp hΟ€
     contradiction
 
-end Equivariant
+end Function.Equivariant
 
 /-- HasSupport is an equivariant relation. -/
-lemma PermSet.support_equivariant : EquivariantRelation 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by
+lemma PermSet.support_equivariant : Rel.Equivariant 𝔸 (HasSupport 𝔸 : X β†’ Set 𝔸 β†’ Prop) := by
   intro x S π hS σ hσ
   have hfix : (π⁻¹ * Οƒ * Ο€) ∈ fix 𝔸 S := by
     intro a ha
@@ -149,7 +145,7 @@ section Nominal
 
 variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
-namespace Equivariant
+namespace Function.Equivariant
 
 /-- If f is equivariant, then supp (f x) βŠ† supp x. -/
 lemma supp_subset {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β†’ NominalSet.supp 𝔸 (f x) βŠ† NominalSet.supp 𝔸 x := by
@@ -173,21 +169,21 @@ lemma preserve_fresh_inj {a : 𝔸} {x : X} {f : X β†’ Y} : Equivariant 𝔸 f β
   intro hequi hinj
   rw [NominalSet.IsFresh, NominalSet.IsFresh, supp_eq_if_inj 𝔸 hequi hinj]
 
-end Equivariant
+end Function.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
+def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X β†’ Y) (hequi : Function.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 Function.Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸)
     Β· exact supp_finite 𝔸
 
 /-- supp is an equivariant function. -/
-lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by
+lemma NominalSet.supp_equivariant : Function.Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸) := by
   intro x Ο€; ext a; constructor
   Β· apply support_subset_supp 𝔸
     Β· apply PermSet.support_equivariant
@@ -208,7 +204,7 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X β†’ Set 𝔸
       exact hS.out.right
 
 /-- Freshness is an equivariant relation. -/
-lemma NominalSet.fresh_equivariant : EquivariantRelation 𝔸 (NominalSet.IsFresh : 𝔸 β†’ X β†’ Prop) := by
+lemma NominalSet.fresh_equivariant : Rel.Equivariant 𝔸 (NominalSet.IsFresh : 𝔸 β†’ X β†’ Prop) := by
   intro x y Ο€ h
   rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff]
 
@@ -221,13 +217,13 @@ For propositions of the form `И a, a R x`, where `R` is an equivariant relation
 -/
 section Freshness
 
-namespace Equivariance
+namespace Rel.Equivariant
 
 variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
 
 -- We continue with a circular implication chain argument to show these equivalences.
 
-private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by
+private lemma for_fresh_iff₁ : Equivariant 𝔸 R β†’ (И a, R a x) β†’ (βˆƒ a, a # x ∧ R a x) := by
   intro hequi h
   apply Set.Finite.infinite_compl at h
   simp at h
@@ -236,7 +232,7 @@ private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R β†’ (И a, R a x) β†
   simp only [Set.mem_diff, Set.mem_setOf_eq] at ha
   use a; exact ha.symm
 
-private lemma for_fresh_iffβ‚‚ : EquivariantRelation 𝔸 R β†’ (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by
+private lemma for_fresh_iffβ‚‚ : Equivariant 𝔸 R β†’ (βˆƒ a, a # x ∧ R a x) β†’ (βˆ€ a, a # x β†’ R a x) := by
   intro hequi h
   obtain ⟨a, ⟨hfresha, ha⟩⟩ := h
   intro b hfreshb
@@ -245,7 +241,7 @@ private lemma for_fresh_iffβ‚‚ : EquivariantRelation 𝔸 R β†’ (βˆƒ a, a # x βˆ
   rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem
   exact hmem
 
-private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by
+private lemma for_fresh_iff₃ : Equivariant 𝔸 R β†’ (βˆ€ a, a # x β†’ R a x) β†’ (И a, R a x) := by
   intro hequi h
   have hsub : {a : 𝔸 | R a x}ᢜ βŠ† NominalSet.supp 𝔸 x := by
     rw [Set.compl_subset_comm]
@@ -256,7 +252,7 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R β†’ (βˆ€ a, a # x β†
   apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub
 
 /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/
-lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by
+lemma for_fresh_iff_exists : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆƒ a, a # x ∧ R a x)) := by
   intro hequi; constructor
   Β· intro h
     apply for_fresh_iff₁ 𝔸 hequi
@@ -267,7 +263,7 @@ lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (
     exact h
 
 /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/
-lemma for_fresh_iff_all : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by
+lemma for_fresh_iff_all : Equivariant 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€ a, a # x β†’ R a x)) := by
   intro hequi; constructor
   Β· intro h
     apply for_fresh_iffβ‚‚ 𝔸 hequi
@@ -277,7 +273,7 @@ lemma for_fresh_iff_all : EquivariantRelation 𝔸 R β†’ ((И a, R a x) ↔ (βˆ€
     apply for_fresh_iff₃ 𝔸 hequi
     exact h
 
-end Equivariance
+end Rel.Equivariant
 
 end Freshness
 
@@ -293,7 +289,7 @@ structure EquivariantMap (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] where
   /-- The underlying function. -/
   toFun : X β†’ Y
   /-- Proof of equivariance. -/
-  equivariant : Equivariant 𝔸 toFun
+  equivariant : Function.Equivariant 𝔸 toFun
 
 /-- We write `X β†’β‚‘ Y` or `X β†’β‚‘[𝔸] Y` for an equivariant map X β†’ Y. -/
 infixr:25 " β†’β‚‘ " => EquivariantMap _
@@ -331,4 +327,8 @@ lemma ext {f g : X β†’β‚‘[𝔸] Y} (h : βˆ€ a, f a = g a) : f = g :=
 
 end EquivariantMap
 
+/-- Extended setoid definition that also requires the relation to be equivariant. -/
+class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where
+  equivariant : Rel.Equivariant 𝔸 r
+
 end BundledFunction
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 943bd43..ba2fbf9 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -60,7 +60,7 @@ private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by
   use ⟨x.atom, x.body⟩
   simp [ofPair]
 
-private lemma ofPair_equivariant : Equivariant 𝔸 (ofPair 𝔸 X) := by
+private lemma ofPair_equivariant : Function.Equivariant 𝔸 (ofPair 𝔸 X) := by
   intro x Ο€
   ext <;> simp [ofPair]
 
@@ -69,7 +69,7 @@ instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) :=
 
 @[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)
+    Function.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
 
@@ -105,7 +105,7 @@ private lemma alpha_eq_iff_pred {x y : NameAbstraction' 𝔸 X} : AlphaEq x y =
   apply NominalSet.for_fresh_ext
   simp [AlphaEqPred]
 
-private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred : 𝔸 β†’ NameAbstraction' 𝔸 X Γ— NameAbstraction' 𝔸 X β†’ Prop) := by
+private lemma alpha_eq_pred_equivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 β†’ NameAbstraction' 𝔸 X Γ— NameAbstraction' 𝔸 X β†’ Prop) := by
   intro a x Ο€
   rw [AlphaEqPred, AlphaEqPred]
   intro h
@@ -116,14 +116,14 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred
 private 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]
-    apply Equivariance.for_fresh_iff_exists
+    apply Rel.Equivariant.for_fresh_iff_exists
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred, @and_assoc]
 
 private 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]
-    apply Equivariance.for_fresh_iff_all
+    apply Rel.Equivariant.for_fresh_iff_all
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred]
 
@@ -202,7 +202,7 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y β†’
   · intro c ⟨hxy, hyz⟩
     rw [hxy, hyz]
 
-private lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X β†’ NameAbstraction' 𝔸 X β†’ Prop) := by
+private lemma alpha_eq_equivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X β†’ NameAbstraction' 𝔸 X β†’ Prop) := by
   intro x y Ο€ h
   rw [alpha_eq_iff_exists'] at *
   obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
@@ -377,11 +377,11 @@ private def map' (f : X β†’β‚‘[𝔸] Y) : NameAbstraction 𝔸 X β†’ NameAbstrac
     exact
       ⟨hcx.left,
        hcy.left,
-       Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right,
-       Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right,
+       Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right,
+       Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right,
        hc'⟩)
 
-private lemma map_equivariant (f : X β†’β‚‘[𝔸] Y) : Equivariant 𝔸 (map' 𝔸 f) := by
+private lemma map_equivariant (f : X β†’β‚‘[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by
   apply Quotient.ind
   intro x Ο€
   rw [← Quotient.mk_equivariant]
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2ebe9b1..d41e87f 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -140,11 +140,11 @@ instance : NominalSet 𝔸 (X Γ— Y) where
 lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
-lemma fst_equivariant : Equivariant 𝔸 (Prod.fst : X Γ— Y β†’ X) := by
-  simp [Equivariant]
+lemma fst_equivariant : Function.Equivariant 𝔸 (Prod.fst : X Γ— Y β†’ X) := by
+  simp [Function.Equivariant]
 
-lemma snd_equivariant : Equivariant 𝔸 (Prod.snd : X Γ— Y β†’ Y) := by
-  simp [Equivariant]
+lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X Γ— Y β†’ Y) := by
+  simp [Function.Equivariant]
 
 end Prod
 
@@ -212,11 +212,11 @@ instance : NominalSet 𝔸 (X βŠ• Y) where
 @[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X βŠ• Y) ↔ a # y := by
   simp [NominalSet.IsFresh]
 
-lemma inl_equivariant : Equivariant 𝔸 (Sum.inl : X β†’ X βŠ• Y) := by
-  simp [Equivariant]
+lemma inl_equivariant : Function.Equivariant 𝔸 (Sum.inl : X β†’ X βŠ• Y) := by
+  simp [Function.Equivariant]
 
-lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y β†’ X βŠ• Y) := by
-  simp [Equivariant]
+lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y β†’ X βŠ• Y) := by
+  simp [Function.Equivariant]
 
 end Sum
 
@@ -251,8 +251,8 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
     apply Quotient.ind
     simp [mul_smul]
 
-lemma mk_equivariant : Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
-  simp [Equivariant]
+lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
+  simp [Function.Equivariant]
 
 variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
 
@@ -265,7 +265,7 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a |
   Β· intro ha x' hx'
     rw [← Quotient.sound hx'] at ha
     have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') βŠ† NominalSet.supp 𝔸 x' :=
-      Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+      Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
     exact hsub ha
   Β· contrapose; intro ha
     simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall]