Documentation

LeanSubst.IsRen

class LeanSubst.HasSimpleVar (T : Type u) [SubstMap T] :

var : Nat → T
smap {lf : Subst.Lift T} {f : Nat → Subst.Action T} {i : Nat} : SubstMap.smap lf f (var i) = match f i with | Subst.Action.re k => var k | Subst.Action.su t => t

Instances

def LeanSubst.tacticSolve_simple_var_smap :

Lean.ParserDescr

Equations

LeanSubst.tacticSolve_simple_var_smap = Lean.ParserDescr.node `LeanSubst.tacticSolve_simple_var_smap 1024 (Lean.ParserDescr.nonReservedSymbol "solve_simple_var_smap" false)

Instances For

@[simp]

theorem LeanSubst.HasSimpleVar.smap_eq {T : Type u} [SubstMap T] [HasSimpleVar T] {lf : Subst.Lift T} {f : Nat → Subst.Action T} {i : Nat} :

SubstMap.smap lf f (var i) = match f i with | Subst.Action.re k => var k | Subst.Action.su t => t

@[simp]

theorem LeanSubst.HasSimpleVar.ren {T : Type u} [SubstMap T] [HasSimpleVar T] {k : Nat} (r : Ren) :

r.apply (var k) = var (r k)

@[simp]

theorem LeanSubst.HasSimpleVar.sub {T : Type u} [SubstMap T] [HasSimpleVar T] {i : Nat} (σ : Subst T) :

var i[σ] = match σ i with | Subst.Action.re k => var k | Subst.Action.su t => t

theorem LeanSubst.HasSimpleVar.re {T : Type u} [SubstMap T] [HasSimpleVar T] {i k : Nat} {σ : Subst T} :

σ i = #k → var i[σ] = var k

theorem LeanSubst.HasSimpleVar.su {T : Type u} [SubstMap T] [HasSimpleVar T] {i : Nat} {t : T} {σ : Subst T} :

σ i = %t → var i[σ] = t

def LeanSubst.IsRen {T : Type u} [SubstMap T] [HasSimpleVar T] (σ : Subst T) :

Equations

LeanSubst.IsRen σ = ∀ (i : Nat), ∃ (k : Nat ), σ i = #k ∨ σ i = %(LeanSubst.HasSimpleVar.var k)

Instances For

theorem LeanSubst.IsRen.var_forced {T : Type u} [SubstMap T] [HasSimpleVar T] {i : Nat} {t : T} {σ : Subst T} :

IsRen σ → σ i = %t → ∃ (k : Nat ), t = HasSimpleVar.var k

theorem LeanSubst.IsRen.var_apply_forced {T : Type u} [SubstMap T] [HasSimpleVar T] {σ : Subst T} (x : Nat) :

IsRen σ → ∃ (k : Nat ), HasSimpleVar.var x[σ] = HasSimpleVar.var k

theorem LeanSubst.IsRen.I {T : Type u} [SubstMap T] [HasSimpleVar T] :

IsRen LeanSubst.I

theorem LeanSubst.IsRen.S {T : Type u} [SubstMap T] [HasSimpleVar T] :

IsRen LeanSubst.S

theorem LeanSubst.IsRen.to {T : Type u} [SubstMap T] [HasSimpleVar T] (r : Ren) :

theorem LeanSubst.IsRen.cons_re {T : Type u} [SubstMap T] [HasSimpleVar T] {σ : Subst T} (k : Nat) :

IsRen σ → IsRen (#k::σ)

theorem LeanSubst.IsRen.cons_su {T : Type u} [SubstMap T] [HasSimpleVar T] {σ : Subst T} (k : Nat) :

IsRen σ → IsRen (%(HasSimpleVar.var k)::σ)

theorem LeanSubst.IsRen.lift {T : Type u} [SubstMap T] [HasSimpleVar T] {σ : Subst T} :

IsRen σ → IsRen σ.lift

theorem LeanSubst.IsRen.compose {T : Type u} [SubstMap T] [HasSimpleVar T] {σ τ : Subst T} :

IsRen σ → IsRen τ → IsRen (σ ∘ τ)