From 2489e2d5da786d6da0bda30f092c9622cc7d3f81 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 24 Oct 2025 01:31:41 +0200
Subject: fill in some proofs

---
 Nominal/Instances/Abstraction.lean | 39 +++++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 17 deletions(-)

(limited to 'Nominal/Instances/Abstraction.lean')

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 85ce3ad..891f00f 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -36,14 +36,13 @@ attribute [ext] NameAbstraction'
 namespace NameAbstraction'
 
 instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where
-  smul π x := .mk (π x.atom) (π • x.body)
+  smul π x := .mk (π • x.atom) (π • x.body)
 
 @[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π x.atom := rfl
 
 @[simp] lemma smul_body (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).body = π • x.body := rfl
 
 instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
-  smul π x := .mk (π x.atom) (π • x.body)
   one_smul := by intro _; ext <;> simp [one_smul]
   mul_smul := by intro _ _ _; ext <;> simp [mul_smul]
 
@@ -74,31 +73,37 @@ variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X :
 def AlphaEq (x y : NameAbstraction' 𝔸 X) : Prop :=
   И c, ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body
 
-/-- Alternatively define alpha equivalence as an equivariant relation. -/
-private def AlphaEq' (c : 𝔸) (xy : NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X) : Prop :=
+/-- Alternatively define alpha equivalence as an equivariant relation.
+
+This is used to show some properties using the Equivariance.for_fresh_* lemmas about the freshness quantifier. -/
+private def AlphaEqPred (c : 𝔸) (xy : NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X) : Prop :=
   ⸨c, xy.fst.atom⸩ • xy.fst.body = ⸨c, xy.snd.atom⸩ • xy.snd.body
 
-private lemma alpha_eq_iff {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = (И c, AlphaEq' c (x, y)) := by
+private lemma alpha_eq_iff_pred {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = (И c, AlphaEqPred c (x, y)) := by
   apply NominalSet.for_fresh_ext
-  simp [AlphaEq']
+  simp [AlphaEqPred]
 
-private lemma alpha_eq_equivariant' : EquivariantRelation 𝔸 (AlphaEq' : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by
-  intro a x π h
-  sorry
+private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by
+  intro a x π
+  rw [AlphaEqPred, AlphaEqPred]
+  intro h
+  have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr
+  simp [smul_smul, FPerm.mul_swap_eq_swap_mul] at h'
+  simpa [smul_smul]
 
 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]
+  suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEqPred c (x, y)) by
+    rw [alpha_eq_iff_pred, this]
     apply Equivariance.for_fresh_iff_exists
-    exact alpha_eq_equivariant'
-  aesop
+    exact alpha_eq_pred_equivariant
+  simp only [Prod.fresh, AlphaEqPred, @and_assoc]
 
 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]
+  suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by
+    rw [alpha_eq_iff_pred, this]
     apply Equivariance.for_fresh_iff_all
-    exact alpha_eq_equivariant'
-  aesop
+    exact alpha_eq_pred_equivariant
+  simp only [Prod.fresh, AlphaEqPred]
 
 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
 
-- 
cgit v1.3.1