module plfa.part2.Substitution where

Introduction

The primary purpose of this chapter is to prove that substitution commutes with itself. Barendregt (1984) refers to this as the substitution lemma:

M [x:=N] [y:=L] = M [y:=L] [x:= N[y:=L] ]

In our setting, with de Bruijn indices for variables, the statement of the lemma becomes:

M [ N ] [ L ] ≑  Mγ€” L 〕[ N [ L ] ]                     (substitution)

where the notation M γ€” L 〕 is for substituting L for index 1 inside M. In addition, because we define substitution in terms of parallel substitution, we have the following generalization, replacing the substitution of L with an arbitrary parallel substitution Οƒ.

subst Οƒ (M [ N ]) ≑ (subst (exts Οƒ) M) [ subst Οƒ N ]    (subst-commute)

The special case for renamings is also useful.

rename ρ (M [ N ]) ≑ (rename (ext ρ) M) [ rename ρ N ]
                                                 (rename-subst-commute)

The secondary purpose of this chapter is to define the Οƒ algebra of parallel substitution due to Abadi, Cardelli, Curien, and Levy (1991). The equations of this algebra not only help us prove the substitution lemma, but they are generally useful. Furthermore, when the equations are applied from left to right, they form a rewrite system that decides whether any two substitutions are equal.

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≑_; refl; sym; cong; congβ‚‚; cong-app)
open Eq.≑-Reasoning using (begin_; step-≑-∣; step-≑-⟩; _∎)
open import Function.Base using (_∘_)
open import plfa.part2.Untyped
     using (Type; Context; _⊒_; β˜…; _βˆ‹_; βˆ…; _,_; Z; S_; `_; Ζ›_; _Β·_;
            rename; subst; ext; exts; _[_]; subst-zero)

postulate
  extensionality : βˆ€ {A B : Set} {f g : A β†’ B}
    β†’ (βˆ€ (x : A) β†’ f x ≑ g x)
      -----------------------
    β†’ f ≑ g

Notation

We introduce the following shorthand for the type of a renaming from variables in context Ξ“ to variables in context Ξ”.

Rename : Context β†’ Context β†’ Set
Rename Ξ“ Ξ” = βˆ€{A} β†’ Ξ“ βˆ‹ A β†’ Ξ” βˆ‹ A

Similarly, we introduce the following shorthand for the type of a substitution from variables in context Ξ“ to terms in context Ξ”.

Subst : Context β†’ Context β†’ Set
Subst Ξ“ Ξ” = βˆ€{A} β†’ Ξ“ βˆ‹ A β†’ Ξ” ⊒ A

We use the following more succinct notation for the subst function.

βŸͺ_⟫ : βˆ€{Ξ“ Ξ” A} β†’ Subst Ξ“ Ξ” β†’ Ξ“ ⊒ A β†’ Ξ” ⊒ A
βŸͺ Οƒ ⟫ = Ξ» M β†’ subst Οƒ M

The Οƒ algebra of substitution

A substitution maps de Bruijn indices (natural numbers) to terms, so we can view a substitution simply as a sequence of terms, or more precisely, as an infinite sequence of terms. The Οƒ algebra consists of four operations for building such sequences: identity ids, shift ↑, cons M β€’ Οƒ, and sequencing Οƒ ⨟ Ο„. The sequence 0, 1, 2, ... is constructed by the identity substitution.

ids : βˆ€{Ξ“} β†’ Subst Ξ“ Ξ“
ids x = ` x

The shift operation ↑ constructs the sequence

1, 2, 3, ...

and is defined as follows.

↑ : βˆ€{Ξ“ A} β†’ Subst Ξ“ (Ξ“ , A)
↑ x = ` (S x)

Given a term M and substitution Οƒ, the operation M β€’ Οƒ constructs the sequence

M , Οƒ 0, Οƒ 1, Οƒ 2, ...

This operation is analogous to the cons operation of Lisp.

infixr 6 _β€’_

_β€’_ : βˆ€{Ξ“ Ξ” A} β†’ (Ξ” ⊒ A) β†’ Subst Ξ“ Ξ” β†’ Subst (Ξ“ , A) Ξ”
(M β€’ Οƒ) Z = M
(M β€’ Οƒ) (S x) = Οƒ x

Given two substitutions Οƒ and Ο„, the sequencing operation Οƒ ⨟ Ο„ composes the two substitutions by first applying Οƒ and then applying Ο„. So it produces the sequence

βŸͺΟ„βŸ«(Οƒ 0), βŸͺΟ„βŸ«(Οƒ 1), βŸͺΟ„βŸ«(Οƒ 2), ...

Here is the definition.

infixr 5 _⨟_

_⨟_ : βˆ€{Ξ“ Ξ” Ξ£} β†’ Subst Ξ“ Ξ” β†’ Subst Ξ” Ξ£ β†’ Subst Ξ“ Ξ£
Οƒ ⨟ Ο„ = βŸͺ Ο„ ⟫ ∘ Οƒ

For the sequencing operation, Abadi et al. use the notation of function composition, writing Οƒ ∘ Ο„, but still with Οƒ applied before Ο„, which is the opposite of standard mathematical practice. We instead write Οƒ ⨟ Ο„, because semicolon is the standard notation for forward function composition.

The Οƒ algebra equations

The Οƒ algebra includes the following equations.

(sub-head)  βŸͺ M β€’ Οƒ ⟫ (` Z) ≑ M
(sub-tail)  ↑ ⨟ (M β€’ Οƒ)    ≑ Οƒ
(sub-Ξ·)     (βŸͺ Οƒ ⟫ (` Z)) β€’ (↑ ⨟ Οƒ) ≑ Οƒ
(Z-shift)   (` Z) β€’ ↑      ≑ ids

(sub-id)    βŸͺ ids ⟫ M      ≑ M
(sub-app)   βŸͺ Οƒ ⟫ (L Β· M)  ≑ (βŸͺ Οƒ ⟫ L) Β· (βŸͺ Οƒ ⟫ M)
(sub-abs)   βŸͺ Οƒ ⟫ (Ζ› N) ≑ Ζ› βŸͺ (` Z) β€’ (Οƒ ⨟ ↑) ⟫ N
(sub-sub)   βŸͺ Ο„ ⟫ βŸͺ Οƒ ⟫ M  ≑ βŸͺ Οƒ ⨟ Ο„ ⟫ M

(sub-idL)   ids ⨟ Οƒ        ≑ Οƒ
(sub-idR)   Οƒ ⨟ ids        ≑ Οƒ
(sub-assoc) (Οƒ ⨟ Ο„) ⨟ ΞΈ    ≑ Οƒ ⨟ (Ο„ ⨟ ΞΈ)
(sub-dist)  (M β€’ Οƒ) ⨟ Ο„    ≑ (βŸͺ Ο„ ⟫ M) β€’ (Οƒ ⨟ Ο„)

The first group of equations describe how the β€’ operator acts like cons. The equation sub-head says that the variable zero Z returns the head of the sequence (it acts like the car of Lisp). Similarly, sub-tail says that sequencing with shift ↑ returns the tail of the sequence (it acts like cdr of Lisp). The sub-Ξ· equation is the Ξ·-expansion rule for sequences, saying that taking the head and tail of a sequence, and then cons’ing them together yields the original sequence. The Z-shift equation says that cons’ing zero onto the shifted sequence produces the identity sequence.

The next four equations involve applying substitutions to terms. The equation sub-id says that the identity substitution returns the term unchanged. The equations sub-app and sub-abs says that substitution is a congruence for the lambda calculus. The sub-sub equation says that the sequence operator ⨟ behaves as intended.

The last four equations concern the sequencing of substitutions. The first two equations, sub-idL and sub-idR, say that ids is the left and right unit of the sequencing operator. The sub-assoc equation says that sequencing is associative. Finally, sub-dist says that post-sequencing distributes through cons.

Relating the Οƒ algebra and substitution functions

The definitions of substitution N [ M ] and parallel substitution subst Οƒ N depend on several auxiliary functions: rename, exts, ext, and subst-zero. We shall relate those functions to terms in the Οƒ algebra.

To begin with, renaming can be expressed in terms of substitution. We have

rename ρ M ≑ βŸͺ ren ρ ⟫ M               (rename-subst-ren)

where ren turns a renaming ρ into a substitution by post-composing ρ with the identity substitution.

ren : βˆ€{Ξ“ Ξ”} β†’ Rename Ξ“ Ξ” β†’ Subst Ξ“ Ξ”
ren ρ = ids ∘ ρ

When the renaming is the increment function, then it is equivalent to shift.

ren S_ ≑ ↑                             (ren-shift)

rename S_ M ≑ βŸͺ ↑ ⟫ M                  (rename-shift)

Renaming with the identity renaming leaves the term unchanged.

rename (Ξ» {A} x β†’ x) M ≑ M             (rename-id)

Next we relate the exts function to the Οƒ algebra. Recall that the exts function extends a substitution as follows:

exts Οƒ = ` Z, rename S_ (Οƒ 0), rename S_ (Οƒ 1), rename S_ (Οƒ 2), ...

So exts is equivalent to cons’ing Z onto the sequence formed by applying Οƒ and then shifting.

exts Οƒ ≑ ` Z β€’ (Οƒ ⨟ ↑)                (exts-cons-shift)

The ext function does the same job as exts but for renamings instead of substitutions. So composing ext with ren is the same as composing ren with exts.

ren (ext ρ) ≑ exts (ren ρ)            (ren-ext)

Thus, we can recast the exts-cons-shift equation in terms of renamings.

ren (ext ρ) ≑ ` Z β€’ (ren ρ ⨟ ↑)       (ext-cons-Z-shift)

It is also useful to specialize the sub-sub equation of the Οƒ algebra to the situation where the first substitution is a renaming.

βŸͺ Οƒ ⟫ (rename ρ M) ≑ βŸͺ Οƒ ∘ ρ ⟫ M       (rename-subst)

The subst-zero M substitution is equivalent to cons’ing M onto the identity substitution.

subst-zero M ≑ M β€’ ids                (subst-Z-cons-ids)

Finally, sequencing exts Οƒ with subst-zero M is equivalent to cons’ing M onto Οƒ.

exts Οƒ ⨟ subst-zero M ≑ (M β€’ Οƒ)       (subst-zero-exts-cons)

Proofs of sub-head, sub-tail, sub-Ξ·, Z-shift, sub-idL, sub-dist, and sub-app

We start with the proofs that are immediate from the definitions of the operators.

sub-head : βˆ€ {Ξ“ Ξ”} {A} {M : Ξ” ⊒ A}{Οƒ : Subst Ξ“ Ξ”}
         β†’ βŸͺ M β€’ Οƒ ⟫ (` Z) ≑ M
sub-head = refl

sub-tail : βˆ€{Ξ“ Ξ”} {A B} {M : Ξ” ⊒ A} {Οƒ : Subst Ξ“ Ξ”}
         β†’ (↑ ⨟ M β€’ Οƒ) {A = B} ≑ Οƒ
sub-tail = extensionality Ξ» x β†’ refl

sub-Ξ· : βˆ€{Ξ“ Ξ”} {A B} {Οƒ : Subst (Ξ“ , A) Ξ”}
      β†’ (βŸͺ Οƒ ⟫ (` Z) β€’ (↑ ⨟ Οƒ)) {A = B} ≑ Οƒ
sub-Ξ· {Ξ“}{Ξ”}{A}{B}{Οƒ} = extensionality Ξ» x β†’ lemma
   where
   lemma : βˆ€ {x} β†’ ((βŸͺ Οƒ ⟫ (` Z)) β€’ (↑ ⨟ Οƒ)) x ≑ Οƒ x
   lemma {x = Z} = refl
   lemma {x = S x} = refl

Z-shift : βˆ€{Ξ“}{A B}
        β†’ ((` Z) β€’ ↑) ≑ ids {Ξ“ , A} {B}
Z-shift {Ξ“}{A}{B} = extensionality lemma
   where
   lemma : (x : Ξ“ , A βˆ‹ B) β†’ ((` Z) β€’ ↑) x ≑ ids x
   lemma Z = refl
   lemma (S y) = refl

sub-idL : βˆ€{Ξ“ Ξ”} {Οƒ : Subst Ξ“ Ξ”} {A}
       β†’ ids ⨟ Οƒ ≑ Οƒ {A}
sub-idL = extensionality Ξ» x β†’ refl

sub-dist :  βˆ€{Ξ“ Ξ” Ξ£ : Context} {A B} {Οƒ : Subst Ξ“ Ξ”} {Ο„ : Subst Ξ” Ξ£}
              {M : Ξ” ⊒ A}
         β†’ ((M β€’ Οƒ) ⨟ Ο„) ≑ ((subst Ο„ M) β€’ (Οƒ ⨟ Ο„)) {B}
sub-dist {Ξ“}{Ξ”}{Ξ£}{A}{B}{Οƒ}{Ο„}{M} = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€ {x : Ξ“ , A βˆ‹ B} β†’ ((M β€’ Οƒ) ⨟ Ο„) x ≑ ((subst Ο„ M) β€’ (Οƒ ⨟ Ο„)) x
  lemma {x = Z} = refl
  lemma {x = S x} = refl

sub-app : βˆ€{Ξ“ Ξ”} {Οƒ : Subst Ξ“ Ξ”} {L : Ξ“ ⊒ β˜…}{M : Ξ“ ⊒ β˜…}
        β†’ βŸͺ Οƒ ⟫ (L Β· M)  ≑ (βŸͺ Οƒ ⟫ L) Β· (βŸͺ Οƒ ⟫ M)
sub-app = refl

Interlude: congruences

In this section we establish congruence rules for the Οƒ algebra operators β€’ and ⨟ and for subst and its helper functions ext, rename, exts, and subst-zero. These congruence rules help with the equational reasoning in the later sections of this chapter.

cong-ext : βˆ€{Ξ“ Ξ”}{ρ ρ′ : Rename Ξ“ Ξ”}{B}
   β†’ (βˆ€{A} β†’ ρ ≑ ρ′ {A})
     ---------------------------------
   β†’ βˆ€{A} β†’ ext ρ {B = B} ≑ ext ρ′ {A}
cong-ext{Ξ“}{Ξ”}{ρ}{ρ′}{B} rr {A} = extensionality Ξ» x β†’ lemma {x}
  where
  lemma : βˆ€{x : Ξ“ , B βˆ‹ A} β†’ ext ρ x ≑ ext ρ′ x
  lemma {Z} = refl
  lemma {S y} = cong S_ (cong-app rr y)

cong-rename : βˆ€{Ξ“ Ξ”}{ρ ρ′ : Rename Ξ“ Ξ”}{B}{M : Ξ“ ⊒ B}
        β†’ (βˆ€{A} β†’ ρ ≑ ρ′ {A})
          ------------------------
        β†’ rename ρ M ≑ rename ρ′ M
cong-rename {M = ` x} rr = cong `_ (cong-app rr x)
cong-rename {ρ = ρ} {ρ′ = ρ′} {M = Ζ› N} rr =
   cong Ζ›_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr))
cong-rename {M = L Β· M} rr =
   congβ‚‚ _Β·_ (cong-rename rr) (cong-rename rr)

cong-exts : βˆ€{Ξ“ Ξ”}{Οƒ Οƒβ€² : Subst Ξ“ Ξ”}{B}
   β†’ (βˆ€{A} β†’ Οƒ ≑ Οƒβ€² {A})
     -----------------------------------
   β†’ βˆ€{A} β†’ exts Οƒ {B = B} ≑ exts Οƒβ€² {A}
cong-exts{Ξ“}{Ξ”}{Οƒ}{Οƒβ€²}{B} ss {A} = extensionality Ξ» x β†’ lemma {x}
   where
   lemma : βˆ€{x} β†’ exts Οƒ x ≑ exts Οƒβ€² x
   lemma {Z} = refl
   lemma {S x} = cong (rename S_) (cong-app (ss {A}) x)

cong-sub : βˆ€{Ξ“ Ξ”}{Οƒ Οƒβ€² : Subst Ξ“ Ξ”}{A}{M Mβ€² : Ξ“ ⊒ A}
            β†’ (βˆ€{A} β†’ Οƒ ≑ Οƒβ€² {A})  β†’  M ≑ Mβ€²
              ------------------------------
            β†’ subst Οƒ M ≑ subst Οƒβ€² Mβ€²
cong-sub {Ξ“} {Ξ”} {Οƒ} {Οƒβ€²} {A} {` x} ss refl = cong-app ss x
cong-sub {Ξ“} {Ξ”} {Οƒ} {Οƒβ€²} {A} {Ζ› M} ss refl =
   cong Ζ›_ (cong-sub {Οƒ = exts Οƒ}{Οƒβ€² = exts Οƒβ€²} {M = M} (cong-exts ss) refl)
cong-sub {Ξ“} {Ξ”} {Οƒ} {Οƒβ€²} {A} {L Β· M} ss refl =
   congβ‚‚ _Β·_ (cong-sub {M = L} ss refl) (cong-sub {M = M} ss refl)

cong-sub-zero : βˆ€{Ξ“}{B : Type}{M Mβ€² : Ξ“ ⊒ B}
  β†’ M ≑ Mβ€²
    -----------------------------------------
  β†’ βˆ€{A} β†’ subst-zero M ≑ (subst-zero Mβ€²) {A}
cong-sub-zero {Ξ“}{B}{M}{Mβ€²} mm' {A} =
   extensionality Ξ» x β†’ cong (Ξ» z β†’ subst-zero z x) mm'

cong-cons : βˆ€{Ξ“ Ξ”}{A}{M N : Ξ” ⊒ A}{Οƒ Ο„ : Subst Ξ“ Ξ”}
  β†’ M ≑ N  β†’  (βˆ€{A} β†’ Οƒ {A} ≑ Ο„ {A})
    --------------------------------
  β†’ βˆ€{A} β†’ (M β€’ Οƒ) {A} ≑ (N β€’ Ο„) {A}
cong-cons{Ξ“}{Ξ”}{A}{M}{N}{Οƒ}{Ο„} refl st {Aβ€²} = extensionality lemma
  where
  lemma : (x : Ξ“ , A βˆ‹ Aβ€²) β†’ (M β€’ Οƒ) x ≑ (M β€’ Ο„) x
  lemma Z = refl
  lemma (S x) = cong-app st x

cong-seq : βˆ€{Ξ“ Ξ” Ξ£}{Οƒ Οƒβ€² : Subst Ξ“ Ξ”}{Ο„ Ο„β€² : Subst Ξ” Ξ£}
  β†’ (βˆ€{A} β†’ Οƒ {A} ≑ Οƒβ€² {A}) β†’ (βˆ€{A} β†’ Ο„ {A} ≑ Ο„β€² {A})
  β†’ βˆ€{A} β†’ (Οƒ ⨟ Ο„) {A} ≑ (Οƒβ€² ⨟ Ο„β€²) {A}
cong-seq {Ξ“}{Ξ”}{Ξ£}{Οƒ}{Οƒβ€²}{Ο„}{Ο„β€²} ss' tt' {A} = extensionality lemma
  where
  lemma : (x : Ξ“ βˆ‹ A) β†’ (Οƒ ⨟ Ο„) x ≑ (Οƒβ€² ⨟ Ο„β€²) x
  lemma x =
     begin
       (Οƒ ⨟ Ο„) x
     β‰‘βŸ¨βŸ©
       subst Ο„ (Οƒ x)
     β‰‘βŸ¨ cong (subst Ο„) (cong-app ss' x) ⟩
       subst Ο„ (Οƒβ€² x)
     β‰‘βŸ¨ cong-sub{M = Οƒβ€² x} tt' refl ⟩
       subst Ο„β€² (Οƒβ€² x)
     β‰‘βŸ¨βŸ©
       (Οƒβ€² ⨟ Ο„β€²) x
     ∎

Relating rename, exts, ext, and subst-zero to the Οƒ algebra

In this section we establish equations that relate subst and its helper functions (rename, exts, ext, and subst-zero) to terms in the Οƒ algebra.

The first equation we prove is

rename ρ M ≑ βŸͺ ren ρ ⟫ M              (rename-subst-ren)

Because subst uses the exts function, we need the following lemma which says that exts and ext do the same thing except that ext works on renamings and exts works on substitutions.

ren-ext : βˆ€ {Ξ“ Ξ”}{B C : Type} {ρ : Rename Ξ“ Ξ”}
        β†’ ren (ext ρ {B = B}) ≑ exts (ren ρ) {C}
ren-ext {Ξ“}{Ξ”}{B}{C}{ρ} = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€ {x : Ξ“ , B βˆ‹ C} β†’ (ren (ext ρ)) x ≑ exts (ren ρ) x
  lemma {x = Z} = refl
  lemma {x = S x} = refl

With this lemma in hand, the proof is a straightforward induction on the term M.

rename-subst-ren : βˆ€ {Ξ“ Ξ”}{A} {ρ : Rename Ξ“ Ξ”}{M : Ξ“ ⊒ A}
                 β†’ rename ρ M ≑ βŸͺ ren ρ ⟫ M
rename-subst-ren {M = ` x} = refl
rename-subst-ren {ρ = ρ}{M = Ζ› N} =
  begin
      rename ρ (Ζ› N)
    β‰‘βŸ¨βŸ©
      Ζ› rename (ext ρ) N
    β‰‘βŸ¨ cong Ζ›_ (rename-subst-ren {ρ = ext ρ}{M = N}) ⟩
      Ζ› βŸͺ ren (ext ρ) ⟫ N
    β‰‘βŸ¨ cong Ζ›_ (cong-sub {M = N} ren-ext refl) ⟩
      Ζ› βŸͺ exts (ren ρ) ⟫  N
    β‰‘βŸ¨βŸ©
      βŸͺ ren ρ ⟫ (Ζ› N)
  ∎
rename-subst-ren {M = L Β· M} = congβ‚‚ _Β·_ rename-subst-ren rename-subst-ren

The substitution ren S_ is equivalent to ↑.

ren-shift : βˆ€{Ξ“}{A}{B}
          β†’ ren S_ ≑ ↑ {A = B} {A}
ren-shift {Ξ“}{A}{B} = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€ {x : Ξ“ βˆ‹ A} β†’ ren (S_{B = B}) x ≑ ↑ {A = B} x
  lemma {x = Z} = refl
  lemma {x = S x} = refl

The substitution rename S_ M is equivalent to shifting: βŸͺ ↑ ⟫ M.

rename-shift : βˆ€{Ξ“} {A} {B} {M : Ξ“ ⊒ A}
             β†’ rename (S_{B = B}) M ≑ βŸͺ ↑ ⟫ M
rename-shift{Ξ“}{A}{B}{M} =
  begin
    rename S_ M
  β‰‘βŸ¨ rename-subst-ren ⟩
    βŸͺ ren S_ ⟫ M
  β‰‘βŸ¨ cong-sub{M = M} ren-shift refl ⟩
    βŸͺ ↑ ⟫ M
  ∎

Next we prove the equation exts-cons-shift, which states that exts is equivalent to cons’ing Z onto the sequence formed by applying Οƒ and then shifting. The proof is by case analysis on the variable x, using rename-subst-ren for when x = S y.

exts-cons-shift : βˆ€{Ξ“ Ξ”} {A B} {Οƒ : Subst Ξ“ Ξ”}
                β†’ exts Οƒ {A} {B} ≑ (` Z β€’ (Οƒ ⨟ ↑))
exts-cons-shift = extensionality Ξ» x β†’ lemma{x = x}
  where
  lemma : βˆ€{Ξ“ Ξ”} {A B} {Οƒ : Subst Ξ“ Ξ”} {x : Ξ“ , B βˆ‹ A}
                  β†’ exts Οƒ x ≑ (` Z β€’ (Οƒ ⨟ ↑)) x
  lemma {x = Z} = refl
  lemma {x = S y} = rename-subst-ren

As a corollary, we have a similar correspondence for ren (ext ρ).

ext-cons-Z-shift : βˆ€{Ξ“ Ξ”} {ρ : Rename Ξ“ Ξ”}{A}{B}
                 β†’ ren (ext ρ {B = B}) ≑ (` Z β€’ (ren ρ ⨟ ↑)) {A}
ext-cons-Z-shift {Ξ“}{Ξ”}{ρ}{A}{B} =
  begin
    ren (ext ρ)
  β‰‘βŸ¨ ren-ext ⟩
    exts (ren ρ)
  β‰‘βŸ¨ exts-cons-shift{Οƒ = ren ρ} ⟩
   ((` Z) β€’ (ren ρ ⨟ ↑))
  ∎

Finally, the subst-zero M substitution is equivalent to cons’ing M onto the identity substitution.

subst-Z-cons-ids : βˆ€{Ξ“}{A B : Type}{M : Ξ“ ⊒ B}
                 β†’ subst-zero M ≑ (M β€’ ids) {A}
subst-Z-cons-ids = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€{Ξ“}{A B : Type}{M : Ξ“ ⊒ B}{x : Ξ“ , B βˆ‹ A}
                      β†’ subst-zero M x ≑ (M β€’ ids) x
  lemma {x = Z} = refl
  lemma {x = S x} = refl

Proofs of sub-abs, sub-id, and rename-id

The equation sub-abs follows immediately from the equation exts-cons-shift.

sub-abs : βˆ€{Ξ“ Ξ”} {Οƒ : Subst Ξ“ Ξ”} {N : Ξ“ , β˜… ⊒ β˜…}
        β†’ βŸͺ Οƒ ⟫ (Ζ› N) ≑ Ζ› βŸͺ (` Z) β€’ (Οƒ ⨟ ↑) ⟫ N
sub-abs {Οƒ = Οƒ}{N = N} =
   begin
     βŸͺ Οƒ ⟫ (Ζ› N)
   β‰‘βŸ¨βŸ©
     Ζ› βŸͺ exts Οƒ ⟫ N
   β‰‘βŸ¨ cong Ζ›_ (cong-sub{M = N} exts-cons-shift refl) ⟩
     Ζ› βŸͺ (` Z) β€’ (Οƒ ⨟ ↑) ⟫ N
   ∎

The proof of sub-id requires the following lemma which says that extending the identity substitution produces the identity substitution.

exts-ids : βˆ€{Ξ“}{A B}
         β†’ exts ids ≑ ids {Ξ“ , B} {A}
exts-ids {Ξ“}{A}{B} = extensionality lemma
  where lemma : (x : Ξ“ , B βˆ‹ A) β†’ exts ids x ≑ ids x
        lemma Z = refl
        lemma (S x) = refl

The proof of βŸͺ ids ⟫ M ≑ M now follows easily by induction on M, using exts-ids in the case for M ≑ Ζ› N.

sub-id : βˆ€{Ξ“} {A} {M : Ξ“ ⊒ A}
         β†’ βŸͺ ids ⟫ M ≑ M
sub-id {M = ` x} = refl
sub-id {M = Ζ› N} =
   begin
     βŸͺ ids ⟫ (Ζ› N)
   β‰‘βŸ¨βŸ©
     Ζ› βŸͺ exts ids ⟫ N
   β‰‘βŸ¨ cong Ζ›_ (cong-sub{M = N} exts-ids refl)  ⟩
     Ζ› βŸͺ ids ⟫ N
   β‰‘βŸ¨ cong Ζ›_ sub-id ⟩
     Ζ› N
   ∎
sub-id {M = L Β· M} = congβ‚‚ _Β·_ sub-id sub-id

The rename-id equation is a corollary is sub-id.

rename-id : βˆ€ {Ξ“}{A} {M : Ξ“ ⊒ A}
  β†’ rename (Ξ» {A} x β†’ x) M ≑ M
rename-id {M = M} =
   begin
     rename (Ξ» {A} x β†’ x) M
   β‰‘βŸ¨ rename-subst-ren  ⟩
     βŸͺ ren (Ξ» {A} x β†’ x) ⟫ M
   β‰‘βŸ¨βŸ©
     βŸͺ ids ⟫ M
   β‰‘βŸ¨ sub-id  ⟩
     M
   ∎

Proof of sub-idR

The proof of sub-idR follows directly from sub-id.

sub-idR : βˆ€{Ξ“ Ξ”} {Οƒ : Subst Ξ“ Ξ”} {A}
       β†’ (Οƒ ⨟ ids) ≑ Οƒ {A}
sub-idR {Ξ“}{Οƒ = Οƒ}{A} =
          begin
            Οƒ ⨟ ids
          β‰‘βŸ¨βŸ©
            βŸͺ ids ⟫ ∘ Οƒ
          β‰‘βŸ¨ extensionality (Ξ» x β†’ sub-id) ⟩
            Οƒ
          ∎

Proof of sub-sub

The sub-sub equation states that sequenced substitutions Οƒ ⨟ Ο„ are equivalent to first applying Οƒ then applying Ο„.

βŸͺ Ο„ ⟫ βŸͺ Οƒ ⟫ M  ≑ βŸͺ Οƒ ⨟ Ο„ ⟫ M

The proof requires several lemmas. First, we need to prove the specialization for renaming.

rename ρ (rename ρ′ M) ≑ rename (ρ ∘ ρ′) M

This in turn requires the following lemma about ext.

compose-ext : βˆ€{Ξ“ Ξ” Ξ£}{ρ : Rename Ξ” Ξ£} {ρ′ : Rename Ξ“ Ξ”} {A B}
            β†’ ((ext ρ) ∘ (ext ρ′)) ≑ ext (ρ ∘ ρ′) {B} {A}
compose-ext = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€{Ξ“ Ξ” Ξ£}{ρ : Rename Ξ” Ξ£} {ρ′ : Rename Ξ“ Ξ”} {A B} {x : Ξ“ , B βˆ‹ A}
              β†’ ((ext ρ) ∘ (ext ρ′)) x ≑ ext (ρ ∘ ρ′) x
  lemma {x = Z} = refl
  lemma {x = S x} = refl

To prove that composing renamings is equivalent to applying one after the other using rename, we proceed by induction on the term M, using the compose-ext lemma in the case for M ≑ Ζ› N.

compose-rename : βˆ€{Ξ“ Ξ” Ξ£}{A}{M : Ξ“ ⊒ A}{ρ : Rename Ξ” Ξ£}{ρ′ : Rename Ξ“ Ξ”}
  β†’ rename ρ (rename ρ′ M) ≑ rename (ρ ∘ ρ′) M
compose-rename {M = ` x} = refl
compose-rename {Ξ“}{Ξ”}{Ξ£}{A}{Ζ› N}{ρ}{ρ′} = cong Ζ›_ G
  where
  G : rename (ext ρ) (rename (ext ρ′) N) ≑ rename (ext (ρ ∘ ρ′)) N
  G =
      begin
        rename (ext ρ) (rename (ext ρ′) N)
      β‰‘βŸ¨ compose-rename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩
        rename ((ext ρ) ∘ (ext ρ′)) N
      β‰‘βŸ¨ cong-rename compose-ext ⟩
        rename (ext (ρ ∘ ρ′)) N
      ∎
compose-rename {M = L Β· M} = congβ‚‚ _Β·_ compose-rename compose-rename

The next lemma states that if a renaming and substitution commute on variables, then they also commute on terms. We explain the proof in detail below.

commute-subst-rename : βˆ€{Ξ“ Ξ”}{M : Ξ“ ⊒ β˜…}{Οƒ : Subst Ξ“ Ξ”}
                        {ρ₁ : Rename Ξ“ (Ξ“ , β˜…)}{ρ₂ : Rename Ξ” (Ξ” , β˜…)}
                     β†’ (βˆ€{x : Ξ“ βˆ‹ β˜…} β†’ exts Οƒ (ρ₁ x) ≑ rename ρ₂ (Οƒ x))
                     β†’ subst (exts Οƒ) (rename ρ₁ M) ≑ rename ρ₂ (subst Οƒ M)
commute-subst-rename {M = ` x} H = H
commute-subst-rename {Ξ“}{Ξ”}{Ζ› N}{Οƒ}{ρ₁}{ρ₂} H =
   cong Ζ›_ (commute-subst-rename{Ξ“ , β˜…}{Ξ” , β˜…}{N}
               {exts Οƒ}{ext ρ₁}{ext ρ₂} (Ξ» {x} β†’ Hβ€² {x}))
   where
   Hβ€² : {x : Ξ“ , β˜… βˆ‹ β˜…} β†’ exts (exts Οƒ) (ext ρ₁ x) ≑ rename (ext ρ₂) (exts Οƒ x)
   Hβ€² {Z} = refl
   Hβ€² {S y} =
     begin
       exts (exts Οƒ) (ext ρ₁ (S y))
     β‰‘βŸ¨βŸ©
       rename S_ (exts Οƒ (ρ₁ y))
     β‰‘βŸ¨ cong (rename S_) H ⟩
       rename S_ (rename ρ₂ (Οƒ y))
     β‰‘βŸ¨ compose-rename ⟩
       rename (S_ ∘ ρ₂) (Οƒ y)
     β‰‘βŸ¨βŸ©
       rename ((ext ρ₂) ∘ S_) (Οƒ y)
     β‰‘βŸ¨ sym compose-rename ⟩
       rename (ext ρ₂) (rename S_ (Οƒ y))
     β‰‘βŸ¨βŸ©
       rename (ext ρ₂) (exts Οƒ (S y))
     ∎
commute-subst-rename {M = L Β· N} H =
  congβ‚‚ _Β·_ (commute-subst-rename{M = L} H)
            (commute-subst-rename{M = N} H)

The proof is by induction on the term M.

  • If M is a variable, then we use the premise to conclude.

  • If M ≑ Ζ› N, we conclude using the induction hypothesis for N. However, to use the induction hypothesis, we must show that

      exts (exts Οƒ) (ext ρ₁ x) ≑ rename (ext ρ₂) (exts Οƒ x)

    We prove this equation by cases on x.

    • If x = Z, the two sides are equal by definition.

    • If x = S y, we obtain the goal by the following equational reasoning.

        exts (exts Οƒ) (ext ρ₁ (S y))
≑ rename S_ (exts Οƒ (ρ₁ y))
≑ rename S_ (rename ρ₂ (Οƒ y))        (by the premise)
≑ rename (S_ ∘ ρ₂) (Οƒ y)             (by compose-rename)
≑ rename ((ext ρ₂) ∘ S_) (Οƒ y)
≑ rename (ext ρ₂) (rename S_ (Οƒ y))  (by compose-rename)
≑ rename (ext ρ₂) (exts Οƒ (S y))

  • If M is an application, we obtain the goal using the induction hypothesis for each subterm.

The last lemma needed to prove sub-sub states that the exts function distributes with sequencing. It is a corollary of commute-subst-rename as described below. (It would have been nicer to prove this directly by equational reasoning in the Οƒ algebra, but that would require the sub-assoc equation, whose proof depends on sub-sub, which in turn depends on this lemma.)

exts-seq : βˆ€{Ξ“ Ξ” Ξ”β€²} {σ₁ : Subst Ξ“ Ξ”} {Οƒβ‚‚ : Subst Ξ” Ξ”β€²}
         β†’ βˆ€ {A} β†’ (exts σ₁ ⨟ exts Οƒβ‚‚) {A} ≑ exts (σ₁ ⨟ Οƒβ‚‚)
exts-seq = extensionality Ξ» x β†’ lemma {x = x}
  where
  lemma : βˆ€{Ξ“ Ξ” Ξ”β€²}{A}{x : Ξ“ , β˜… βˆ‹ A} {σ₁ : Subst Ξ“ Ξ”}{Οƒβ‚‚ : Subst Ξ” Ξ”β€²}
     β†’ (exts σ₁ ⨟ exts Οƒβ‚‚) x ≑ exts (σ₁ ⨟ Οƒβ‚‚) x
  lemma {x = Z} = refl
  lemma {A = β˜…}{x = S x}{σ₁}{Οƒβ‚‚} =
     begin
       (exts σ₁ ⨟ exts Οƒβ‚‚) (S x)
     β‰‘βŸ¨βŸ©
       βŸͺ exts Οƒβ‚‚ ⟫ (rename S_ (σ₁ x))
     β‰‘βŸ¨ commute-subst-rename{M = σ₁ x}{Οƒ = Οƒβ‚‚}{ρ₁ = S_}{ρ₂ = S_} refl ⟩
       rename S_ (βŸͺ Οƒβ‚‚ ⟫ (σ₁ x))
     β‰‘βŸ¨βŸ©
       rename S_ ((σ₁ ⨟ Οƒβ‚‚) x)
     ∎

The proof proceed by cases on x.

  • If x = Z, the two sides are equal by the definition of exts and sequencing.

  • If x = S x, we unfold the first use of exts and sequencing, then apply the lemma commute-subst-rename. We conclude by the definition of sequencing.

Now we come to the proof of sub-sub, which we explain below.

sub-sub : βˆ€{Ξ“ Ξ” Ξ£}{A}{M : Ξ“ ⊒ A} {σ₁ : Subst Ξ“ Ξ”}{Οƒβ‚‚ : Subst Ξ” Ξ£}
            β†’ βŸͺ Οƒβ‚‚ ⟫ (βŸͺ σ₁ ⟫ M) ≑ βŸͺ σ₁ ⨟ Οƒβ‚‚ ⟫ M
sub-sub {M = ` x} = refl
sub-sub {Ξ“}{Ξ”}{Ξ£}{A}{Ζ› N}{σ₁}{Οƒβ‚‚} =
   begin
     βŸͺ Οƒβ‚‚ ⟫ (βŸͺ σ₁ ⟫ (Ζ› N))
   β‰‘βŸ¨βŸ©
     Ζ› βŸͺ exts Οƒβ‚‚ ⟫ (βŸͺ exts σ₁ ⟫ N)
   β‰‘βŸ¨ cong Ζ›_ (sub-sub{M = N}{σ₁ = exts σ₁}{Οƒβ‚‚ = exts Οƒβ‚‚}) ⟩
     Ζ› βŸͺ exts σ₁ ⨟ exts Οƒβ‚‚ ⟫ N
   β‰‘βŸ¨ cong Ζ›_ (cong-sub{M = N} (Ξ» {A} β†’ exts-seq) refl) ⟩
     Ζ› βŸͺ exts ( σ₁ ⨟ Οƒβ‚‚) ⟫ N
   ∎
sub-sub {M = L Β· M} = congβ‚‚ _Β·_ (sub-sub{M = L}) (sub-sub{M = M})

We proceed by induction on the term M.

  • If M = x, then both sides are equal to Οƒβ‚‚ (σ₁ x).

  • If M = Ζ› N, we first use the induction hypothesis to show that

      Ζ› βŸͺ exts Οƒβ‚‚ ⟫ (βŸͺ exts σ₁ ⟫ N) ≑ Ζ› βŸͺ exts σ₁ ⨟ exts Οƒβ‚‚ ⟫ N

    and then use the lemma exts-seq to show

      Ζ› βŸͺ exts σ₁ ⨟ exts Οƒβ‚‚ ⟫ N ≑ Ζ› βŸͺ exts ( σ₁ ⨟ Οƒβ‚‚) ⟫ N

  • If M is an application, we use the induction hypothesis for both subterms.

The following corollary of sub-sub specializes the first substitution to a renaming.

rename-subst : βˆ€{Ξ“ Ξ” Ξ”β€²}{M : Ξ“ ⊒ β˜…}{ρ : Rename Ξ“ Ξ”}{Οƒ : Subst Ξ” Ξ”β€²}
             β†’ βŸͺ Οƒ ⟫ (rename ρ M) ≑ βŸͺ Οƒ ∘ ρ ⟫ M
rename-subst {Ξ“}{Ξ”}{Ξ”β€²}{M}{ρ}{Οƒ} =
   begin
     βŸͺ Οƒ ⟫ (rename ρ M)
   β‰‘βŸ¨ cong βŸͺ Οƒ ⟫ (rename-subst-ren{M = M}) ⟩
     βŸͺ Οƒ ⟫ (βŸͺ ren ρ ⟫ M)
   β‰‘βŸ¨ sub-sub{M = M} ⟩
     βŸͺ ren ρ ⨟ Οƒ ⟫ M
   β‰‘βŸ¨βŸ©
     βŸͺ Οƒ ∘ ρ ⟫ M
   ∎

Proof of sub-assoc

The proof of sub-assoc follows directly from sub-sub and the definition of sequencing.

sub-assoc : βˆ€{Ξ“ Ξ” Ξ£ Ξ¨ : Context} {Οƒ : Subst Ξ“ Ξ”} {Ο„ : Subst Ξ” Ξ£}
             {ΞΈ : Subst Ξ£ Ξ¨}
          β†’ βˆ€{A} β†’ (Οƒ ⨟ Ο„) ⨟ ΞΈ ≑ (Οƒ ⨟ Ο„ ⨟ ΞΈ) {A}
sub-assoc {Ξ“}{Ξ”}{Ξ£}{Ξ¨}{Οƒ}{Ο„}{ΞΈ}{A} = extensionality Ξ» x β†’ lemma{x = x}
  where
  lemma : βˆ€ {x : Ξ“ βˆ‹ A} β†’ ((Οƒ ⨟ Ο„) ⨟ ΞΈ) x ≑ (Οƒ ⨟ Ο„ ⨟ ΞΈ) x
  lemma {x} =
      begin
        ((Οƒ ⨟ Ο„) ⨟ ΞΈ) x
      β‰‘βŸ¨βŸ©
        βŸͺ ΞΈ ⟫ (βŸͺ Ο„ ⟫ (Οƒ x))
      β‰‘βŸ¨ sub-sub{M = Οƒ x} ⟩
        βŸͺ Ο„ ⨟ ΞΈ ⟫ (Οƒ x)
      β‰‘βŸ¨βŸ©
        (Οƒ ⨟ Ο„ ⨟ ΞΈ) x
      ∎

Proof of subst-zero-exts-cons

The last equation we needed to prove subst-zero-exts-cons was sub-assoc, so we can now go ahead with its proof. We simply apply the equations for exts and subst-zero and then apply the Οƒ algebra equation to arrive at the normal form M β€’ Οƒ.

subst-zero-exts-cons : βˆ€{Ξ“ Ξ”}{Οƒ : Subst Ξ“ Ξ”}{B}{M : Ξ” ⊒ B}{A}
                     β†’ exts Οƒ ⨟ subst-zero M ≑ (M β€’ Οƒ) {A}
subst-zero-exts-cons {Ξ“}{Ξ”}{Οƒ}{B}{M}{A} =
    begin
      exts Οƒ ⨟ subst-zero M
    β‰‘βŸ¨ cong-seq exts-cons-shift subst-Z-cons-ids ⟩
      (` Z β€’ (Οƒ ⨟ ↑)) ⨟ (M β€’ ids)
    β‰‘βŸ¨ sub-dist ⟩
      (βŸͺ M β€’ ids ⟫ (` Z)) β€’ ((Οƒ ⨟ ↑) ⨟ (M β€’ ids))
    β‰‘βŸ¨ cong-cons (sub-head{Οƒ = ids}) refl ⟩
      M β€’ ((Οƒ ⨟ ↑) ⨟ (M β€’ ids))
    β‰‘βŸ¨ cong-cons refl (sub-assoc{Οƒ = Οƒ}) ⟩
      M β€’ (Οƒ ⨟ (↑ ⨟ (M β€’ ids)))
    β‰‘βŸ¨ cong-cons refl (cong-seq{Οƒ = Οƒ} refl (sub-tail{M = M}{Οƒ = ids})) ⟩
      M β€’ (Οƒ ⨟ ids)
    β‰‘βŸ¨ cong-cons refl (sub-idR{Οƒ = Οƒ}) ⟩
      M β€’ Οƒ
    ∎

Proof of the substitution lemma

We first prove the generalized form of the substitution lemma, showing that a substitution Οƒ commutes with the substitution of M into N.

βŸͺ exts Οƒ ⟫ N [ βŸͺ Οƒ ⟫ M ] ≑ βŸͺ Οƒ ⟫ (N [ M ])

This proof is where the Οƒ algebra pays off. The proof is by direct equational reasoning. Starting with the left-hand side, we apply Οƒ algebra equations, oriented left-to-right, until we arrive at the normal form

βŸͺ βŸͺ Οƒ ⟫ M β€’ Οƒ ⟫ N

We then do the same with the right-hand side, arriving at the same normal form.

subst-commute : βˆ€{Ξ“ Ξ”}{N : Ξ“ , β˜… ⊒ β˜…}{M : Ξ“ ⊒ β˜…}{Οƒ : Subst Ξ“ Ξ” }
    β†’ βŸͺ exts Οƒ ⟫ N [ βŸͺ Οƒ ⟫ M ] ≑ βŸͺ Οƒ ⟫ (N [ M ])
subst-commute {Ξ“}{Ξ”}{N}{M}{Οƒ} =
     begin
       βŸͺ exts Οƒ ⟫ N [ βŸͺ Οƒ ⟫ M ]
     β‰‘βŸ¨βŸ©
       βŸͺ subst-zero (βŸͺ Οƒ ⟫ M) ⟫ (βŸͺ exts Οƒ ⟫ N)
     β‰‘βŸ¨ cong-sub {M = βŸͺ exts Οƒ ⟫ N} subst-Z-cons-ids refl ⟩
       βŸͺ βŸͺ Οƒ ⟫ M β€’ ids ⟫ (βŸͺ exts Οƒ ⟫ N)
     β‰‘βŸ¨ sub-sub {M = N} ⟩
       βŸͺ (exts Οƒ) ⨟ ((βŸͺ Οƒ ⟫ M) β€’ ids) ⟫ N
     β‰‘βŸ¨ cong-sub {M = N} (cong-seq exts-cons-shift refl) refl ⟩
       βŸͺ (` Z β€’ (Οƒ ⨟ ↑)) ⨟ (βŸͺ Οƒ ⟫ M β€’ ids) ⟫ N
     β‰‘βŸ¨ cong-sub {M = N} (sub-dist {M = ` Z}) refl ⟩
       βŸͺ βŸͺ βŸͺ Οƒ ⟫ M β€’ ids ⟫ (` Z) β€’ ((Οƒ ⨟ ↑) ⨟ (βŸͺ Οƒ ⟫ M β€’ ids)) ⟫ N
     β‰‘βŸ¨βŸ©
       βŸͺ βŸͺ Οƒ ⟫ M β€’ ((Οƒ ⨟ ↑) ⨟ (βŸͺ Οƒ ⟫ M β€’ ids)) ⟫ N
     β‰‘βŸ¨ cong-sub{M = N} (cong-cons refl (sub-assoc{Οƒ = Οƒ})) refl ⟩
       βŸͺ βŸͺ Οƒ ⟫ M β€’ (Οƒ ⨟ ↑ ⨟ βŸͺ Οƒ ⟫ M β€’ ids) ⟫ N
     β‰‘βŸ¨ cong-sub{M = N} refl refl ⟩
       βŸͺ βŸͺ Οƒ ⟫ M β€’ (Οƒ ⨟ ids) ⟫ N
     β‰‘βŸ¨ cong-sub{M = N} (cong-cons refl (sub-idR{Οƒ = Οƒ})) refl ⟩
       βŸͺ βŸͺ Οƒ ⟫ M β€’ Οƒ ⟫ N
     β‰‘βŸ¨ cong-sub{M = N} (cong-cons refl (sub-idL{Οƒ = Οƒ})) refl ⟩
       βŸͺ βŸͺ Οƒ ⟫ M β€’ (ids ⨟ Οƒ) ⟫ N
     β‰‘βŸ¨ cong-sub{M = N} (sym sub-dist) refl ⟩
       βŸͺ M β€’ ids ⨟ Οƒ ⟫ N
     β‰‘βŸ¨ sym (sub-sub{M = N}) ⟩
       βŸͺ Οƒ ⟫ (βŸͺ M β€’ ids ⟫ N)
     β‰‘βŸ¨ cong βŸͺ Οƒ ⟫ (sym (cong-sub{M = N} subst-Z-cons-ids refl)) ⟩
       βŸͺ Οƒ ⟫ (N [ M ])
     ∎

A corollary of subst-commute is that rename also commutes with substitution. In the proof below, we first exchange rename ρ for the substitution βŸͺ ren ρ ⟫, and apply subst-commute, and then convert back to rename ρ.

rename-subst-commute : βˆ€{Ξ“ Ξ”}{N : Ξ“ , β˜… ⊒ β˜…}{M : Ξ“ ⊒ β˜…}{ρ : Rename Ξ“ Ξ” }
    β†’ (rename (ext ρ) N) [ rename ρ M ] ≑ rename ρ (N [ M ])
rename-subst-commute {Ξ“}{Ξ”}{N}{M}{ρ} =
     begin
       (rename (ext ρ) N) [ rename ρ M ]
     β‰‘βŸ¨ cong-sub (cong-sub-zero (rename-subst-ren{M = M}))
                 (rename-subst-ren{M = N}) ⟩
       (βŸͺ ren (ext ρ) ⟫ N) [ βŸͺ ren ρ ⟫ M ]
     β‰‘βŸ¨ cong-sub refl (cong-sub{M = N} ren-ext refl) ⟩
       (βŸͺ exts (ren ρ) ⟫ N) [ βŸͺ ren ρ ⟫ M ]
     β‰‘βŸ¨ subst-commute{N = N} ⟩
       subst (ren ρ) (N [ M ])
     β‰‘βŸ¨ sym (rename-subst-ren) ⟩
       rename ρ (N [ M ])
     ∎

To present the substitution lemma, we introduce the following notation for substituting a term M for index 1 within term N.

_γ€”_〕 : βˆ€ {Ξ“ A B C}
        β†’ Ξ“ , B , C ⊒ A
        β†’ Ξ“ ⊒ B
          ---------
        β†’ Ξ“ , C ⊒ A
_γ€”_〕 {Ξ“} {A} {B} {C} N M =
   subst {Ξ“ , B , C} {Ξ“ , C} (exts (subst-zero M)) {A} N

The substitution lemma is stated as follows and proved as a corollary of the subst-commute lemma.

substitution : βˆ€{Ξ“}{M : Ξ“ , β˜… , β˜… ⊒ β˜…}{N : Ξ“ , β˜… ⊒ β˜…}{L : Ξ“ ⊒ β˜…}
    β†’ (M [ N ]) [ L ] ≑ (M γ€” L 〕) [ (N [ L ]) ]
substitution{M = M}{N = N}{L = L} =
   sym (subst-commute{N = M}{M = N}{Οƒ = subst-zero L})

Notes

Most of the properties and proofs in this file are based on the paper Autosubst: Reasoning with de Bruijn Terms and Parallel Substitution by Schafer, Tebbi, and Smolka (ITP 2015). That paper, in turn, is based on the paper of Abadi, Cardelli, Curien, and Levy (1991) that defines the Οƒ algebra.

Unicode

This chapter uses the following unicode:

βŸͺ  U+27EA  MATHEMATICAL LEFT DOUBLE ANGLE BRACKET (\<<)
⟫  U+27EA  MATHEMATICAL RIGHT DOUBLE ANGLE BRACKET (\>>)
↑  U+2191  UPWARDS ARROW (\u)
β€’  U+2022  BULLET (\bub)
⨟  U+2A1F  Z NOTATION SCHEMA COMPOSITION (C-x 8 RET Z NOTATION SCHEMA COMPOSITION)
γ€”  U+3014  LEFT TORTOISE SHELL BRACKET (\( option 9 on page 2)
〕  U+3015  RIGHT TORTOISE SHELL BRACKET (\) option 9 on page 2)