diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 84 | ||||
| -rw-r--r-- | Nominal/Support.lean | 2 |
2 files changed, 47 insertions, 39 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 19b8566..82fd683 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -58,7 +58,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅. -/ section Discrete -def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where +def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where smul π x := x one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl @@ -69,21 +69,21 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where · intro π hπ; simp [PermSet.fix']; rfl · exact Set.finite_empty -@[simp] lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by +@[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by rw [← Set.subset_empty_iff] apply Set.sInter_subset_of_mem constructor - · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete] + · intro π hπ; simp [PermSet.fix', is_discrete] · exact Set.finite_empty -@[simp] lemma NominalSet.fresh_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {a : 𝔸} {x : X} : a # x := by +@[simp] lemma NominalSet.Discrete.fresh {X : Type} [NominalSet.Discrete 𝔸 X] {a : 𝔸} {x : X} : a # x := by simp [IsFresh] /-- We consider Unit a discrete nominal set. -/ -instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit +instance : NominalSet.Discrete 𝔸 Unit := NominalSet.discrete 𝔸 Unit /-- We consider Bool a discrete nominal set. -/ -instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool +instance : NominalSet.Discrete 𝔸 Bool := NominalSet.discrete 𝔸 Bool end Discrete @@ -94,25 +94,27 @@ Pairs of two nominal sets also form a nominal set, where supp (x, y) = supp x -/ section Products +namespace Prod + instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] -private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by +private lemma supp' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y) := by intro π hπ obtain ⟨hπ₁, hπ₂⟩ := PermSet.fix_union 𝔸 hπ - exact Prod.mk_inj.mpr ⟨supp_is_support 𝔸 hπ₁, supp_is_support 𝔸 hπ₂⟩ + exact Prod.mk_inj.mpr ⟨NominalSet.supp_is_support 𝔸 hπ₁, NominalSet.supp_is_support 𝔸 hπ₂⟩ instance : NominalSet 𝔸 (X × Y) where fin_supp := by intro ⟨x, y⟩; use NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y - exact ⟨NominalSet.supp_product' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩ + exact ⟨supp' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩ -@[simp] lemma NominalSet.supp_product {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y := by +@[simp] lemma supp {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y := by ext b; constructor - · apply support_subset_supp - · exact supp_product' 𝔸 - · exact Set.Finite.union (supp_finite 𝔸) (supp_finite 𝔸) + · apply NominalSet.support_subset_supp + · exact supp' 𝔸 + · exact Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸) · intro hb; cases hb with | inl hx => intro S hS @@ -127,18 +129,20 @@ instance : NominalSet 𝔸 (X × Y) where suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right exact (hS.out.left hπ).out -@[simp] lemma NominalSet.fresh_product {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by - simp [IsFresh] +@[simp] lemma fresh {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by + simp [NominalSet.IsFresh] -lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by +lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by simp; apply Set.union_comm -lemma Prod.fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by +lemma fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by simp [Equivariant] -lemma Prod.snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by +lemma snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by simp [Equivariant] +end Prod + end Products /-! @@ -148,59 +152,63 @@ Sums of two nominal sets also form a nominal set, where supp (inl x) = supp x an -/ section Coproducts +namespace Sum + instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] -private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by +private lemma supp_inl' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (NominalSet.supp 𝔸 x) := by intro π hπ simp [PermSet.fix'] - exact supp_is_support 𝔸 hπ + exact NominalSet.supp_is_support 𝔸 hπ -private lemma NominalSet.supp_coproduct₂' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (supp 𝔸 y) := by +private lemma supp_inr' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (NominalSet.supp 𝔸 y) := by intro π hπ simp [PermSet.fix'] - exact supp_is_support 𝔸 hπ + exact NominalSet.supp_is_support 𝔸 hπ instance : NominalSet 𝔸 (X ⊕ Y) where fin_supp := by intro xy cases xy with - | inl x => use NominalSet.supp 𝔸 x; exact ⟨NominalSet.supp_coproduct₁' 𝔸, NominalSet.supp_finite 𝔸⟩ - | inr y => use NominalSet.supp 𝔸 y; exact ⟨NominalSet.supp_coproduct₂' 𝔸, NominalSet.supp_finite 𝔸⟩ + | inl x => use NominalSet.supp 𝔸 x; exact ⟨supp_inl' 𝔸, NominalSet.supp_finite 𝔸⟩ + | inr y => use NominalSet.supp 𝔸 y; exact ⟨supp_inr' 𝔸, NominalSet.supp_finite 𝔸⟩ -@[simp] lemma NominalSet.supp_coproduct₁ {x : X} : supp 𝔸 (.inl x : X ⊕ Y) = supp 𝔸 x := by +@[simp] lemma supp_inl {x : X} : NominalSet.supp 𝔸 (.inl x : X ⊕ Y) = NominalSet.supp 𝔸 x := by ext b; constructor - · apply support_subset_supp - · exact supp_coproduct₁' 𝔸 - · exact supp_finite 𝔸 + · apply NominalSet.support_subset_supp + · exact supp_inl' 𝔸 + · exact NominalSet.supp_finite 𝔸 · intro hb S hS suffices PermSet.HasSupport 𝔸 x S by apply hb; exact ⟨this, hS.out.right⟩ intro π hπ suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by simp [PermSet.fix'] at this; exact this exact (hS.out.left hπ).out -@[simp] lemma NominalSet.supp_coproduct₂ {y : Y} : supp 𝔸 (.inr y : X ⊕ Y) = supp 𝔸 y := by +@[simp] lemma supp_inr {y : Y} : NominalSet.supp 𝔸 (.inr y : X ⊕ Y) = NominalSet.supp 𝔸 y := by ext b; constructor - · apply support_subset_supp - · exact supp_coproduct₂' 𝔸 - · exact supp_finite 𝔸 + · apply NominalSet.support_subset_supp + · exact supp_inr' 𝔸 + · exact NominalSet.supp_finite 𝔸 · intro hb S hS suffices PermSet.HasSupport 𝔸 y S by apply hb; exact ⟨this, hS.out.right⟩ intro π hπ suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this exact (hS.out.left hπ).out -@[simp] lemma NominalSet.fresh_coproduct₁ {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by - simp [IsFresh] +@[simp] lemma fresh_inl {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by + simp [NominalSet.IsFresh] -@[simp] lemma NominalSet.fresh_coproduct₂ {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by - simp [IsFresh] +@[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by + simp [NominalSet.IsFresh] -lemma Sum.inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by +lemma inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by simp [Equivariant] -lemma Sum.inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by +lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by simp [Equivariant] +end Sum + end Coproducts diff --git a/Nominal/Support.lean b/Nominal/Support.lean index f2bf90d..460c7ae 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -186,7 +186,7 @@ class NominalSet (X : Type) extends PermSet 𝔸 X where fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite /-- A discrete nominal set where permutations do not change anything. -/ -class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X where +class NominalSet.Discrete (X : Type) extends NominalSet 𝔸 X where is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x namespace NominalSet |