1 files changed, 61 insertions, 46 deletions

diff --git a/Algebra/Term.lean b/Algebra/Term.lean
index 665999f..b4d18f9 100644
--- a/Algebra/Term.lean
+++ b/Algebra/Term.lean
@@ -55,21 +55,35 @@ inductive Term.HasDepth : Term 𝔸 sig X → ℕ → Prop
 def TermAtDepth (sig : Signature) (X : Type) [NominalSet 𝔸 X] (n : ℕ) :=
   { t : Term 𝔸 sig X // t.HasDepth 𝔸 n }
 
+def TermAtDepth.var (x : X) : TermAtDepth 𝔸 sig X 0 := ⟨.var x, by constructor⟩
+
+def TermAtDepth.pure {n : ℕ} (f : sig.pure) (args : sig.pureArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.pureDepth f) :=
+  ⟨.pure f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
+def TermAtDepth.free {n : ℕ} (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.freeDepth f) :=
+  ⟨.free a f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
+def TermAtDepth.bound {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.boundDepth f) :=
+  ⟨.bound a f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
 def Substitution (sig : Signature) (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] (l : ℕ) :=
   X → TermAtDepth 𝔸 sig Y l
 
-private def Substitution.apply' {l : ℕ} (σ : Substitution 𝔸 sig X Y l) : Term 𝔸 sig X → Term 𝔸 sig Y
+def Substitution.apply {l : ℕ} (σ : Substitution 𝔸 sig X Y l) : Term 𝔸 sig X → Term 𝔸 sig Y
   | .var x => (σ x).val
-  | .pure f args => .pure f (fun x => σ.apply' (args x))
-  | .free a f args => .free a f (fun x => σ.apply' (args x))
-  | .bound a f args => .bound a f (fun x => σ.apply' (args x))
+  | .pure f args => .pure f (fun x => σ.apply (args x))
+  | .free a f args => .free a f (fun x => σ.apply (args x))
+  | .bound a f args => .bound a f (fun x => σ.apply (args x))
 
-def Substitution.apply {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermAtDepth 𝔸 sig X n) :
+def Substitution.applyUniform {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermAtDepth 𝔸 sig X n) :
     TermAtDepth 𝔸 sig Y (n + l) :=
-  ⟨σ.apply' 𝔸 t.val, by
-    suffices ∀ t n, t.HasDepth 𝔸 n → (σ.apply' 𝔸 t).HasDepth 𝔸 (n + l) by
+  ⟨σ.apply 𝔸 t.val, by
+    suffices ∀ t n, t.HasDepth 𝔸 n → (σ.apply 𝔸 t).HasDepth 𝔸 (n + l) by
       exact this t.val n t.prop
-    intro t; fun_induction apply'
+    intro t; fun_induction apply
     · intro n h; cases h
       rw [Nat.zero_add]
       exact (σ _).prop
@@ -79,21 +93,36 @@ def Substitution.apply {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermA
       constructor; intro arg
       apply ih1; exact h arg⟩
 
-private def rename' (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig X
+@[simp] lemma Substitution.apply_var {l : ℕ} {x : X} {σ : Substitution 𝔸 sig X Y l} :
+    σ.apply 𝔸 (.var x) = (σ x).val := rfl
+
+@[simp] lemma Substitution.apply_pure
+    {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} {l : ℕ} {σ : Substitution 𝔸 sig X Y l} :
+    σ.apply 𝔸 (.pure f args) = .pure f (apply 𝔸 σ ∘ args) := rfl
+
+@[simp] lemma Substitution.apply_free
+    {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → Term 𝔸 sig X} {l : ℕ} {σ : Substitution 𝔸 sig X Y l} :
+    σ.apply 𝔸 (.free a f args) = .free a f (apply 𝔸 σ ∘ args) := rfl
+
+@[simp] lemma Substitution.apply_bound
+    {a : 𝔸} {f : sig.bound} {l : ℕ} {args : sig.boundArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y l} :
+    σ.apply 𝔸 (.bound a f args) = .bound a f (apply 𝔸 σ ∘ args) := rfl
+
+private def rename (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig 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))
+  | .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))
 
-private lemma one_rename (t : Term 𝔸 sig X) : rename' 𝔸 1 t = t := by
-  induction' t <;> all_goals simp [rename', *]
+private lemma one_rename (t : Term 𝔸 sig X) : rename 𝔸 1 t = t := by
+  induction' t <;> all_goals simp [rename, *]
 
 private lemma mul_rename (π τ : FPerm 𝔸) (t : Term 𝔸 sig X) :
-    rename' 𝔸 (π * τ) t = rename' 𝔸 π (rename' 𝔸 τ t) := by
-  induction' t <;> all_goals simp [rename', mul_smul, *]
+    rename 𝔸 (π * τ) t = rename 𝔸 π (rename 𝔸 τ t) := by
+  induction' t <;> all_goals simp [rename, mul_smul, *]
 
 instance : PermSet 𝔸 (Term 𝔸 sig X) where
-  smul := rename' 𝔸
+  smul := rename 𝔸
   one_smul := one_rename 𝔸
   mul_smul := mul_rename 𝔸
 
@@ -159,21 +188,10 @@ private lemma atoms_support (t : Term 𝔸 sig X) : PermSet.HasSupport 𝔸 t (a
     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]
+  all_goals
+    intro hπ
+    simp only [PermSet.fix', smul_free, smul_bound, Term.free.injEq, Term.bound.injEq, heq_eq_eq,
+      true_and, Set.mem_setOf_eq]
     constructor
     · apply PermSet.fix_antitone_mem 𝔸 hπ
       apply Set.subset_union_left
@@ -191,21 +209,18 @@ instance : NominalSet 𝔸 (Term 𝔸 sig X) where
     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
-      exact this t.val n t.prop
-    intro t; fun_induction rename'
-    · intro n h; cases h; constructor
-    all_goals
-        intro n h; cases h
-        expose_names
-        constructor; intro arg
-        apply ih1; exact h arg⟩
-
-instance Term.instHasDepthEquivariant {n : ℕ} : Set.Equivariant 𝔸 {t : Term 𝔸 sig X | HasDepth 𝔸 t n} := by
+instance Term.instHasDepthEquivariant {n : ℕ} :
+    Set.Equivariant 𝔸 {t : Term 𝔸 sig X | HasDepth 𝔸 t n} := by
   constructor; intro t π ht
-  exact (rename 𝔸 π ⟨t, ht⟩).prop
+  suffices ∀ t n, t.HasDepth 𝔸 n → (rename 𝔸 π t).HasDepth 𝔸 n by
+    exact this t n ht
+  intro t; fun_induction rename
+  · intro n h; cases h; constructor
+  all_goals
+      intro n h; cases h
+      expose_names
+      constructor; intro arg
+      apply ih1; exact h arg
 
 instance {n : ℕ} : NominalSet 𝔸 (TermAtDepth 𝔸 sig X n) :=
   (Subtype.instNominalSetElem 𝔸 : NominalSet 𝔸 {t : Term 𝔸 sig X | Term.HasDepth 𝔸 t n})