proof sketch for proving different AlphaEq characterizations

1 files changed, 24 insertions, 2 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 92385d7..85ce3ad 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -74,9 +74,31 @@ variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X :
 def AlphaEq (x y : NameAbstraction' 𝔸 X) : Prop :=
   И c, ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body
 
-lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry
+/-- Alternatively define alpha equivalence as an equivariant relation. -/
+private def AlphaEq' (c : 𝔸) (xy : NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X) : Prop :=
+  ⸨c, xy.fst.atom⸩ • xy.fst.body = ⸨c, xy.snd.atom⸩ • xy.snd.body
 
-lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry
+private lemma alpha_eq_iff {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = (И c, AlphaEq' c (x, y)) := by
+  apply NominalSet.for_fresh_ext
+  simp [AlphaEq']
+
+private lemma alpha_eq_equivariant' : EquivariantRelation 𝔸 (AlphaEq' : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by
+  intro a x π h
+  sorry
+
+lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
+  suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEq' c (x, y)) by
+    rw [alpha_eq_iff, this]
+    apply Equivariance.for_fresh_iff_exists
+    exact alpha_eq_equivariant'
+  aesop
+
+lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
+  suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEq' c (x, y)) by
+    rw [alpha_eq_iff, this]
+    apply Equivariance.for_fresh_iff_all
+    exact alpha_eq_equivariant'
+  aesop
 
 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 ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry