Explicit substitutions for some type of terms 'a.

Assuming terms enjoy a notion of typability Γ ⊢ t : A, where Γ is a telescope and A a type, substitutions can be typed as Γ ⊢ σ : Δ, where as a first approximation σ is a list of terms u₁; ...; uₙ s.t. Δ := (x₁ : A₁), ..., (xₙ : Aₙ) and Γ ⊢ uᵢ : Aᵢu₁...uᵢ₋₁ for all 1 ≤ i ≤ n.

Substitutions can be applied to terms as follows, and furthermore if Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ tσ : Aσ.

We make the typing rules explicit below, but we omit the explicit De Bruijn fidgetting and leave relocations implicit in terms and types.

Assuming |Γ| = n, Γ ⊢ subs_id n : Γ

Assuming Γ ⊢ σ : Δ and Γ ⊢ t : Aσ, then Γ ⊢ subs_cons t σ : Δ, A

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ

Unary variant of subst_liftn.

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ

expand_rel k subs expands de Bruijn k in the explicit substitution subs. The result is either (Inl(lams,v)) when the variable is substituted by value v under lams binders (i.e. v *has* to be shifted by lams), or (Inr (k',p)) when the variable k is just relocated as k'; p is None if the variable points inside subs and Some(k) if the variable points k bindings beyond subs (cf argument of ESID).

Tests whether a substitution behaves like the identity

Compact representation of explicit relocations

• ELSHFT(l,n) == lift of n, then apply lift l.
• ELLFT(n,l) == apply l to de Bruijn > n i.e under n binders.

Invariant ensured by the private flag: no lift contains two consecutive ELSHFT nor two consecutive ELLFT.

Relocations are a particular kind of substitutions that only contain variables. In particular, el_* enjoys the same typing rules as the equivalent substitution function subs_*.

For arbitrary Γ: Γ ⊢ el_id : Γ

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ el_shft (n, σ) : Δ

Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ el_liftn n σ : Δ, Ξ

Unary variant of subst_liftn.

Assuming Γ₁, A, Γ₂ ⊢ σ : Δ₁, A, Δ₂ and Δ₁, A, Δ₂ ⊢ n : A, then Γ₁, A, Γ₂ ⊢ reloc_rel n σ : A

Lift applied to substitution: lift_subst mk_clos el s computes a substitution equivalent to applying el then s. Argument mk_clos is used when a closure has to be created, i.e. when el is applied on an element of s.

That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.

Debugging utilities