diff options
| -rw-r--r-- | Nominal/Category.lean | 6 | ||||
| -rw-r--r-- | Nominal/Equivariance.lean | 8 | ||||
| -rw-r--r-- | Nominal/Helpers/Finset.lean | 2 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 6 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 29 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 4 | ||||
| -rw-r--r-- | Nominal/Support.lean | 9 |
7 files changed, 40 insertions, 24 deletions
diff --git a/Nominal/Category.lean b/Nominal/Category.lean index 29a0b73..721dfb0 100644 --- a/Nominal/Category.lean +++ b/Nominal/Category.lean @@ -66,6 +66,10 @@ instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where forget₂ := { obj X := Action.ofMulAction (FPerm 𝔸) X.carrier - map f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ } + map f := ⟨f.toFun, by + intro π + ext x + simp only [EquivariantMap.toFun_eq_coe, types_comp_apply, Action.ofMulAction_apply] + apply f.equivariant⟩ } end Forget diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 368d266..50cf7c2 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -38,7 +38,7 @@ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ ∀ (x : X) ( · intro hx; exact h x π hx · intro hx apply (h (π • x) π⁻¹) at hx - simp at hx + simp only [inv_smul_smul] at hx exact hx · intro h x π hx exact (h x π).mp hx @@ -50,7 +50,7 @@ lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𝔸 R ↔ · intro hxy; exact h x y π hxy · intro hxy apply (h (π • x) (π • y) π⁻¹) at hxy - simp at hxy + simp only [inv_smul_smul] at hxy exact hxy · intro h x y π hxy exact (h x y π).mp hxy @@ -201,7 +201,7 @@ private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) intro hequi h have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸) obtain ⟨a, ha⟩ := hinf.nonempty - simp at ha + 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 @@ -220,7 +220,7 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x intro a ha rw [Set.mem_compl_iff] at ha exact h a ha - simp [NominalSet.ForFresh] + simp only [NominalSet.ForFresh] apply Set.infinite_of_finite_compl apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub diff --git a/Nominal/Helpers/Finset.lean b/Nominal/Helpers/Finset.lean index 1287c8e..9a74ffc 100644 --- a/Nominal/Helpers/Finset.lean +++ b/Nominal/Helpers/Finset.lean @@ -16,7 +16,7 @@ theorem induction · apply insert · assumption · apply h_1; assumption - · simp at h + · simp only [not_nonempty_iff_eq_empty] at h rw [h] apply single diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 891f00f..d7fade9 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -88,7 +88,7 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred rw [AlphaEqPred, AlphaEqPred] intro h have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr - simp [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' + simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' simpa [smul_smul] 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 @@ -96,14 +96,14 @@ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ rw [alpha_eq_iff_pred, this] apply Equivariance.for_fresh_iff_exists exact alpha_eq_pred_equivariant - simp only [Prod.fresh, AlphaEqPred, @and_assoc] + simp [Prod.fresh, AlphaEqPred, @and_assoc] 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 exact alpha_eq_pred_equivariant - simp only [Prod.fresh, AlphaEqPred] + simp [Prod.fresh, AlphaEqPred] 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 ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry 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 diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index a583b4c..b8d510e 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -31,7 +31,7 @@ theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := b /-- If an element does not occur in the support, the permutation doesn't move it. -/ lemma supp_notin {π : Equiv.Perm X} {x : X} : x ∉ π.supp → π x = x := by - rw [show (π x = x) ↔ ¬(π x ≠ x) by simp] + rw [show (π x = x) ↔ ¬(π x ≠ x) by simp only [ne_eq, not_not]] simp [← (mem_supp π x).not] /-- The support of the identity function is the empty set. -/ @@ -46,7 +46,7 @@ lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/ lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by - simp [supp] + simp only [supp, coe_mul, Function.comp_apply, ne_eq] apply set_support_mul_subset end Equiv.Perm diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 89021a0..430aa8c 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -62,7 +62,8 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite -- First we obtain an injection m : S \ T → (π'.supp ∪ S ∪ T)ᶜ. have h_cod_inf : ((π'.supp ∪ S ∪ T)ᶜ).Infinite := by apply Set.Finite.infinite_compl - simp; exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩ + simp only [Set.finite_union] + exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩ have h_dom_fin : (S \ T).Finite := Set.Finite.diff h_S_finite @@ -308,7 +309,7 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ PermSet.fix' 𝔸 x := by intro ha hb suffices ⸨a, b⸩ • x = (1 : FPerm 𝔸) • x by - simp only [one_smul, PermSet.fix', Set.mem_setOf_eq] at *; assumption + simp [one_smul, PermSet.fix'] at *; assumption apply PermSet.support_permutations_eq · exact supp_is_support 𝔸 · intro c hc @@ -316,13 +317,13 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by - simp [NominalSet.ForFresh]; intro h + simp only [ForFresh]; intro h exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by intro h - simp [NominalSet.ForFresh] + simp only [ForFresh, eq_iff_iff] suffices {a | P a} = {a | Q a} by rw [this] exact Set.ext h |