finish name abstraction supp proof

1 files changed, 30 insertions, 24 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 76cb360..269e80f 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -278,6 +278,7 @@ lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b
 
 @[simp]
 lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by
+  -- XXX: This is rather ugly...
   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
@@ -297,21 +298,32 @@ lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.su
   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
+  · by_cases h_eq : a = b
+    · contrapose; intro h
+      subst h_eq
+      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})
+      simp only [Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc
+      use ⟨c, ⸨a, c⸩ • x⟩
+      have haeq : (⟪c⟫ ⸨a, c⸩ • x) = (⟪a⟫ x) := by
+        rw [eq_iff_cases]
+        right
+        exact ⟨hc.left, hc.right, by rw [FPerm.swap_comm]⟩
+      constructor
+      · exact Quotient.exact haeq
+      · constructor
+        · exact Ne.symm hc.left
+        · suffices a ∉ NominalSet.supp 𝔸 (⟨c, ⸨a, c⸩ • x⟩ : NameAbstraction' 𝔸 X) by
+            simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, not_or] at this
+            exact this.right
+          rw [hswap c (⸨a, c⸩ • x) haeq.symm]
+          simp [Ne.symm hc.left]
+    · intro h
+      specialize h ⟨a, x⟩ (by rfl)
+      simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Ne.symm h_eq, false_or] at h
+      rw [Set.mem_diff_singleton]
+      exact ⟨h, Ne.symm h_eq⟩
   · intro h x' hx'
     suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by
       rw [this]
@@ -320,20 +332,14 @@ lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.su
     apply Quotient.sound
     exact (Setoid.symm hx')
 
+@[simp] lemma fresh {a b : 𝔸} {x : X} : b # (⟪a⟫ x) ↔ b # x ∨ b = a := by
+  simp only [NominalSet.IsFresh, supp, Set.mem_diff, Set.mem_singleton_iff, not_and_or, Decidable.not_not]
+
 end NameAbstraction
 
 end Quotient
 
 /-!
-## Nominal Set Instance
-
-The equivalence classes of name abstractions form a nominal set where supp (⟪a⟫ x) = supp x \ {a}.
--/
-section NominalSet
-
-end NominalSet
-
-/-!
 ## Abstraction Functor
 
 Name abstraction can also be considered as a functor `Nom → Nom`.