show properties for freshness quantifier based on equivariant relations

1 files changed, 29 insertions, 1 deletions

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 64cc371..89021a0 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -170,6 +170,24 @@ lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (
       · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right
       · apply Set.Finite.inter_of_left hsing.right
 
+/-- If two permutations π and σ are equal for all atoms in a support of x, then πx = σx. -/
+lemma support_permutations_eq {π σ : FPerm 𝔸} {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → (∀ a ∈ S, π a = σ a) → π • x = σ • x := by
+  intro hsupp heq
+  have hfix : σ⁻¹ * π  ∈ PermSet.fix 𝔸 S := by
+    intro a ha
+    calc
+      (σ⁻¹ * π) • a = σ⁻¹ (π a)        := rfl
+      _             = σ⁻¹ (σ a)        := by rw [heq a ha]
+      _             = (σ⁻¹ * σ) a      := rfl
+      _             = (1 : FPerm 𝔸) a  := by rw [inv_mul_cancel]
+      _             = a                := rfl
+  calc
+    π • x = (1 * π) • x         := rfl
+    _     = (σ * σ⁻¹ * π) • x   := by rw [mul_inv_cancel]
+    _     = (σ * (σ⁻¹ * π)) • x := rfl
+    _     = σ • ((σ⁻¹ * π) • x) := by rw [smul_smul]
+    _     = σ • x               := by rw [hsupp hfix]
+
 end PermSet
 
 end Support
@@ -286,10 +304,20 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by
   obtain ⟨a, ⟨_, ha⟩⟩ := Set.Infinite.exists_notMem_finite h_inf h_fin
   use a
 
+/-- If a and b are fresh for x, then (a b) fixes x. -/
+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
+  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)
+
 /-- 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
-  exact Set.Infinite.nonempty 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