Implementation of simultaneous substitutions following Schäfer/Tebbi/Smolka in Autosubst: Reasoning with de Bruijn Terms and Parallel Substitution.

def Expr.snoc {X : Sort u} (σ : ℕ → X) (x : X) : ℕ → X

Append an element to a substitution or a renaming.

Δ ⊢ σ : Γ  Γ ⊢ A  Δ ⊢ t : A[σ]
------------------------------
Δ ⊢ σ.t : Γ.A

Equations

• Expr.snoc σ x 0 = x
• Expr.snoc σ x n.succ = σ n

@[simp]

theorem Expr.snoc_zero {X : Sort u_1} (σ : ℕ → X) (x : X) : snoc σ x 0 = x

@[simp]

theorem Expr.snoc_succ {X : Sort u_1} (σ : ℕ → X) (x : X) (n : ℕ) : snoc σ x (n + 1) = σ n

Renaming

def Expr.upr (ξ : ℕ → ℕ) : ℕ → ℕ

Lift a renaming under a binder. See up.

Equations

• Expr.upr ξ = Expr.snoc (fun (i : ℕ) => ξ i + 1) 0

@[simp]

theorem Expr.upr_id : upr id = id

def Expr.rename {χ : Type u_1} (ξ : ℕ → ℕ) : Expr χ → Expr χ

Rename the de Bruijn indices in an expression.

Equations

• Expr.rename ξ (Expr.ax c A) = Expr.ax c (Expr.rename ξ A)
• Expr.rename ξ (Expr.bvar i) = Expr.bvar (ξ i)
• Expr.rename ξ (Expr.pi l l' A B) = Expr.pi l l' (Expr.rename ξ A) (Expr.rename (Expr.upr ξ) B)
• Expr.rename ξ (Expr.sigma l l' A B) = Expr.sigma l l' (Expr.rename ξ A) (Expr.rename (Expr.upr ξ) B)
• Expr.rename ξ (Expr.lam l l' A t) = Expr.lam l l' (Expr.rename ξ A) (Expr.rename (Expr.upr ξ) t)
• Expr.rename ξ (Expr.app l l' B fn arg) = Expr.app l l' (Expr.rename (Expr.upr ξ) B) (Expr.rename ξ fn) (Expr.rename ξ arg)
• Expr.rename ξ (Expr.pair l l' B t u) = Expr.pair l l' (Expr.rename (Expr.upr ξ) B) (Expr.rename ξ t) (Expr.rename ξ u)
• Expr.rename ξ (Expr.fst l l' A B p) = Expr.fst l l' (Expr.rename ξ A) (Expr.rename (Expr.upr ξ) B) (Expr.rename ξ p)
• Expr.rename ξ (Expr.snd l l' A B p) = Expr.snd l l' (Expr.rename ξ A) (Expr.rename (Expr.upr ξ) B) (Expr.rename ξ p)
• Expr.rename ξ (Expr.Id l A t u) = Expr.Id l (Expr.rename ξ A) (Expr.rename ξ t) (Expr.rename ξ u)
• Expr.rename ξ (Expr.refl l t) = Expr.refl l (Expr.rename ξ t)
• Expr.rename ξ (Expr.idRec l l' t C r u h) = Expr.idRec l l' (Expr.rename ξ t) (Expr.rename (Expr.upr (Expr.upr ξ)) C) (Expr.rename ξ r) (Expr.rename ξ u) (Expr.rename ξ h)
• Expr.rename ξ (Expr.univ l) = Expr.univ l
• Expr.rename ξ a.el = (Expr.rename ξ a).el
• Expr.rename ξ A.code = (Expr.rename ξ A).code

Substitution

@[irreducible]

def Expr.up {χ : Type u_1} (σ : ℕ → Expr χ) : ℕ → Expr χ

Lift a substitution under a binder.

Δ ⊢ σ : Γ  Γ ⊢ A
------------------------
Δ.A[σ] ⊢ (↑≫σ).v₀ : Γ.A

Warning: don't unfold this definition! Use up_eq_snoc instead.

Equations

• Expr.up σ = Expr.snoc (Expr.rename Nat.succ ∘ σ) (Expr.bvar 0)

@[simp]

theorem Expr.up_bvar (χ : Type u_2) : up bvar = bvar

def Expr.subst {χ : Type u_1} (σ : ℕ → Expr χ) : Expr χ → Expr χ

Apply a substitution to an expression.

Equations

• Expr.subst σ (Expr.ax c A) = Expr.ax c (Expr.subst σ A)
• Expr.subst σ (Expr.bvar i) = σ i
• Expr.subst σ (Expr.pi l l' A B) = Expr.pi l l' (Expr.subst σ A) (Expr.subst (Expr.up σ) B)
• Expr.subst σ (Expr.sigma l l' A B) = Expr.sigma l l' (Expr.subst σ A) (Expr.subst (Expr.up σ) B)
• Expr.subst σ (Expr.lam l l' A t) = Expr.lam l l' (Expr.subst σ A) (Expr.subst (Expr.up σ) t)
• Expr.subst σ (Expr.app l l' B fn arg) = Expr.app l l' (Expr.subst (Expr.up σ) B) (Expr.subst σ fn) (Expr.subst σ arg)
• Expr.subst σ (Expr.pair l l' B t u) = Expr.pair l l' (Expr.subst (Expr.up σ) B) (Expr.subst σ t) (Expr.subst σ u)
• Expr.subst σ (Expr.fst l l' A B p) = Expr.fst l l' (Expr.subst σ A) (Expr.subst (Expr.up σ) B) (Expr.subst σ p)
• Expr.subst σ (Expr.snd l l' A B p) = Expr.snd l l' (Expr.subst σ A) (Expr.subst (Expr.up σ) B) (Expr.subst σ p)
• Expr.subst σ (Expr.Id l A t u) = Expr.Id l (Expr.subst σ A) (Expr.subst σ t) (Expr.subst σ u)
• Expr.subst σ (Expr.refl l t) = Expr.refl l (Expr.subst σ t)
• Expr.subst σ (Expr.idRec l l' t C r u h) = Expr.idRec l l' (Expr.subst σ t) (Expr.subst (Expr.up (Expr.up σ)) C) (Expr.subst σ r) (Expr.subst σ u) (Expr.subst σ h)
• Expr.subst σ (Expr.univ l) = Expr.univ l
• Expr.subst σ a.el = (Expr.subst σ a).el
• Expr.subst σ A.code = (Expr.subst σ A).code

@[simp]

theorem Expr.subst_bvar (χ : Type u_2) : subst bvar = id

@[simp]

theorem Expr.subst_snoc_zero {χ : Type u_1} (σ : ℕ → Expr χ) (t : Expr χ) : subst (snoc σ t) (bvar 0) = t

def Expr.ofRen (χ : Type u_2) (ξ : ℕ → ℕ) : ℕ → Expr χ

Turn a renaming into a substitution.

Equations

• Expr.ofRen χ ξ i = Expr.bvar (ξ i)

@[simp]

theorem Expr.ofRen_id (χ : Type u_2) : ofRen χ id = bvar

theorem Expr.ofRen_upr (χ : Type u_2) (ξ : ℕ → ℕ) : ofRen χ (upr ξ) = up (ofRen χ ξ)

theorem Expr.rename_eq_subst_ofRen (χ : Type u_2) (ξ : ℕ → ℕ) : rename ξ = subst (ofRen χ ξ)

def Expr.comp {χ : Type u_1} (σ τ : ℕ → Expr χ) : ℕ → Expr χ

Compose two substitutions.

Θ ⊢ σ : Δ  Δ ⊢ τ : Γ
--------------------
Θ ⊢ σ≫τ : Γ

Equations

• Expr.comp σ τ = Expr.subst σ ∘ τ

@[simp]

theorem Expr.bvar_comp {χ : Type u_1} (σ : ℕ → Expr χ) : comp bvar σ = σ

@[simp]

theorem Expr.comp_bvar {χ : Type u_1} (σ : ℕ → Expr χ) : comp σ bvar = σ

theorem Expr.up_comp_ren_sb {χ : Type u_1} (ξ : ℕ → ℕ) (σ : ℕ → Expr χ) : up (σ ∘ ξ) = up σ ∘ upr ξ

theorem Expr.rename_subst {χ : Type u_1} (σ : ℕ → Expr χ) (ξ : ℕ → ℕ) (t : Expr χ) : subst σ (rename ξ t) = subst (σ ∘ ξ) t

theorem Expr.up_comp_sb_ren {χ : Type u_1} (σ : ℕ → Expr χ) (ξ : ℕ → ℕ) : up (rename ξ ∘ σ) = rename (upr ξ) ∘ up σ

theorem Expr.subst_rename {χ : Type u_1} (ξ : ℕ → ℕ) (σ : ℕ → Expr χ) (t : Expr χ) : rename ξ (subst σ t) = subst (rename ξ ∘ σ) t

theorem Expr.up_comp {χ : Type u_1} (σ τ : ℕ → Expr χ) : up (comp σ τ) = comp (up σ) (up τ)

theorem Expr.subst_subst {χ : Type u_1} (σ τ : ℕ → Expr χ) (t : Expr χ) : subst σ (subst τ t) = subst (comp σ τ) t

theorem Expr.comp_assoc {χ : Type u_1} (σ τ ρ : ℕ → Expr χ) : comp σ (comp τ ρ) = comp (comp σ τ) ρ

theorem Expr.comp_snoc {χ : Type u_1} (σ τ : ℕ → Expr χ) (t : Expr χ) : comp σ (snoc τ t) = snoc (comp σ τ) (subst σ t)

def Expr.wk {χ : Type u_1} : ℕ → Expr χ

The weakening substitution.

Γ ⊢ A
------------
Γ.A ⊢ ↑ : Γ

Equations

• Expr.wk = Expr.ofRen χ Nat.succ

@[simp]

theorem Expr.ofRen_succ (χ : Type u_2) : ofRen χ Nat.succ = wk

theorem Expr.up_eq_snoc {χ : Type u_1} (σ : ℕ → Expr χ) : up σ = snoc (comp wk σ) (bvar 0)

@[simp]

theorem Expr.snoc_comp_wk {χ : Type u_1} (σ : ℕ → Expr χ) (t : Expr χ) : comp (snoc σ t) wk = σ

@[simp]

theorem Expr.snoc_wk_zero (χ : Type u_2) : snoc wk (bvar 0) = bvar

theorem Expr.snoc_comp_wk_succ {χ : Type u_1} (σ : ℕ → Expr χ) (n : ℕ) : snoc (comp wk σ) (bvar (n + 1)) = comp wk (snoc σ (bvar n))

def Expr.toSb {χ : Type u_1} (t : Expr χ) : ℕ → Expr χ

A substitution that instantiates one binder.

Γ ⊢ t : A
--------------
Γ ⊢ id.t : Γ.A

Equations

• t.toSb = Expr.snoc Expr.bvar t

Decision procedure

theorem Expr.snoc_comp_wk_zero_subst {χ : Type u_1} (σ : ℕ → Expr χ) : snoc (comp σ wk) (subst σ (bvar 0)) = σ

theorem Expr.ofRen_comp (χ : Type u_2) (ξ₁ ξ₂ : ℕ → ℕ) : ofRen χ (ξ₁ ∘ ξ₂) = comp (ofRen χ ξ₁) (ofRen χ ξ₂)

@[simp]

theorem Expr.wk_app (χ : Type u_2) (n : ℕ) : wk n = bvar (n + 1)

def Expr.tacticAutosubst : Lean.ParserDescr

Decides equality of substitutions applied to expressions.

Equations

• Expr.tacticAutosubst = Lean.ParserDescr.node `Expr.tacticAutosubst 1024 (Lean.ParserDescr.nonReservedSymbol "autosubst" false)

def Expr.«termAutosubst%_» : Lean.ParserDescr

Use a term modulo autosubst conversion.

Equations

• Expr.«termAutosubst%_» = Lean.ParserDescr.node `Expr.«termAutosubst%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "autosubst% ") (Lean.ParserDescr.cat `term 0))

Lemmas that come up in a few proofs

theorem Expr.subst_toSb_subst {χ : Type u_1} (B a : Expr χ) (σ : ℕ → Expr χ) : subst σ (subst a.toSb B) = subst (subst σ a).toSb (subst (up σ) B)

theorem Expr.subst_snoc_toSb_subst {χ : Type u_1} (B a b : Expr χ) (σ : ℕ → Expr χ) : subst σ (subst (snoc a.toSb b) B) = subst (snoc (subst σ a).toSb (subst σ b)) (subst (up (up σ)) B)

Closed expressions

def Expr.isClosed {χ : Type u_1} (k : ℕ := 0) : Expr χ → Bool

The expression uses only indices up to k.

Equations

• Expr.isClosed k (Expr.univ l) = true
• Expr.isClosed k (Expr.ax c A) = Expr.isClosed k A
• Expr.isClosed k (Expr.bvar i) = decide (i < k)
• Expr.isClosed k (Expr.refl l t) = Expr.isClosed k t
• Expr.isClosed k t.el = Expr.isClosed k t
• Expr.isClosed k t.code = Expr.isClosed k t
• Expr.isClosed k (Expr.pi l l' t b) = (Expr.isClosed k t && Expr.isClosed (k + 1) b)
• Expr.isClosed k (Expr.sigma l l' t b) = (Expr.isClosed k t && Expr.isClosed (k + 1) b)
• Expr.isClosed k (Expr.lam l l' t b) = (Expr.isClosed k t && Expr.isClosed (k + 1) b)
• Expr.isClosed k (Expr.app l l' b t u) = (Expr.isClosed (k + 1) b && Expr.isClosed k t && Expr.isClosed k u)
• Expr.isClosed k (Expr.pair l l' b t u) = (Expr.isClosed (k + 1) b && Expr.isClosed k t && Expr.isClosed k u)
• Expr.isClosed k (Expr.fst l l' t b u) = (Expr.isClosed (k + 1) b && Expr.isClosed k t && Expr.isClosed k u)
• Expr.isClosed k (Expr.snd l l' t b u) = (Expr.isClosed (k + 1) b && Expr.isClosed k t && Expr.isClosed k u)
• Expr.isClosed k (Expr.Id l A t u) = (Expr.isClosed k A && Expr.isClosed k t && Expr.isClosed k u)
• Expr.isClosed k (Expr.idRec l l' t M r u h) = (Expr.isClosed k t && Expr.isClosed (k + 2) M && Expr.isClosed k r && Expr.isClosed k u && Expr.isClosed k h)

def Expr.SbIsBvar {χ : Type u_1} (σ : ℕ → Expr χ) (n : ℕ) : Prop

The substitution acts via identity on indices strictly below n.

Equations

• Expr.SbIsBvar σ n = ∀ ⦃i : ℕ⦄, i < n → σ i = Expr.bvar i

theorem Expr.SbIsBvar.up {χ : Type u_1} {σ : ℕ → Expr χ} {n : ℕ} : SbIsBvar σ n → SbIsBvar (Expr.up σ) (n + 1)

theorem Expr.SbIsBvar.zero {χ : Type u_1} (σ : ℕ → Expr χ) : SbIsBvar σ 0

theorem Expr.subst_of_isClosed' {χ : Type u_1} {e : Expr χ} {k : ℕ} {σ : ℕ → Expr χ} : isClosed k e = true → SbIsBvar σ k → subst σ e = e

theorem Expr.subst_of_isClosed {χ : Type u_1} {e : Expr χ} (σ : ℕ → Expr χ) : isClosed 0 e = true → subst σ e = e