diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:19:45 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:20:20 +0200 |
| commit | 10edba2c0365a6858a74da22042c98f9d5fa1acc (patch) | |
| tree | e8d1b29734b02cf654d91f6b33921915e108b296 /Nominal/Instances/Abstraction.lean | |
| parent | c3700706466cb8fb9ed287ea066b656caacdc9c7 (diff) | |
simplify FPerm computations
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 20 |
1 files changed, 7 insertions, 13 deletions
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 |