refactor equivariant props to use type classes

1 files changed, 101 insertions, 5 deletions

diff --git a/Algebra/Term.lean b/Algebra/Term.lean
index 20fd009..665999f 100644
--- a/Algebra/Term.lean
+++ b/Algebra/Term.lean
@@ -80,7 +80,7 @@ def Substitution.apply {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermA
       apply ih1; exact h arg⟩
 
 private def rename' (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig X
-  | .var x => .var x
+  | .var x => .var (π • x)
   | .pure f args => .pure f (fun x => rename' π (args x))
   | .free a f args => .free (π • a) f (fun x => rename' π (args x))
   | .bound a f args => .bound (π • a) f (fun x => rename' π (args x))
@@ -97,6 +97,100 @@ instance : PermSet 𝔸 (Term 𝔸 sig X) where
   one_smul := one_rename 𝔸
   mul_smul := mul_rename 𝔸
 
+@[simp] lemma smul_var {π : FPerm 𝔸} {x : X} :
+    π • (Term.var x : Term 𝔸 sig X) = Term.var (π • x) := rfl
+
+@[simp] lemma smul_pure {π : FPerm 𝔸} {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} :
+    π • Term.pure f args = Term.pure f ((π • ·) ∘ args) := rfl
+
+@[simp] lemma smul_free {π : FPerm 𝔸} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → Term 𝔸 sig X} :
+    π • Term.free a f args = Term.free (π • a) f ((π • ·) ∘ args) := rfl
+
+@[simp] lemma smul_bound {π : FPerm 𝔸} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → Term 𝔸 sig X} :
+    π • Term.bound a f args = Term.bound (π • a) f ((π • ·) ∘ args) := rfl
+
+private def atoms : Term 𝔸 sig X → Set 𝔸
+  | .var x => NominalSet.supp 𝔸 x
+  | .pure f args => ⋃₀ {atoms (args x) | x : sig.pureArgs f}
+  | .free a f args => {a} ∪ ⋃₀ {atoms (args x) | x : sig.freeArgs f}
+  | .bound a f args => {a} ∪ ⋃₀ {atoms (args x) | x : sig.boundArgs f}
+
+private lemma atoms_finite (t : Term 𝔸 sig X) : (atoms 𝔸 t).Finite := by
+  fun_induction atoms <;> all_goals expose_names
+  · exact NominalSet.supp_finite 𝔸
+  · have hfin := (sig.pureArgs_fintype f).finite
+    apply Set.Finite.sUnion
+    · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+      apply Set.finite_range
+    · intro S ⟨x, hS⟩
+      rw [← hS]
+      exact ih1 x
+  · have hfin := (sig.freeArgs_fintype f).finite
+    apply Set.Finite.union
+    · exact Set.finite_singleton a
+    · apply Set.Finite.sUnion
+      · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+        apply Set.finite_range
+      · intro S ⟨x, hS⟩
+        rw [← hS]
+        exact ih1 x
+  · have hfin := (sig.boundArgs_fintype f).finite
+    apply Set.Finite.union
+    · exact Set.finite_singleton a
+    · apply Set.Finite.sUnion
+      · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+        apply Set.finite_range
+      · intro S ⟨x, hS⟩
+        rw [← hS]
+        exact ih1 x
+
+private lemma atoms_support (t : Term 𝔸 sig X) : PermSet.HasSupport 𝔸 t (atoms 𝔸 t) := by
+  intro π
+  fun_induction atoms <;> all_goals expose_names
+  · have hsupp : PermSet.HasSupport 𝔸 x (NominalSet.supp 𝔸 x) := NominalSet.supp_is_support 𝔸
+    intro hπ
+    simp only [PermSet.fix', smul_var, Term.var.injEq, Set.mem_setOf_eq]
+    exact hsupp hπ
+  · intro hπ
+    simp only [PermSet.fix', smul_pure, Term.pure.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq]
+    ext x
+    rw [Function.comp_apply]
+    apply ih1
+    apply PermSet.fix_antitone_mem 𝔸 hπ
+    apply Set.subset_sUnion_of_mem
+    use x
+  · intro hπ
+    simp only [PermSet.fix', smul_free, Term.free.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq]
+    constructor
+    · apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_left
+      rfl
+    · ext x
+      rw [Function.comp_apply]
+      apply ih1
+      apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_of_subset_right
+      apply Set.subset_sUnion_of_mem
+      use x
+  · intro hπ
+    simp only [PermSet.fix', smul_bound, Term.bound.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq]
+    constructor
+    · apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_left
+      rfl
+    · ext x
+      rw [Function.comp_apply]
+      apply ih1
+      apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_of_subset_right
+      apply Set.subset_sUnion_of_mem
+      use x
+
+instance : NominalSet 𝔸 (Term 𝔸 sig X) where
+  fin_supp t := by
+    use atoms 𝔸 t
+    exact ⟨atoms_support 𝔸 t, atoms_finite 𝔸 t⟩
+
 private def rename {n : ℕ} (π : FPerm 𝔸) (t : TermAtDepth 𝔸 sig X n) : TermAtDepth 𝔸 sig X n :=
   ⟨π • t.val, by
     suffices ∀ t n, t.HasDepth 𝔸 n → (rename' 𝔸 π t).HasDepth 𝔸 n by
@@ -109,9 +203,11 @@ private def rename {n : ℕ} (π : FPerm 𝔸) (t : TermAtDepth 𝔸 sig X n) :
         constructor; intro arg
         apply ih1; exact h arg⟩
 
-instance {n : ℕ} : PermSet 𝔸 (TermAtDepth 𝔸 sig X n) where
-  smul := rename 𝔸
-  one_smul t := by apply Subtype.eq; exact one_rename 𝔸 t.val
-  mul_smul π τ t := by apply Subtype.eq; exact mul_rename 𝔸 π τ t.val
+instance Term.instHasDepthEquivariant {n : ℕ} : Set.Equivariant 𝔸 {t : Term 𝔸 sig X | HasDepth 𝔸 t n} := by
+  constructor; intro t π ht
+  exact (rename 𝔸 π ⟨t, ht⟩).prop
+
+instance {n : ℕ} : NominalSet 𝔸 (TermAtDepth 𝔸 sig X n) :=
+  (Subtype.instNominalSetElem 𝔸 : NominalSet 𝔸 {t : Term 𝔸 sig X | Term.HasDepth 𝔸 t n})
 
 end Algebra