differentiate bw substitution and uniform substitution

1 files changed, 44 insertions, 19 deletions

diff --git a/Algebra/Term.lean b/Algebra/Term.lean
index b4d18f9..fe7e742 100644
--- a/Algebra/Term.lean
+++ b/Algebra/Term.lean
@@ -69,21 +69,42 @@ def TermAtDepth.bound {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs
     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
+def Substitution (sig : Signature) (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] :=
+  X → Term 𝔸 sig Y
 
-def Substitution.apply {l : ℕ} (σ : Substitution 𝔸 sig X Y l) : Term 𝔸 sig X → Term 𝔸 sig Y
-  | .var x => (σ x).val
+def Substitution.apply (σ : Substitution 𝔸 sig X Y) : Term 𝔸 sig X → Term 𝔸 sig Y
+  | .var x => σ 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.applyUniform {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t : TermAtDepth 𝔸 sig X n) :
+@[simp] lemma Substitution.apply_var {x : X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply 𝔸 (.var x) = (σ x) := rfl
+
+@[simp] lemma Substitution.apply_pure
+    {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y} :
+    σ.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} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply 𝔸 (.free a f args) = .free a f (apply 𝔸 σ ∘ args) := rfl
+
+@[simp] lemma Substitution.apply_bound
+    {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply 𝔸 (.bound a f args) = .bound a f (apply 𝔸 σ ∘ args) := rfl
+
+def UniformSubstitution (sig : Signature) (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] (l : ℕ) :=
+  X → TermAtDepth 𝔸 sig Y l
+
+def UniformSubstitution.toSubstitution {l : ℕ} (σ : UniformSubstitution 𝔸 sig X Y l) : Substitution 𝔸 sig X Y :=
+  fun x => (σ x).val
+
+def UniformSubstitution.apply {n l : ℕ} (σ : UniformSubstitution 𝔸 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
+  ⟨σ.toSubstitution.apply 𝔸 t.val, by
+    suffices ∀ t n, t.HasDepth 𝔸 n → (σ.toSubstitution.apply 𝔸 t).HasDepth 𝔸 (n + l) by
       exact this t.val n t.prop
-    intro t; fun_induction apply
+    intro t; fun_induction Substitution.apply
     · intro n h; cases h
       rw [Nat.zero_add]
       exact (σ _).prop
@@ -93,20 +114,24 @@ def Substitution.applyUniform {n l : ℕ} (σ : Substitution 𝔸 sig X Y l) (t
       constructor; intro arg
       apply ih1; exact h arg⟩
 
-@[simp] lemma Substitution.apply_var {l : ℕ} {x : X} {σ : Substitution 𝔸 sig X Y l} :
-    σ.apply 𝔸 (.var x) = (σ x).val := rfl
+@[simp] lemma UniformSubstitution.apply_var
+    {x : X} {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply 𝔸 (.var 𝔸 x)).val = (σ 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 UniformSubstitution.apply_pure
+    {n : ℕ} {f : sig.pure} {args : sig.pureArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply 𝔸 (.pure 𝔸 f args)).val = (TermAtDepth.pure 𝔸 f (apply 𝔸 σ ∘ args)).val := 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 UniformSubstitution.apply_free
+    {n : ℕ} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply 𝔸 (.free 𝔸 a f args)).val = (TermAtDepth.free 𝔸 a f (apply 𝔸 σ ∘ args)).val := 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
+@[simp] lemma UniformSubstitution.apply_bound
+    {n : ℕ} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply 𝔸 (.bound 𝔸 a f args)).val = (TermAtDepth.bound 𝔸 a f (apply 𝔸 σ ∘ args)).val := rfl
 
 private def rename (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig X
   | .var x => .var (π • x)