finish name abstraction proofs

4 files changed, 84 insertions, 21 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index 57c6d11..189ca66 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -215,6 +215,8 @@ variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
 
 private lemma for_fresh_iff₁ : EquivariantRelation 𝔸 R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by
   intro hequi h
+  apply Set.Finite.infinite_compl at h
+  simp at h
   have hinf : ({a | R a x} \ NominalSet.supp 𝔸 x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite 𝔸)
   obtain ⟨a, ha⟩ := hinf.nonempty
   simp only [Set.mem_diff, Set.mem_setOf_eq] at ha
@@ -237,7 +239,6 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𝔸 R → (∀ a, a # x �
     rw [Set.mem_compl_iff] at ha
     exact h a ha
   simp only [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`". -/
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 660c2ab..bb654ed 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -133,15 +133,19 @@ lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c,
 
 For ⟪a⟫ x = ⟪b⟫ y, we either have (a, x) = (b, y) or x is just (a b) y, requiring that a is not in the support of y. -/
 lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y.body ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by
-  by_cases h_eq : x.atom = y.atom
-  · constructor
-    · sorry
-    · sorry
-  · constructor
-    · rw [alpha_eq_iff_exists]
-      intro h; right
-      obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
-      constructor
+  constructor
+  · rw [alpha_eq_iff_exists]
+    intro h
+    obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
+    by_cases h_eq : x.atom = y.atom
+    · left; constructor
+      · exact h_eq
+      · calc
+          x.body = ⸨c, x.atom⸩ • ⸨c, x.atom⸩ • x.body := by rw [← mul_smul, FPerm.swap_mul_self, one_smul]
+          _      = ⸨c, x.atom⸩ • ⸨c, y.atom⸩ • y.body := by rw [hc]
+          _      = ⸨c, y.atom⸩ • ⸨c, y.atom⸩ • y.body := by rw [h_eq]
+          _      = y.body                             := by rw [← mul_smul, FPerm.swap_mul_self, one_smul]
+    · right; constructor
       · exact h_eq
       · simp at hcx
         simp at hcy
@@ -160,24 +164,63 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at
             _      = (⸨c, x.atom⸩ * ⸨c, y.atom⸩) • y.body    := by rw [mul_smul, hc]
             _      = ⸨x.atom, y.atom⸩ • ⸨c, x.atom⸩ • y.body := by rw [← mul_smul, h_swap]
             _      = ⸨x.atom, y.atom⸩ • y.body               := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom]
-    · rw [alpha_eq_iff_all]
-      intro h c ⟨hcx, hcy⟩
+  · rw [alpha_eq_iff_all]
+    intro h c ⟨hcx, hcy⟩
+    cases h with
+    | inl h =>
+      rw [h.left, h.right]
+    | inr h =>
       simp at hcx
       simp at hcy
-      simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h
       have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := by
         ext a
         by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom
-        all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq]
-      rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left]
+        all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h.left]
+      rw [h.right.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.right.left]
 
-private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry
+private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by
+  rw [alpha_eq_iff_cases]; left
+  trivial
 
-private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by sorry
+private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by
+  rw [alpha_eq_iff_cases, alpha_eq_iff_cases]
+  intro h
+  cases h with
+  | inl h =>
+    left; exact ⟨h.left.symm, h.right.symm⟩
+  | inr h =>
+    right; constructor
+    · exact h.left.symm
+    · constructor
+      · have h : ⸨x.atom, y.atom⸩ • x.atom # x.body := by
+          rw [h.right.right]
+          exact NominalSet.fresh_equivariant 𝔸 _ _ _ h.right.left
+        simp at h; exact h
+      · rw [h.right.right, ← mul_smul, FPerm.swap_comm, FPerm.swap_mul_self, one_smul]
 
-private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by sorry
+private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by
+  intro hxy hyz
+  have h : AlphaEq x y ∧ AlphaEq y z := ⟨hxy, hyz⟩
+  simp only [AlphaEq, AlphaEq, NominalSet.for_fresh_and] at h
+  apply NominalSet.for_fresh_imp
+  · exact h
+  · intro c ⟨hxy, hyz⟩
+    rw [hxy, hyz]
 
-lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by sorry
+/-- Alpha-equivalence is an equivariant relation. -/
+lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by
+  intro x y π h
+  rw [alpha_eq_iff_exists] at *
+  obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
+  use π • c
+  constructor
+  · apply NominalSet.fresh_equivariant; exact hcx
+  · constructor
+    · apply NominalSet.fresh_equivariant; exact hcy
+    · -- XXX: This is largely similar to alpha_eq_pred...
+      have h' : π • ⸨c, x.atom⸩ • x.body = π • ⸨c, y.atom⸩ • y.body := by congr
+      simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h'
+      simpa [smul_smul]
 
 end NameAbstraction
 
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 1726ed7..a2f8d56 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -138,6 +138,11 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by
   apply ext
   simp [swap]
 
+/-- Lifting of Equiv.swap_comm to finite permutations. -/
+lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by
+  apply ext
+  simp [swap, Equiv.swap_comm]
+
 /-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/
 lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by
   intro ha hb
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index d80503f..b8e6809 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -271,9 +271,9 @@ section Freshness
 
 We also write И a, P for for_fresh (fun a => P), using the cyrillic letter И.
 
-A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/
+A proposition holds for "suitably fresh" atoms iff the set of atoms that are not "suitably fresh" is finite. -/
 def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop :=
-  {a : 𝔸 | P a}.Infinite
+  {a : 𝔸 | P a}ᶜ.Finite
 
 macro "И" x:ident "," t:term : term =>
   `(NominalSet.ForFresh (fun $x => $t))
@@ -318,6 +318,8 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P
 /-- 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 only [ForFresh]; intro h
+  apply Set.Finite.infinite_compl at h
+  rw [compl_compl] at h
   exact h.nonempty
 
 /-- Extensionality lemma for the freshness quantifier. -/
@@ -327,6 +329,18 @@ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a)
   suffices {a | P a} = {a | Q a} by rw [this]
   exact Set.ext h
 
+/-- The freshness quantifier preserves implications. -/
+lemma for_fresh_imp {P Q : 𝔸 → Prop} : (И a, P a) → (∀ a, P a → Q a) → (И a, Q a) := by
+  intro hfin himp
+  apply Set.Finite.subset
+  · exact hfin
+  · simp only [Set.compl_subset_compl, Set.setOf_subset_setOf]
+    exact himp
+
+/-- The freshness quantifier commutes with conjunctions. -/
+lemma for_fresh_and {P Q : 𝔸 → Prop} : (И a, P a) ∧ (И a, Q a) ↔ (И a, P a ∧ Q a) := by
+  simp [ForFresh, Set.setOf_and, Set.compl_inter]
+
 end NominalSet
 
 end Freshness