From ac2363701c3d2a03116af449ca7bc4f918fbfda7 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 24 Oct 2025 18:05:28 +0200 Subject: show properties for freshness quantifier based on equivariant relations --- Nominal/Permutations.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'Nominal/Permutations.lean') diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 1bcb00f..a583b4c 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -133,6 +133,14 @@ lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, apply ext apply Equiv.mul_swap_eq_swap_mul +/-- 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 + 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⟩ + end FPerm example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩ @@ -168,4 +176,7 @@ open Pointwise /-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/ instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where +/-- Simplification for swaps applied to an atom. -/ +@[simp] lemma PermSet.atom_swap {a b c : 𝔸} : ⸨a, b⸩ • c = (Equiv.swap a b) c := by rfl + end PermSet -- cgit v1.3.1