From 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 3 Dec 2025 20:34:41 +0100 Subject: refactor equivariant props to use type classes --- Nominal/Instances/Abstraction.lean | 63 ++++++++++----------- Nominal/Instances/Basic.lean | 111 +++++++++++++++++++++++++++---------- 2 files changed, 114 insertions(+), 60 deletions(-) (limited to 'Nominal/Instances') diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 69e29f2..e03d67a 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -49,11 +49,11 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where private def equiv : EquivariantEquiv 𝔸 (NameAbstraction' 𝔸 X) (𝔸 × X) := { toFun x := ⟨x.atom, x.body⟩ invFun x := ⟨x.fst, x.snd⟩ - toFun_equivariant := by intro x π; ext <;> simp + toFun_equivariant := by constructor; intro x π; ext <;> simp } instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) := - NominalSet.fromEquivariantEquiv 𝔸 (equiv 𝔸 X) + NominalSet.ofEquivariantEquiv 𝔸 (equiv 𝔸 X) @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by have h : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 (x.atom, x.body) := @@ -93,8 +93,8 @@ 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 : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by - intro a x π +private instance instAlphaEqPredEquivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by + constructor; intro a x π rw [AlphaEqPred, AlphaEqPred] intro h have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr @@ -105,14 +105,12 @@ private lemma alpha_eq_iff_exists' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y 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 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 Rel.Equivariant.for_fresh_iff_all - exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred] private 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 @@ -132,8 +130,9 @@ private lemma alpha_eq_iff_cases' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y · 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 + have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body := by + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact hcx.right have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by ext a by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom @@ -176,8 +175,8 @@ private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → Al · exact h.left.symm · constructor · have h : ⸨x.atom, y.atom⸩ • x.atom # x.body := by - rw [h.right.right] - exact NominalSet.fresh_equivariant 𝔸 _ _ _ h.right.left + rw [h.right.right, ← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact h.right.left simp at h; exact h · rw [h.right.right, ← mul_smul, FPerm.swap_comm, FPerm.swap_mul_self, one_smul] @@ -190,15 +189,15 @@ 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 : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by - intro x y π h +private instance instAlphaEqEquivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by + constructor; intro x y π h rw [alpha_eq_iff_exists'] at * obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h use π • c constructor - · apply NominalSet.fresh_equivariant; exact hcx + · rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]; exact hcx · constructor - · apply NominalSet.fresh_equivariant; exact hcy + · rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]; exact hcy · -- XXX: This is largely similar to alpha_eq_pred... have h' : π • ⸨c, x.atom⸩ • x.body = π • ⸨c, y.atom⸩ • y.body := by congr simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' @@ -218,19 +217,21 @@ section Quotient variable (X : Type) [NominalSet 𝔸 X] /-- Associate the name abstraction structure with alpha-equivalence. -/ -instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸 X) where +instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where r := AlphaEq iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩ - equivariant := alpha_eq_equivariant + +instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸 X) := + instAlphaEqEquivariant /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/ -def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid +def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X) namespace NameAbstraction /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/ abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X := - Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x) + Quotient.mk (setoid 𝔸 X) (.mk a x) /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ notation "⟪" a "⟫ " x:60 => mk a x @@ -283,7 +284,7 @@ private lemma raw_supp_swap {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y → N 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⸩] + rw [h.right.right, Function.equivariant 𝔸 (NominalSet.supp 𝔸)] ext c by_cases h₁ : c = b · simp [h₁] @@ -350,7 +351,7 @@ namespace NameAbstraction variable {X Y Z : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [NominalSet 𝔸 Z] private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstraction 𝔸 Y := - Quotient.lift (fun x => ⟪x.atom⟫ f x.body) (by + Quotient.lift (fun x => ⟪x.atom⟫ f.toFun x.body) (by intro x y hxy rw [alpha_eq_iff_exists] at hxy obtain ⟨c, ⟨hcx, hcy, hc⟩⟩ := hxy @@ -358,28 +359,28 @@ private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstrac rw [NameAbstraction'.fresh] at hcy rw [eq_iff_exists] use c - have hc' : ⸨c,x.atom⸩ • f x.body = ⸨c,y.atom⸩ • f y.body := by - rw [show f x.body = f.toFun x.body from rfl, ← f.equivariant] - rw [show f y.body = f.toFun y.body from rfl, ← f.equivariant] + have hc' : ⸨c,x.atom⸩ • f.toFun x.body = ⸨c,y.atom⸩ • f.toFun y.body := by + rw [← Function.equivariant 𝔸 f.toFun] + rw [← Function.equivariant 𝔸 f.toFun] congr exact ⟨hcx.left, hcy.left, - Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right, - Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right, + Function.Equivariant.preserve_fresh 𝔸 hcx.right, + Function.Equivariant.preserve_fresh 𝔸 hcy.right, hc'⟩) -private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by +private instance instMapEquivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by + constructor apply Quotient.ind intro x π - rw [← Quotient.mk_equivariant] + rw [← Function.equivariant 𝔸 (Quotient.mk _)] simp only [map', Quotient.lift_mk, NameAbstraction'.smul_atom, NameAbstraction'.smul_body, smul] - rw [show f (π • x.body) = f.toFun (π • x.body) from rfl, f.equivariant] - rfl + rw [← Function.equivariant 𝔸 f.toFun] /-- Lifts an equivariant function to name abstractions. -/ def map (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X →ₑ[𝔸] NameAbstraction 𝔸 Y := - ⟨map' 𝔸 f, map_equivariant 𝔸 f⟩ + ⟨map' 𝔸 f, instMapEquivariant 𝔸 f⟩ /-- Application of equivariant functions lifted to name abstractions. -/ @[simp] @@ -400,7 +401,7 @@ private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 /-- Name abstractions form a functor `Nom ⥤ Nom`. -/ def Functor : Nom 𝔸 ⥤ Nom 𝔸 := { obj X := ⟨NameAbstraction 𝔸 X⟩ - map f := ⟨NameAbstraction.map 𝔸 f, NameAbstraction.map_equivariant 𝔸 f⟩ + map f := ⟨NameAbstraction.map 𝔸 f, NameAbstraction.instMapEquivariant 𝔸 f⟩ map_id := fun _ => map_id 𝔸 map_comp f g := map_comp 𝔸 g f } diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 7f461ac..dcca75b 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 : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by - simp [Function.Equivariant] +instance instFstEquivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by + constructor; simp -lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by - simp [Function.Equivariant] +instance instSndEquivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by + constructor; simp 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 : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by - simp [Function.Equivariant] +instance instInlEquivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by + constructor; simp -lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by - simp [Function.Equivariant] +instance instInrEquivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by + constructor; simp end Sum @@ -231,17 +231,18 @@ section Quotient namespace Quotient -variable {X : Type} [PermSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} +variable {X : Type} [PermSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r] -instance : SMul (FPerm 𝔸) (Quotient setoid.toSetoid) where +instance : SMul (FPerm 𝔸) (Quotient setoid) where smul π := Quotient.lift (fun x => ⟦π • x⟧) (by intro x y hxy simp only [Quotient.eq] - apply setoid.equivariant x y π hxy) + rw [← Rel.equivariant 𝔸 setoid.r] + exact hxy) -@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid.toSetoid x) = ⟦π • x⟧ := rfl +@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid x) = ⟦π • x⟧ := rfl -instance : PermSet 𝔸 (Quotient setoid.toSetoid) where +instance : PermSet 𝔸 (Quotient setoid) where one_smul := by apply Quotient.ind intro x @@ -251,32 +252,33 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where apply Quotient.ind simp [mul_smul] -lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by - simp [Function.Equivariant] +instance instMkEquivariant : Function.Equivariant 𝔸 (Quotient.mk setoid) := by + constructor; simp -lemma lift_equivariant - {Y : Type} [PermSet 𝔸 Y] (f : X → Y) (h : ∀ (a b : X), a ≈ b → f a = f b) : - Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 (Quotient.lift f h) := by - intro hequi x π +def lift_equivariant + {Y : Type} [PermSet 𝔸 Y] (f : X → Y) [Function.Equivariant 𝔸 f] + (h : ∀ (a b : X), a ≈ b → f a = f b) : + Function.Equivariant 𝔸 (Quotient.lift f h) := by + constructor; intro x π obtain ⟨x', hx'⟩ := x.exists_rep - simp [← hx', hequi x' π] + simp [← hx', Function.equivariant 𝔸 f] -variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} +variable {X : Type} [NominalSet 𝔸 X] {setoid : Setoid X} [Rel.Equivariant 𝔸 setoid.r] -instance : NominalSet 𝔸 (Quotient setoid.toSetoid) := - NominalSet.fromEquivariantSurjective 𝔸 (Quotient.mk setoid.toSetoid) (mk_equivariant 𝔸) mk_surjective +instance : NominalSet 𝔸 (Quotient setoid) := + NominalSet.ofEquivariantSurjective 𝔸 (Quotient.mk setoid) mk_surjective -lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by +lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by ext a constructor · intro ha x' hx' rw [← Quotient.sound hx'] at ha - have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' := - Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸) + have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid x') ⊆ NominalSet.supp 𝔸 x' := + Function.Equivariant.supp_subset 𝔸 exact hsub ha · contrapose; intro ha simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall] - have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x)).Finite := NominalSet.supp_finite 𝔸 + have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid x)).Finite := NominalSet.supp_finite 𝔸 have hfin₂ : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸 -- Show that we can find a fresh c for which (a c) • ⟦x⟧ = ⟦x⟧ obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin₁.toFinset ∪ hfin₂.toFinset) @@ -285,15 +287,66 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | · apply Quotient.exact rw [← smul_quotient] exact NominalSet.fresh_swap_fix 𝔸 ha hc.left - · rw [NominalSet.supp_equivariant, Set.mem_smul_set_iff_inv_smul_mem] + · rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸), Set.mem_smul_set_iff_inv_smul_mem] simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] exact hc.right /-- If an atom is not in the support of the equivalence class, one can always pick a representative where it is not in the least support. -/ -lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by +lemma supp_pick_fresh {a : 𝔸} {x : X} : a ∉ NominalSet.supp 𝔸 (Quotient.mk setoid x) → ∃ (y : X), y ≈ x ∧ a ∉ NominalSet.supp 𝔸 y := by contrapose simp [not_exists, not_and, not_not, supp] end Quotient end Quotient + +/-! +## Subtypes + +If X is a nominal set, Y is a subtype of X, and π • x ∈ Y for all π ∈ FPerm 𝔸 and x ∈ X, then Y is +also a nominal set. +-/ +section Subtype + +namespace Subtype + +variable {X : Type} [PermSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S] + +instance : PermSet 𝔸 S where + smul π x := ⟨π • x.val, by + rw [← Set.equivariant 𝔸 S] + exact x.prop⟩ + one_smul x := by + apply Subtype.eq + exact MulAction.one_smul x.val + mul_smul π τ x := by + apply Subtype.eq + exact MulAction.mul_smul π τ x.val + +@[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl + +instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : S → X) := by + constructor; simp + +variable {X : Type} [NominalSet 𝔸 X] {S : Set X} [Set.Equivariant 𝔸 S] + +instance : NominalSet 𝔸 S where + fin_supp x := by + use NominalSet.supp 𝔸 x.val + constructor + · intro π hπ + apply Subtype.eq + exact NominalSet.supp_is_support 𝔸 hπ + · exact NominalSet.supp_finite 𝔸 + +@[simp] lemma supp {x : S} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.val := by + symm + apply Function.Equivariant.supp_eq_if_inj + exact val_injective + +@[simp] lemma fresh {a : 𝔸} {x : S} : a # x ↔ a # x.val := by + simp [NominalSet.IsFresh] + +end Subtype + +end Subtype -- cgit v1.3.1