diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 20 | ||||
| -rw-r--r-- | Nominal/Instances/Basic.lean | 2 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 19 | ||||
| -rw-r--r-- | Nominal/Support.lean | 2 |
4 files changed, 22 insertions, 21 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 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₂ diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 62d7470..1726ed7 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -138,13 +138,20 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by apply ext simp [swap] -/-- If c is not equal to a or b, then (a b) leaves c unchanged. -/ -lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by +/-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/ +lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by intro ha hb - apply Equiv.Perm.supp_notin - simp only [swap, Equiv.Perm.supp_swap, ne_eq, ite_not, Set.mem_ite_empty_left, Set.mem_insert_iff, Set.mem_singleton_iff, not_and, not_or] - intro _ - exact ⟨ha, hb⟩ + simp [swap, Equiv.swap_apply_of_ne_of_ne, ha, hb] + +/-- Lifting of Equiv.swap_apply_left to finite permutations. -/ +@[simp] +lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by + simp [swap] + +/-- Lifting of Equiv.swap_apply_right to finite permutations. -/ +@[simp] +lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by + simp [swap] end FPerm diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 430aa8c..d80503f 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -313,7 +313,7 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P apply PermSet.support_permutations_eq · exact supp_is_support 𝔸 · intro c hc - apply FPerm.swap_neq (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) + apply FPerm.swap_apply_of_ne_of_ne (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) /-- 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 |