add hetero subst laws

Author: amarmaduke

Examples/LambdaCalc.lean

@@ -52,15 +52,15 @@ namespace LeanSubst.Examples.LambdaCalc
 
   @[simp]
   theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ x := by
-    unfold Subst.apply; simp [SubstMap.smap]
+    simp [Subst.apply, SubstMap.smap]
 
   @[simp]
   theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by
-    unfold Subst.apply; simp [SubstMap.smap]
+    simp [Subst.apply, SubstMap.smap]
 
   @[simp]
   theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by
-    unfold Subst.apply; simp [SubstMap.smap]
+    simp [Subst.apply, SubstMap.smap]
 
   @[simp]
   theorem Term.from_action_compose {x} {σ τ : Subst Term}
@@ -81,7 +81,7 @@ namespace LeanSubst.Examples.LambdaCalc
     : r = σ -> Ren.apply (T := Term) r = Subst.apply σ
   := by solve_stable Term, r, σ
 
-  instance : SubstMapStable Term Term where
+  instance : SubstMapStable Term where
     apply_stable := apply_stable
 
   theorem apply_compose {s : Term} {σ τ : Subst Term} : s[σ][τ] = s[σ ∘ τ] := by

LeanSubst/Basic.lean

@@ -60,6 +60,8 @@ namespace LeanSubst
 
   def Subst.apply [RenMap T] [SubstMap S T] (σ : Subst T) : S -> S := SubstMap.smap Subst.lift σ
 
+  abbrev Subst.apply1 [RenMap S] [SubstMap S S] := Subst.apply (S := S) (T := S)
+
   def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T
   | σ, τ, n =>
     match σ n with
@@ -116,18 +118,20 @@ namespace LeanSubst
     funext; case _ x =>
     cases x <;> simp [Ren.to, Subst.compose]
 
-  abbrev the {T : Type} (_ : T) := T
-
-  macro:max t:term noWs "[" σ:term "]" : term => `(Subst.apply (S := the $t) (T := the $t) $σ $t)
+  macro:max t:term noWs "[" σ:term "]" : term => `(Subst.apply1 $σ $t)
   macro:max t:term noWs "[" σ:term ":" T:term "]" : term => `(Subst.apply (T := $T) $σ $t)
   infixr:85 " ∘ " => Subst.compose
-  infixr:85 " • " => Subst.hcompose
+  infixr:85 " ◾ " => Subst.hcompose
+
+  @[app_unexpander Subst.apply1]
+  def unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander
+  | `($_ $σ $t) => `($t[$σ])
+  | _ => throw ()
 
   @[app_unexpander Subst.apply]
   def unexpandSubstApply : Lean.PrettyPrinter.Unexpander
-  | `($_ $σ $t) => `($t[$σ])
+  | `($_ $σ $t) => `($t[$σ : _])
   | `($_ (T := $T) $σ $t) => `($t[$σ : $T])
-  | `($_ (S := the $_) (T := the $_) $σ $t) => `($t[$σ])
   | _ => throw ()
 
 end LeanSubst

LeanSubst/Laws.lean

@@ -128,6 +128,115 @@ namespace LeanSubst
       simp [Subst.compose]
       cases σ x <;> simp
 
+  @[simp]
+  theorem hrewrite1
+    [RenMap T] [SubstMap S T] [SubstMapId S T]
+    {σ : Subst S}
+    : σ ◾ (+0@T) = σ
+  := by
+    funext; case _ x =>
+    simp [Subst.hcompose]
+    generalize zdef : σ x = z
+    cases z <;> simp
+
+  theorem hcomp_ren_left
+    [RenMap S] [RenMap T] [SubstMap S T]
+    (r : Ren) (σ : Subst T)
+    : (@Ren.to S r) ◾ σ = r.to
+  := by
+    funext; case _ x =>
+    induction x <;> simp [Subst.hcompose, Ren.to]
+
+  @[simp]
+  theorem hrewrite2
+    [RenMap S] [RenMap T] [SubstMap S T]
+    {σ : Subst T}
+    : (+0@S) ◾ σ = +0
+  := by
+    have lem := hcomp_ren_left (S := S) (T := T) (λ x => x) σ
+    simp at lem; exact lem
+
+  @[simp]
+  theorem hrewrite3
+    [RenMap S] [RenMap T] [SubstMap S T]
+    {σ : Subst T}
+    : (+1@S) ◾ σ = +1
+  := by
+    have lem := hcomp_ren_left (S := S) (T := T) (· + 1) σ
+    simp at lem; exact lem
+
+  @[simp]
+  theorem hrewrite4
+    [RenMap T] [SubstMap S T]
+    {x} {σ : Subst S} {τ : Subst T}
+    : (re x :: σ) ◾ τ = re x :: (σ ◾ τ)
+  := by
+    funext; case _ i =>
+    cases i <;> simp [Subst.hcompose]
+
+  theorem hcomp_dist_ren_left
+    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
+    (r : Ren) {σ : Subst S} {τ : Subst T}
+    : (r.to ∘ σ) ◾ τ = r.to ∘ σ ◾ τ
+  := by
+    funext; case _ x =>
+    simp [Subst.hcompose, Subst.compose, Ren.to]
+
+  class SubstMapRenCommute (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] where
+    apply_ren_commute {s : S} (r : Ren) (τ : Subst T) : s[r.to][τ:T] = s[τ:T][r.to]
+
+  @[simp]
+  theorem hrewrite5
+    [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
+    {σ : Subst S} {τ μ : Subst T}
+    : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ)
+  := by
+    funext; case _ x =>
+    simp [Subst.hcompose]
+    generalize zdef : σ x = z
+    cases z <;> simp
+
+  theorem hcomp_distr_ren_right
+    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T]
+    (r : Ren) (σ : Subst S) (μ : Subst T)
+    : (σ ∘ r.to) ◾ μ = (σ ◾ μ) ∘ r.to
+  := by
+    funext; case _ x =>
+    simp [Subst.hcompose, Subst.compose, Ren.to]
+    generalize zdef : σ x = z
+    cases z <;> simp
+    rw [SubstMapRenCommute.apply_ren_commute r μ]
+
+  @[simp]
+  theorem hrewrite6
+    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T]
+    (r : Ren) (σ : Subst S)
+    : (σ ∘ r.to) ◾ (+1@T) = (σ ◾ +1@T) ∘ r.to
+  := by
+    have lem := hcomp_distr_ren_right (T := T) r σ +1
+    simp at lem; exact lem
+
+  class SubstMapHetCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] where
+    apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ:T] = s[τ:T][σ ◾ τ]
+
+  @[simp]
+  theorem apply_hcompose
+    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
+    {s : S} {σ : Subst S} {τ : Subst T}
+    : s[σ][τ:T] = s[τ:T][σ ◾ τ]
+  := by exact SubstMapHetCompose.apply_hcompose
+
+  @[simp]
+  theorem hrewrite7
+    [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
+    {σ τ : Subst S} (μ : Subst T)
+    : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ
+  := by
+    funext; case _ x =>
+    simp [Subst.hcompose, Subst.compose]
+    generalize zdef : σ x = z
+    cases z <;> simp
+
   end Subst
 
   macro "solve_stable" S:term "," r:term "," σ:term : tactic => `(tactic| {
@@ -136,7 +245,7 @@ namespace LeanSubst
     induction t generalizing $r $σ
     all_goals simp [RenMap.rmap, SubstMap.smap, *] at *; try simp [*]
     any_goals solve | (
-      rw [<-Ren.lift_eq_from_eq (S := $S) h])
+      rw [<-Ren.lift_eq_from_eq (S := $S) (r := $r) h])
     any_goals solve | (rw [<-h]; simp [Ren.to])
   })
 
@@ -152,13 +261,14 @@ namespace LeanSubst
       cases x <;> simp
       case _ x => simp [Ren.to, Subst.succ, Subst.compose]
     have lem2s {σ : Subst $Ty} : (+1 ∘ σ).lift = +1.lift ∘ σ.lift := by rw [<-Ren.to_succ, lem2]
-    have lem3 {σ : Subst $Ty} {r : Ren} {t} : t[r][σ] = t[r ∘ σ] := by
+    have lem3 {σ : Subst $Ty} {r : Ren} {t : $Ty} : t[r:$Ty][σ:_] = t[(r ∘ σ):_] := by
       induction t generalizing σ r
       any_goals solve | simp [*]
       any_goals solve | (
         simp [-Subst.rewrite_lift, *]
         rw [<-Ren.to_lift (S := $Ty)]; simp [*])
-    have lem3s {σ : Subst $Ty} {t} : t[+1][σ] = t[+1 ∘ σ] := by rw [<-Ren.to_succ, lem3]
+    have lem3s {σ : Subst $Ty} {t : $Ty} : t[+1:$Ty][σ:_] = t[+1 ∘ σ:_] := by
+      rw [<-Ren.to_succ, lem3]
     have lem4 {σ τ : Subst $Ty} : +1 ∘ τ ∘ σ = (+1 ∘ τ) ∘ σ := by
       funext; case _ x =>
       cases x <;> simp [Subst.compose, Subst.succ]
@@ -174,13 +284,14 @@ namespace LeanSubst
         simp [Subst.compose]
         cases τ x <;> simp [*]
     have lem6s {τ : Subst $Ty} : (τ ∘ +1).lift = τ.lift ∘ +1.lift := by rw [<-Ren.to_succ, lem6]
-    have lem7 {τ : Subst $Ty} {t} {r : Ren} : t[τ][r] = t[τ ∘ r.to] := by
+    have lem7 {τ : Subst $Ty} {t:$Ty} {r : Ren} : t[τ:_][r:$Ty] = t[τ ∘ r.to:_] := by
       induction t generalizing τ r
       any_goals solve | simp [*]
       any_goals solve | (
         simp [-Subst.rewrite_lift, *]
         rw [<-Ren.to_lift (S := $Ty)]; simp [*])
-    have lem7s {τ : Subst $Ty} {t} : t[τ][+1] = t[τ ∘ +1] := by rw [<-Ren.to_succ, lem7]
+    have lem7s {τ : Subst $Ty} {t : $Ty} : t[τ:_][+1:$Ty] = t[τ ∘ +1:_] := by
+      rw [<-Ren.to_succ, lem7]
     have lem8 {σ τ : Subst $Ty} : (σ ∘ +1) ∘ τ = σ ∘ +1 ∘ τ := by
       funext; case _ x =>
       unfold Subst.compose; simp