more wip

2 files changed, 102 insertions, 14 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index b4a6cee..76cb360 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -243,31 +243,84 @@ instance NameAbstraction.setoid : EquivariantSetoid 𝔸 (NameAbstraction' 𝔸
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
 def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X).toSetoid
 
+namespace NameAbstraction
+
 /-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
-def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
+def mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
   Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x)
 
 /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
-notation "⟪" a "⟫ " t => NameAbstraction.mk a t
+notation "⟪" a "⟫ " t => mk a t
 
 instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
 
 @[simp]
-lemma NameAbstraction.smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr
+lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr
+
+/-- Two name abstractions are equal iff they are alpha-equivalent. -/
+lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by
+  rw [mk, mk, Quotient.eq_iff_equiv]
+  rfl
+
+/-- Lifting of alpha_eq_iff_exists to name abstractions. -/
+lemma eq_iff_exists {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by
+  simp only [eq_iff_alpha_eq, alpha_eq_iff_exists, NameAbstraction'.fresh, ne_eq]
+  ac_nf
+
+/-- Lifting of alpha_eq_iff_exists to name abstractions. -/
+lemma eq_iff_all  {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by
+  simp only [eq_iff_alpha_eq, alpha_eq_iff_all, NameAbstraction'.fresh, ne_eq]
+  ac_nf
+
+/-- Lifting of alpha_eq_iff_cases to name abstractions. -/
+lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by
+  simp [eq_iff_alpha_eq, alpha_eq_iff_cases]
 
 @[simp]
-lemma NameAbstraction.supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by
-  sorry
-  -- ext b; constructor
-  -- · apply NominalSet.support_subset_supp 𝔸
-  --   · intro π hπ
-  --     simp [PermSet.fix']
+lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by
+  have hswap : ∀ (b : 𝔸) (y : X), (⟪a⟫ x) = (⟪b⟫ y) → NominalSet.supp 𝔸 (⟨b, y⟩ : NameAbstraction' 𝔸 X) = {b} ∪ (NominalSet.supp 𝔸 x \ {a}) := by
+    intro b y heq
+    rw [eq_iff_cases] at heq
+    cases heq with
+    | inl h =>
+      rw [h.left, h.right]
+      simp only [NameAbstraction'.supp, Set.union_singleton, Set.union_diff_self, Set.singleton_union]
+    | inr h =>
+      simp only [NameAbstraction'.supp, Set.union_comm]
+      rw [h.right.right, NominalSet.supp_equivariant 𝔸 y ⸨a, b⸩]
+      ext c
+      by_cases h₁ : c = b
+      · simp [h₁]
+      · by_cases h₂ : c = a
+        · simp [h₂, show a ∉ NominalSet.supp 𝔸 y by exact h.right.left]
+        · simp [h₁, h₂, ← PermSet.atom_set_swap_ne_ne]
+  rw [mk, Quotient.supp]
+  ext b
+  constructor
+  · contrapose; intro h
+    simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, Classical.not_imp, not_forall, not_or]
+    have hfin : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸
+    obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin.toFinset ∪ {a, b})
+    simp only [Finset.union_insert, Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc
+    use ⟨c, ⸨a, c⸩ • x⟩
+    constructor
+    · apply Quotient.exact
+      rw [← mk, ← mk, eq_iff_cases]
+      right
+      exact ⟨hc.left, hc.right.right, by rw [FPerm.swap_comm]⟩
+    · constructor
+      · exact Ne.symm hc.right.left
+      · simp
+        sorry
+  · intro h x' hx'
+    suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by
+      rw [this]
+      exact Set.mem_union_right {x'.atom} h
+    apply hswap
+    apply Quotient.sound
+    exact (Setoid.symm hx')
 
-  --     sorry
-  --   · exact Set.Finite.diff (NominalSet.supp_finite 𝔸)
-  -- · rw [mk, Quotient.supp]
-  --   intro hb x' hx'
-  --   sorry
+end NameAbstraction
 
 end Quotient
 
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 0d6b81c..bc775b9 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -202,4 +202,39 @@ 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
 
+/-- Given x = (a b) y, we also know y = (a b) x. -/
+lemma PermSet.swap_switch {X : Type} [PermSet 𝔸 X] {a b : 𝔸} {x y : X} : x = ⸨a, b⸩ • y → y = ⸨a, b⸩ • x := by
+  intro h
+  have h' : ⸨a, b⸩ • x = ⸨a, b⸩ • ⸨a, b⸩ • y := by congr
+  rw [← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+  exact h'.symm
+
+/-- If the element is not affected by the swap, membership of it is the same as before the swap. -/
+lemma PermSet.atom_set_swap_ne_ne {a b c : 𝔸} {S : Set 𝔸} : c ≠ a → c ≠ b → (c ∈ S ↔ c ∈ ⸨a, b⸩ • S) := by
+  intro ha hb
+  constructor
+  · intro h
+    rw [← FPerm.swap_apply_of_ne_of_ne ha hb]
+    exact Set.smul_mem_smul_set h
+  · intro h
+    have h' : ⸨a, b⸩ c ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_of_ne_of_ne ha hb, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+    exact h'
+
+/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
+lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ ⸨a, b⸩ • S := by
+  constructor
+  · intro h
+    have h' : ⸨a, b⸩ a ∈ ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_left] at h'
+    exact h'
+  · intro h
+    have h' : ⸨a, b⸩ b ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
+    rw [FPerm.swap_apply_right, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
+    exact h'
+
+/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
+lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by
+  rw [FPerm.swap_comm, atom_set_swap_left]
+
 end PermSet