diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 29 |
1 files changed, 20 insertions, 9 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 577cff8..2786c86 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -30,12 +30,15 @@ instance : NominalSet 𝔸 𝔸 where · apply support_subset_supp 𝔸 · exact NominalSet.supp_atom' 𝔸 · exact Set.finite_singleton a - · suffices a ∈ supp 𝔸 a by simp; intro h; rwa [h] + · suffices a ∈ supp 𝔸 a by + simp only [Set.mem_singleton_iff] + 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 + simp only [Finset.singleton_union, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by intro d hd apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right) @@ -64,7 +67,7 @@ def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where fin_supp := by intro x; use {} constructor - · intro π hπ; simp [PermSet.fix']; rfl + · intro π hπ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl · exact Set.finite_empty @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by @@ -118,13 +121,17 @@ instance : NominalSet 𝔸 (X × Y) where intro S hS suffices PermSet.HasSupport 𝔸 x S by apply hx; exact ⟨this, hS.out.right⟩ intro π hπ - suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.left + suffices π ∈ PermSet.fix' 𝔸 (x, y) by + simp only [PermSet.fix', smul_mk, mk.injEq, Set.mem_setOf_eq] at this + exact this.left exact (hS.out.left hπ).out | inr hy => intro S hS suffices PermSet.HasSupport 𝔸 y S by apply hy; exact ⟨this, hS.out.right⟩ intro π hπ - suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right + suffices π ∈ PermSet.fix' 𝔸 (x, y) by + simp only [PermSet.fix', smul_mk, mk.injEq, Set.mem_setOf_eq] at this + exact this.right exact (hS.out.left hπ).out @[simp] lemma fresh {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by @@ -158,12 +165,12 @@ variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] private lemma supp_inl' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (NominalSet.supp 𝔸 x) := by intro π hπ - simp [PermSet.fix'] + simp only [PermSet.fix', smul_inl, inl.injEq, Set.mem_setOf_eq] exact NominalSet.supp_is_support 𝔸 hπ private lemma supp_inr' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (NominalSet.supp 𝔸 y) := by intro π hπ - simp [PermSet.fix'] + simp only [PermSet.fix', smul_inr, inr.injEq, Set.mem_setOf_eq] exact NominalSet.supp_is_support 𝔸 hπ instance : NominalSet 𝔸 (X ⊕ Y) where @@ -181,7 +188,9 @@ instance : NominalSet 𝔸 (X ⊕ Y) where · 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 + suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by + simp only [PermSet.fix', smul_inl, inl.injEq, Set.mem_setOf_eq] at this + exact this exact (hS.out.left hπ).out @[simp] lemma supp_inr {y : Y} : NominalSet.supp 𝔸 (.inr y : X ⊕ Y) = NominalSet.supp 𝔸 y := by @@ -192,7 +201,9 @@ instance : NominalSet 𝔸 (X ⊕ Y) where · 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 + suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by + simp only [PermSet.fix', smul_inr, inr.injEq, Set.mem_setOf_eq] at this + exact this exact (hS.out.left hπ).out @[simp] lemma fresh_inl {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by |