fill in some proofs

2 files changed, 32 insertions, 17 deletions

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
 
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 4a3e88f..1bcb00f 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -116,6 +116,11 @@ end Equiv.Perm
 
 namespace FPerm
 
+/-- Extensionality lemma for finite permutations. -/
+lemma ext {X : Type} {π₁ π₂ : FPerm X} : π₁.val = π₂.val → π₁ = π₂ := by
+  intro h; ext; rw [h]
+
+/-- Transpositions are finite permutations. -/
 def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
   apply Set.Finite.subset
   · apply ({x, y} : Finset X).finite_toSet
@@ -123,6 +128,11 @@ def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
 
 notation "⸨" a "," b "⸩" => FPerm.swap a b
 
+/-- Lifting of Equiv.mul_swap_eq_swap_mul to finite permutations. -/
+lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, π b⸩ * π := by
+  apply ext
+  apply Equiv.mul_swap_eq_swap_mul
+
 end FPerm
 
 example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩