In this module we compute the action of substitutions.

Lifting/weakening

Write ↑ⁿ for the n-fold weakening substitution {n+i/i}. Write σ:k for σ.vₖ₋₁.….v₁.v₀.

The thinning substitution ↑ⁿ⁺ᵏ:k, i.e., {0/0,…,k-1/k-1, k+n/k,k+1+n/k+1,…}, arises by starting with ↑ⁿ and traversing under k binders: for example, (ΠA. B)[↑¹] ≡ ΠA[↑¹]. B[↑².v₀] ≡ ΠA[↑¹]. B[↑¹⁺¹:1]. Applying ↑ⁿ⁺ᵏ:k moves an expression into a context with n new binders inserted at index k: Γ.Bₙ.….B₁.Aₖ₋₁[↑ⁿ].….A₀[⋯] ⊢ ↑ⁿ⁺ᵏ:k : Γ.Aₖ₋₁.….A₀. (With k = 0, the codomain is just Γ.)

def liftVar (n i : Nat) (k : Nat := 0) : Nat

Substitute ↑ⁿ⁺ᵏ:k in the de Bruijn index i.

Equations

• liftVar n i k = if i < k then i else n + i

def Expr.liftN (n : Nat) : Expr → (k : optParam Nat 0) → Expr

Substitute ↑ⁿ⁺ᵏ:k in an expression.

Equations

• Expr.liftN n (Expr.bvar i) x✝ = Expr.bvar (liftVar n i x✝)
• Expr.liftN n (Expr.pi l l' A B) x✝ = Expr.pi l l' (Expr.liftN n A x✝) (Expr.liftN n B (x✝ + 1))
• Expr.liftN n (Expr.lam l l' A t) x✝ = Expr.lam l l' (Expr.liftN n A x✝) (Expr.liftN n t (x✝ + 1))
• Expr.liftN n (Expr.app l l' B fn arg) x✝ = Expr.app l l' (Expr.liftN n B (x✝ + 1)) (Expr.liftN n fn x✝) (Expr.liftN n arg x✝)
• Expr.liftN n (Expr.univ l) x✝ = Expr.univ l
• Expr.liftN n a.el x✝ = (Expr.liftN n a x✝).el
• Expr.liftN n A.code x✝ = (Expr.liftN n A x✝).code

@[reducible, inline]

abbrev Expr.lift : Expr → Expr

Substitute ↑¹ in an expression.

Equations

• a✝.lift = Expr.liftN 1 a✝

Instantiation

The substitution ↑ᵏ.e[↑ᵏ]:k, i.e., {0/0,…,k-1/k-1, e[↑ᵏ]/k, k/k+1,k+2/k+3,…}, arises by starting with id.e and traversing under k binders: for example (ΠA. B)[id.e] ≡ ΠA[id.e]. B[↑.e[↑].v₀] ≡ ΠA[id.e]. B[↑¹.e[↑¹]:1]. Applying ↑ᵏ.e[↑ᵏ]:k moves an expression t into a context with the kth binder removed: Γ.Aₖ₋₁[id.e].….A₀[⋯] ⊢ ↑ᵏ.e[↑ᵏ]:k : Γ.B.Aₖ₋₁.….A₀.

The substitution id.e is used in β-reduction: (λa) b ↝ a[id.b].

def instVar (i : Nat) (e : Expr) (k : Nat := 0) : Expr

Substitute ↑ᵏ.e[↑ᵏ]:k in the de Bruijn index i.

Equations

• instVar i e k = if i < k then Expr.bvar i else if i = k then Expr.liftN k e else Expr.bvar (i - 1)

def Expr.inst : Expr → Expr → (k : optParam Nat 0) → Expr

Substitute ↑ᵏ.e[↑ᵏ]:k in an expression.

Equations

• (Expr.bvar i).inst x✝¹ x✝ = instVar i x✝¹ x✝
• (Expr.pi l l' A B).inst x✝¹ x✝ = Expr.pi l l' (A.inst x✝¹ x✝) (B.inst x✝¹ (x✝ + 1))
• (Expr.lam l l' A t).inst x✝¹ x✝ = Expr.lam l l' (A.inst x✝¹ x✝) (t.inst x✝¹ (x✝ + 1))
• (Expr.app l l' B fn arg).inst x✝¹ x✝ = Expr.app l l' (B.inst x✝¹ (x✝ + 1)) (fn.inst x✝¹ x✝) (arg.inst x✝¹ x✝)
• (Expr.univ l).inst x✝¹ x✝ = Expr.univ l
• a.el.inst x✝¹ x✝ = (a.inst x✝¹ x✝).el
• A.code.inst x✝¹ x✝ = (A.inst x✝¹ x✝).code

Lemmas

@[simp]

theorem liftVar_zero (i k : Nat) : liftVar 0 i k = i

@[simp]

theorem liftVar_zero' (n i : Nat) : liftVar n i = n + i

@[simp]

theorem Expr.lift_zero (t : Expr) (k : Nat) : liftN 0 t k = t