show properties for freshness quantifier based on equivariant relations

4 files changed, 89 insertions, 7 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 8475a21..368d266 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -195,11 +195,56 @@ namespace Equivariance
 
 variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
 
+-- We continue with a circular implication chain argument to show these equivalences.
+
+private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by
+  intro hequi h
+  have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸)
+  obtain ⟨a, ha⟩ := hinf.nonempty
+  simp at ha
+  use a; exact ha.symm
+
+private lemma for_fresh_iff₂ : EquivariantRelation 𝔸 R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by
+  intro hequi h
+  obtain ⟨a, ⟨hfresha, ha⟩⟩ := h
+  intro b hfreshb
+  have hmem := hequi a x ⸨a, b⸩ ha
+  rw [PermSet.atom_swap, Equiv.swap_apply_left] at hmem
+  rw [NominalSet.fresh_swap_fix 𝔸 hfresha hfreshb] at hmem
+  exact hmem
+
+private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x → R a x) → (И a, R a x) := by
+  intro hequi h
+  have hsub : {a : 𝔸 | R a x}ᶜ ⊆ NominalSet.supp 𝔸 x := by
+    rw [Set.compl_subset_comm]
+    intro a ha
+    rw [Set.mem_compl_iff] at ha
+    exact h a ha
+  simp [NominalSet.ForFresh]
+  apply Set.infinite_of_finite_compl
+  apply Set.Finite.subset (NominalSet.supp_finite 𝔸) hsub
+
 /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/
-lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by sorry
+lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by
+  intro hequi; constructor
+  · intro h
+    apply for_fresh_iff₁ 𝔸 hequi
+    exact h
+  · intro h
+    apply for_fresh_iff₃ 𝔸 hequi
+    apply for_fresh_iff₂ 𝔸 hequi
+    exact h
 
 /-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/
-lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by sorry
+lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by
+  intro hequi; constructor
+  · intro h
+    apply for_fresh_iff₂ 𝔸 hequi
+    apply for_fresh_iff₁ 𝔸 hequi
+    exact h
+  · intro h
+    apply for_fresh_iff₃ 𝔸 hequi
+    exact h
 
 end Equivariance
 
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 82fd683..577cff8 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -38,10 +38,8 @@ instance : NominalSet 𝔸 𝔸 where
     simp at hc
     have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
       intro d hd
-      apply Equiv.Perm.supp_notin
-      simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left]
-      exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩
-    have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl]
+      apply FPerm.swap_neq (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₂
     exact hc.left h₂
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
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