diff options
| -rw-r--r-- | Nominal/Instances.lean | 46 | ||||
| -rw-r--r-- | Nominal/Support.lean | 65 |
2 files changed, 46 insertions, 65 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index 793baa4..bf1d372 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -23,34 +23,28 @@ instance : NominalSet 𝔸 𝔸 where fin_supp := by intro a use {a} - constructor - · exact NominalSet.supp_atoms' 𝔸 - · simp + exact ⟨NominalSet.supp_atoms' 𝔸, Set.finite_singleton a⟩ lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by ext b; constructor · apply support_subset_supp · apply NominalSet.supp_atoms' - · simp - · suffices : a ∈ supp 𝔸 a - · simp; intro h; rw [h]; assumption - · intro S ⟨hsuppS, hfinS⟩ - by_contra ha - obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset) - simp at hc - have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by - intro d hd - rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl] - apply Equiv.Perm.supp_notin - simp [Equiv.Perm.supp_swap, Ne.symm hc.left] - exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ - have ha₁ : ⸨a, c⸩ • a = c := by - simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] - have ha₂ : ⸨a, c⸩ • a = a := by - specialize hsuppS hfix - simpa [PermSet.fix'] - rw [ha₁] at ha₂ - exact hc.left ha₂ + · apply Set.finite_singleton + · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h] + intro S ⟨hsuppS, hfinS⟩ + by_contra ha + -- Show that we can find a fresh c with (a c) ∈ fix S + obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset ({a} ∪ hfinS.toFinset) + simp at hc + have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by + intro d hd + apply Equiv.Perm.supp_notin + simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left] + exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ + have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] + have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption + rw [h₁] at h₂ + exact hc.left h₂ end Atoms @@ -71,15 +65,13 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where use {} constructor · intro π hπ; simp [PermSet.fix']; rfl - · simp + · exact Set.finite_empty lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by rw [← Set.subset_empty_iff] apply Set.sInter_subset_of_mem constructor - · intro π hπ - simp [PermSet.fix'] - exact DiscreteNominalSet.is_discrete x π + · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete] · exact Set.finite_empty /-- We consider Unit a discrete nominal set. -/ diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 6a1d4d9..d8058e0 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -35,11 +35,7 @@ def HasSupport (x : X) (S : Set 𝔸) : Prop := /-- Alternative definition with fix 𝔸 S unfolded. -/ lemma support_iff {x : X} {S : Set 𝔸} : HasSupport 𝔸 x S ↔ ∀ (π : FPerm 𝔸), (∀ x ∈ S, π x = x) → π ∈ fix' 𝔸 x := by - constructor - · intro hsupp π hπ - exact hsupp hπ - · intro hsupp π hπ - exact hsupp π hπ + simp [HasSupport, fix, fix'] /-- If a support is a subset of another set, that set is also a support. -/ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆ T → HasSupport 𝔸 x T := by @@ -155,21 +151,15 @@ lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → · have : DecidableEq (Set 𝔸) := Classical.typeDecidableEq (Set 𝔸) apply Finset.Nonempty.induction · intro S hS - rw [show ⋂₀ ({S} : Finset (Set 𝔸)).toSet = S by simp] - apply hS - simp + rw [Finset.coe_singleton S, Set.sInter_singleton S] + apply hS S (Finset.mem_singleton.mpr rfl) · intro S C' hS hC' hsing rw [Finset.coe_insert S C', Set.sInter_insert S ↑C'] - have hother : (∀ S ∈ C', HasSupport 𝔸 x S ∧ S.Finite) := by - intro S' hS' - apply hsing - exact Finset.mem_insert_of_mem hS' - specialize hC' hother - specialize hsing S (by simp) + specialize hC' (fun S' hS' => hsing S' (Finset.mem_insert_of_mem hS')) + specialize hsing S (Finset.mem_insert_self S C') constructor - · apply support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right - · apply Set.Finite.inter_of_left - exact hsing.right + · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right + · apply Set.Finite.inter_of_left hsing.right end PermSet @@ -182,8 +172,6 @@ Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely sup -/ section NominalSet -variable (𝔸 : Type) - /-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/ class NominalSet (X : Type) extends PermSet 𝔸 X where fin_supp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite @@ -206,31 +194,32 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x apply Set.Finite.subset · exact hfinS - · grind + · apply Set.sInter_subset_of_mem + exact Set.mem_sep hsuppS hfinS + +/-- We can restrict the supp definition to subsets of a single finite support. -/ +private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite } := by + intro hsuppS hfinS + unfold supp; ext a + constructor + · intro h T hT + exact h T hT.out.right + · intro h T hT + suffices a ∈ S ∩ T by apply Set.mem_of_mem_inter_right; assumption + apply h + constructor + · exact Set.inter_subset_left + · constructor + · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right + · exact Set.Finite.inter_of_left hfinS T /-- The least finite support is itself a support. -/ lemma supp_is_support [Infinite 𝔸] {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x - have suppf : (supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite }) := by - unfold supp; ext a - constructor - · intro h T hT - apply h - exact hT.out.right - · intro h T hT - suffices : a ∈ S ∩ T - · apply Set.mem_of_mem_inter_right; assumption - · apply h - constructor - · exact Set.inter_subset_left - · constructor - · exact PermSet.support_inter 𝔸 hsuppS hfinS hT.out.left hT.out.right - · apply Set.Finite.inter_of_left; assumption - rw [suppf] + rw [supp_equiv_finite 𝔸 hsuppS hfinS] apply PermSet.support_sInter · apply Set.Finite.subset - · apply Set.Finite.powerset - exact hfinS + · exact Set.Finite.powerset hfinS · intro T hT exact hT.out.left · use S |