From 5dde77b6db9fc78094363f91e0c6643a84be513e Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 29 Oct 2025 00:40:13 +0100 Subject: refactor equivariance namespaces --- Nominal/Equivariance.lean | 60 +++++++++++++++++++------------------- Nominal/Instances/Abstraction.lean | 18 ++++++------ Nominal/Instances/Basic.lean | 22 +++++++------- 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] -- cgit v1.3.1