proof sketch for proving different AlphaEq characterizations

3 files changed, 54 insertions, 4 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index ac50519..8475a21 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -185,6 +185,27 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
 end Nominal
 
 /-!
+## Freshness
+
+For propositions of the form `И a, a R x`, where `R` is an equivariant relation, we do not have to differentiate between "for any fresh a" and "for all fresh a".
+-/
+section Freshness
+
+namespace Equivariance
+
+variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
+
+/-- 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
+
+/-- 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
+
+end Equivariance
+
+end Freshness
+
+/-!
 ## Bundled Functions
 
 In the following, we also define a bundled function type for equivariant functions.
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
 
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 460c7ae..64cc371 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -253,7 +253,7 @@ 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. -/
-@[simp] def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop :=
+def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop :=
   {a : 𝔸 | P a}.Infinite
 
 macro "И" x:ident "," t:term : term =>
@@ -288,9 +288,16 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by
 
 /-- 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; intro h
+  simp [NominalSet.ForFresh]; intro h
   exact Set.Infinite.nonempty h
 
+/-- 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
+  intro h
+  simp [NominalSet.ForFresh]
+  suffices {a | P a} = {a | Q a} by rw [this]
+  exact Set.ext h
+
 end NominalSet
 
 end Freshness