From 10edba2c0365a6858a74da22042c98f9d5fa1acc Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 26 Oct 2025 01:19:45 +0200 Subject: simplify FPerm computations --- Nominal/Instances/Abstraction.lean | 20 +++++++------------- Nominal/Instances/Basic.lean | 2 +- 2 files changed, 8 insertions(+), 14 deletions(-) (limited to 'Nominal/Instances') diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 508167e..660c2ab 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -147,19 +147,10 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at 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 - -- TODO: Refactor into lemma have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by ext a - simp [FPerm.swap] - by_cases h₁ : (a = c) <;> by_cases h₂ : (a = x.atom) <;> by_cases h₃ : (a = y.atom) - · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] - · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] - · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] - · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] - · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left] - · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left] - · simp [h₃, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] - · simp [Equiv.swap_apply_of_ne_of_ne h₁ h₃, Equiv.swap_apply_of_ne_of_ne h₁ h₂, Equiv.swap_apply_of_ne_of_ne h₂ h₃] + by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom + all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq] rw [mul_smul, PermSet.atom_swap, PermSet.atom_swap, Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq] at h_atom rw [mul_smul, hc, ← mul_smul, FPerm.swap_mul_self, one_smul] at h_atom constructor @@ -171,10 +162,13 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at _ = ⸨x.atom, y.atom⸩ • y.body := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom] · rw [alpha_eq_iff_all] intro h c ⟨hcx, hcy⟩ + simp at hcx simp at hcy simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h - -- TODO: Use new lemma from before - have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := sorry + have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := by + ext a + by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom + all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq] rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left] private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 2786c86..2bb389d 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -41,7 +41,7 @@ instance : NominalSet 𝔸 𝔸 where 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) + apply FPerm.swap_apply_of_ne_of_ne (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right) have h₁ : ⸨a, c⸩ • a = c := by rw [PermSet.atom_swap, Equiv.swap_apply_left] have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption rw [h₁] at h₂ -- cgit v1.3.1