Documentation

LeanSubst.Misc

source
instance LeanSubst.instSubstMapRenComposeLeftList {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [SubstMapRenComposeLeft S V] :
SubstMapRenComposeLeft (List S) V
source
instance LeanSubst.instSubstMapRenComposeRightList {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapAll V] [SubstMap S V] [SubstMapRenComposeRight S V] :
SubstMapRenComposeRight (List S) V
source
@[simp]
theorem LeanSubst.Subst.rewrite3_cons_ren_fix {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {a : Action T} {σ : Subst T} {r : Ren T} :
a :: σ >> r = a⟨r⟩ :: (σ >> r)
source
@[simp]
theorem LeanSubst.Subst.rewrite3_cons_ren_subst {T : Type u2} [SubstMap T [T]] {x : Nat} {σ : Subst T} {r : Ren T} :
x :: r >> σ = σ.act x :: (r >> σ)
source
@[simp]
theorem LeanSubst.Subst.ren_succ_beta_to {T : Type u2} {a : Action T} {r : Ren T} :
(r >> 𝐫1(T)) >> a :: 𝐬0(T) = r.to
source
theorem LeanSubst.Ren.lift_of_succ_rev {S : Type u1} {k : Nat} {r : Ren S} :
r.lift (1 + k) = r.lift.lift k
source
theorem LeanSubst.Ren.lift_of_add {S : Type u1} {a b : Nat} {r : Ren S} :
r.lift (a + b) = (r.lift a).lift b
source
theorem LeanSubst.Subst.compose_commute_add_ren_subst {T : Type u2} [RenMap T [T]] [SubstMap T [T]] [SubstMapStable T [T]] {k : Nat} {τ : Subst T} :
τ >> Ren.add T k = Ren.add T k >> τ.lift k
source
theorem LeanSubst.Subst.compose_commute_add_ren {T : Type u2} [RenMap T [T]] {k : Nat} {r : Ren T} :
r >> add T k = add T k >> r.lift k
source
theorem LeanSubst.Subst.compose_commute_add_ren_ren {T : Type u2} {k : Nat} {r : Ren T} :
r >> Ren.add T k = Ren.add T k >> r.lift k
source
@[simp]
theorem LeanSubst.Ren.to_cons {T : Type u2} {x : Nat} {r : Ren T} :
(x :: r).to = re x :: r.to
source
theorem LeanSubst.Ren.cons_add_succ {T : Type u_1} {n : Nat} :
n :: add T (n + 1) = add T n
source
theorem LeanSubst.Ren.assoc {T : Type u_1} {xs ys : List Nat} {r : Ren T} :
xs ++ (ys ++ r) = xs ++ ys ++ r
source
theorem LeanSubst.Ren.append_range_succ_succ {T : Type u_1} {s e : Nat} {r : Ren T} {h : s ≤ e + 1} :
s..(e + 2) ++ r = s..(e + 1) ++ (e + 1) :: r
source
theorem LeanSubst.Subst.rewrite1_append_ren_le {T : Type u_1} {s e : Nat} :
s..e ++ Ren.add T e = Ren.add T (min s e)
source
theorem LeanSubst.subst_append_assoc_nat {T : Type u_1} {xs ys : List Nat} {σ : Subst T} :
xs ++ (ys ++ σ) = xs ++ ys ++ σ
source
theorem LeanSubst.Subst.append_range_succ_succ {T : Type u_1} {s e : Nat} {σ : Subst T} {h : s ≤ e + 1} :
s..(e + 2) ++ σ = s..(e + 1) ++ re (e + 1) :: σ
source
theorem LeanSubst.Subst.cons_add_succ {T : Type u_1} {n : Nat} :
re n :: add T (n + 1) = add T n
source
theorem LeanSubst.Subst.rewrite1_append_le {T : Type u_1} {s e : Nat} :
s..e ++ add T e = add T (min s e)
source
@[simp]
theorem LeanSubst.Subst.rewrite1_append_ren {T : Type u2} {e : Nat} :
0..e ++ Ren.add T e = 𝐫0(T)
source
@[simp]
theorem LeanSubst.Subst.rewrite1_append {T : Type u2} {e : Nat} :
0..e ++ add T e = 𝐬0(T)
source
theorem LeanSubst.Subst.rewrite_lift_ren {T : Type u2} {r : Ren T} :
r.lift = 0 :: (r >> 𝐫1(T))
source
@[simp]
theorem LeanSubst.Subst.rewrite3_append_ren_ren_cons {T : Type u2} {x : Nat} {r1 r2 : Ren T} :
x :: r1 >> r2 = r2.act x :: (r1 >> r2)
source
@[simp]
theorem LeanSubst.Subst.rewrite3_append_ren_ren {T : Type u2} {ℓ : List Nat} {r1 r2 : Ren T} :
ℓ ++ r1 >> r2 = ℓ⟨r2⟩ ++ (r1 >> r2)
source
@[simp]
theorem LeanSubst.range_act_succ_ren_fixed {T : Type u2} {s e : Nat} :
(s..e)⟨𝐫1(T)⟩ = s.succ..e.succ
source
theorem LeanSubst.Subst.rewrite_lift_k_ren {T : Type u2} {k : Nat} {r : Ren T} :
r.lift k = 0..k ++ (r >> Ren.add T k)
source
@[simp]
theorem LeanSubst.Subst.rewrite4_cons_ren_add_direct {T : Type u2} {r : Ren T} {ℓ : List Nat} :
Ren.add T ℓ.length >> ℓ ++ r = r
source
@[simp]
theorem LeanSubst.Subst.rewrite4_cons_ren_add_indirect {T : Type u2} {k : Nat} {r : Ren T} {ℓ : List Nat} {h : k = ℓ.length} :
Ren.add T k >> ℓ ++ r = r
source
@[simp]
theorem LeanSubst.Subst.rewrite4_append_add_direct {T : Type u2} {σ : Subst T} {ℓ : List (Action T)} :
Ren.add T ℓ.length >> ℓ ++ σ = σ
source
@[simp]
theorem LeanSubst.Subst.rewrite4_append_add_indirect {T : Type u2} {k : Nat} {σ : Subst T} {ℓ : List (Action T)} {h : k = ℓ.length} :
Ren.add T k >> ℓ ++ σ = σ
source
theorem LeanSubst.Subst.compose_ren_left_cons_lift_1 {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {a : Action T} {r : Ren T} {σ : Subst T} :
r.lift >> a :: σ = a :: (r >> σ)
source
@[simp]
theorem LeanSubst.Subst.compose_ren_left_cons_lift_k1 {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {k : Nat} {a : Action T} {r : Ren T} {σ : Subst T} :
r.lift (k + 1) >> a :: σ = a :: (r.lift k >> σ)
source
theorem LeanSubst.Subst.compose_ren_left_cons_lift_direct {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {ℓ : List (Action T)} {r : Ren T} {σ : Subst T} :
r.lift ℓ.length >> ℓ ++ σ = ℓ ++ (r >> σ)
source
@[simp]
theorem LeanSubst.Subst.compose_ren_right_append {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {ℓ : List (Action T)} {r : Ren T} {σ : Subst T} :
ℓ ++ σ >> r = ℓ⟨r⟩ ++ (σ >> r)
source
@[simp]
theorem LeanSubst.Subst.compose_ren_right_assoc {S : Type u1} [RenMap S [S]] [SubstMap S [S]] [SubstMapRenComposeLeft S [S]] {σ τ : Subst S} {r : Ren S} :
(σ >> r) >> τ = σ >> r >> τ
source
@[simp]
theorem LeanSubst.Subst.compose_ren_right_assoc2 {S : Type u1} [RenMapAll [S]] [SubstMap S [S]] [RenMapVecDef S S []] [RenMapEmpty S] [SubstMapRenComposeRight S [S]] {σ τ : Subst S} {r : Ren S} :
(σ >> τ) >> r = σ >> τ >> r
source
@[simp]
theorem LeanSubst.Subst.to_append {T : Type u2} {ℓ : List Nat} {r : Ren T} :
(ℓ ++ r).to = ℓ ++ r.to
source
@[simp]
theorem LeanSubst.Subst.ren_rewrite1 {T : Type u2} [RenMap T [T]] {r : Ren T} :
𝐬0(T) >> r = r.to
source
@[simp]
theorem LeanSubst.Subst.ren_rewrite1_left {T : Type u2} {r : Ren T} :
r >> 𝐬0(T) = r.to
source
@[simp]
theorem LeanSubst.Subst.compose_ren_right_from_to {T : Type u2} [SubstMap T [T]] [RenMap T [T]] [SubstMapStable T [T]] {σ : Subst T} {r : Ren T} :
σ >> r.to = σ >> r
source
@[simp]
theorem LeanSubst.Subst.compose_compose_left_succ {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {x : Action T} {σ τ : Subst T} :
(σ >> 𝐫1(T)) >> x :: τ = σ >> τ
source
theorem LeanSubst.Subst.compose_left_cons_lift1_indirect {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {x : Action T} {σ τ : Subst T} :
σ.lift >> x :: τ = x :: (σ >> τ)
source
@[simp]
theorem LeanSubst.Subst.List.smap_append {S : Type u1} {V : List (Type u2)} [SubstMap S V] {a b : List S} {σ : SubstVec V} :
(a ++ b)[σ,] = a[σ,] ++ b[σ,]
source
@[simp]
theorem LeanSubst.Subst.List.rmap_reverse {S : Type u1} {V : List (Type u2)} [RenMap S V] {ℓ : List S} {r : RenVec V} :
ℓ.reverse⟨r,⟩ = ℓ⟨r,⟩.reverse
source
@[simp]
theorem LeanSubst.Subst.List.smap_reverse {S : Type u1} {V : List (Type u2)} [SubstMap S V] {ℓ : List S} {σ : SubstVec V} :
ℓ.reverse[σ,] = ℓ[σ,].reverse
source
@[simp]
theorem LeanSubst.Subst.List.rmap_map_su {T : Type u2} [RenMap T [T]] {ℓ : List T} {r : Ren T} :
(List.map su ℓ)⟨r⟩ = List.map su ℓ⟨r⟩
source
@[simp]
theorem LeanSubst.Subst.List.smap_map_su {T : Type u2} [SubstMap T [T]] {ℓ : List T} {σ : Subst T} :
(List.map su ℓ)[σ] = List.map su ℓ[σ]
source
def LeanSubst.tacticSubst_solve_id :
Lean.ParserDescr
Equations
Instances For
    source
    def LeanSubst.tacticSubst_solve_stable :
    Lean.ParserDescr
    Equations
    Instances For
      source
      def LeanSubst.tacticSubst_solve_compose :
      Lean.ParserDescr
      Equations
      Instances For