refactor equivariant props to use type classes

1 files changed, 27 insertions, 26 deletions

diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean
index be0d77d..91f4fb8 100644
--- a/Nominal/LambdaCalculus/Terms.lean
+++ b/Nominal/LambdaCalculus/Terms.lean
@@ -34,30 +34,31 @@ inductive AlphaEq : Preterm → Preterm → Prop where
   | rename {x y : Var} {t : Preterm} : y ∉ t.fv → AlphaEq (.abs x t) (.abs y (⸨x, y⸩ • t))
 
 /-- By definition, AlphaEq is an equivariant equivalence relation. -/
-instance Preterm.setoid : EquivariantSetoid Var Preterm where
+instance Preterm.setoid : Setoid Preterm where
   r := AlphaEq
-  iseqv := ⟨fun x => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩
-  equivariant := by
-    intro t u π htu
-    induction' htu <;> all_goals expose_names
-    · exact AlphaEq.refl
-    · exact AlphaEq.symm a_ih
-    · exact AlphaEq.trans a_ih a_ih_1
-    · exact AlphaEq.cong_abs a_ih
-    · exact AlphaEq.cong_app a_ih a_ih_1
-    · simp only [Preterm.smul_abs]
-      rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul]
-      apply AlphaEq.rename
-      rw [Preterm.fv_equivariant, Set.smul_mem_smul_set_iff]
-      exact h
+  iseqv := ⟨fun _ => AlphaEq.refl, AlphaEq.symm, AlphaEq.trans⟩
+
+instance Preterm.instSetoidEquivariant : Rel.Equivariant Var setoid.r := by
+  constructor; intro t u π htu
+  induction' htu <;> all_goals expose_names
+  · exact AlphaEq.refl
+  · exact AlphaEq.symm a_ih
+  · exact AlphaEq.trans a_ih a_ih_1
+  · exact AlphaEq.cong_abs a_ih
+  · exact AlphaEq.cong_app a_ih a_ih_1
+  · simp only [Preterm.smul_abs]
+    rw [← mul_smul, FPerm.mul_swap_eq_swap_mul, mul_smul]
+    apply AlphaEq.rename
+    rw [Function.equivariant Var Preterm.fv, Set.smul_mem_smul_set_iff]
+    exact h
 
 /-- Define λ-terms as the quotient Preterm/≈. -/
-def Term := Quotient Preterm.setoid.toSetoid
+def Term := Quotient Preterm.setoid
 
 namespace Term
 
 /-- The equivalence class of a λ-preterm. -/
-abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid.toSetoid
+abbrev mk : Preterm → Term := Quotient.mk Preterm.setoid
 
 instance : NominalSet Var Term := Quotient.instNominalSet Var
 
@@ -135,7 +136,7 @@ private lemma pick_fresh {t : Preterm} : ∀ x ∉ t.fv, ∃ u, t ≈ u ∧ x �
     rw [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc
     have hc' : c ∉ (π • a_1).fv := fun h => hc.right (Preterm.fv_subset_vars _ h)
     obtain ⟨u, hu⟩ := a_ih (⸨π • a, c⸩ * π) x (by
-      rw [mul_smul, Preterm.fv_equivariant]
+      rw [mul_smul, Function.equivariant Var Preterm.fv]
       intro hcontra
       by_cases hxa : x = π • a
       · rw [hxa, ← PermSet.atom_set_swap_right] at hcontra
@@ -177,7 +178,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by
         rw [h_1]
     · obtain ⟨z, ⟨hz₁, hz₂⟩⟩ := pick_fresh y h
       apply AlphaEq'.abs
-      rw [Quotient.mk_equivariant, Quotient.sound hz₁, NameAbstraction.eq_iff_cases]
+      rw [Function.equivariant Var (Quotient.mk _), Quotient.sound hz₁, NameAbstraction.eq_iff_cases]
       by_cases hxy : x = y
       · left
         simp [hxy, FPerm.swap_self, one_smul]
@@ -187,8 +188,8 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by
         · constructor
           · rw [← Preterm.supp] at hz₂
             nth_rw 1 [show x = ⸨x, y⸩ • y by simp]
-            apply NominalSet.fresh_equivariant
-            exact Function.Equivariant.preserve_fresh Var (Quotient.mk_equivariant Var) hz₂
+            rw [← Rel.equivariant Var NominalSet.IsFresh]
+            exact Function.Equivariant.preserve_fresh Var hz₂
           · rw [← mul_smul, FPerm.swap_mul_self, one_smul]
   · intro h; cases h <;> all_goals expose_names
     · exact AlphaEq.refl
@@ -201,7 +202,7 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by
         exact h.right
       | inr h =>
         obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := Quotient.supp_pick_fresh Var h.right.left
-        rw [← Quotient.sound hs₁, ← Quotient.mk_equivariant] at h
+        rw [← Quotient.sound hs₁, ← Function.equivariant Var (Quotient.mk _)] at h
         have hrename : Preterm.abs y s ≈ Preterm.abs x (⸨y, x⸩ • s) := by
           apply AlphaEq.rename
           rw [Preterm.supp] at hs₂
@@ -241,6 +242,7 @@ lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫
   obtain ⟨u', hu'⟩ := u.exists_rep
   simp only [abs, ← ht', Quotient.lift_mk, ← hu']
   rw [Quotient.eq_iff_equiv, alpha_eq_abs]
+  rfl
 
 /-- Alternative characterization of α-equivalence for application preterms. -/
 lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by
@@ -293,7 +295,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
       (by
         intro t u htu
         rw [alpha_eq, alpha_eq_iff] at htu
-        cases htu <;> simp [*])
+        cases htu <;> simp only [Sum.inr.injEq, Sum.inl.injEq, *]; assumption)
     invFun
       | .inl x => .var x
       | .inr (.inl x) => Quotient.liftOn x
@@ -323,7 +325,7 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term
           simp only [app, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq]
           rw [hx', hy']
     toFun_equivariant := by
-      intro t π
+      constructor; intro t π
       obtain ⟨t', ht'⟩ := t.exists_rep
       rw [← ht']
       cases t' <;> all_goals rfl
@@ -357,8 +359,7 @@ def fv : Term → Set Var := Quotient.lift Preterm.fv (by
   simp [← ht', ← hu', Preterm.fv]
 
 /-- The lifted fv function is also equivariant.-/
-lemma fv_equivariant : Function.Equivariant Var fv :=
-  Quotient.lift_equivariant Var _ _ Preterm.fv_equivariant
+instance instFvEquivariant : Function.Equivariant Var fv := Quotient.lift_equivariant Var _ _
 
 /-- The support of a term consists exactly of the free variables in it. -/
 lemma supp : NominalSet.supp Var = fv := by