Module Esubst

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, σ) : Δ

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

Unary variant of subst_liftn.

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

• ELID: identity relocation id
• ELSHFT (σ, n): shift of n, then σ; ↑^n ∘ σ in sigma calculi
• ELLFT (n, σ): apply σ to de Bruijn > n, i.e under n binders; ⇑^n(σ) in sigma calculi

Invariant ensured by the private flag: no lift contains an ELLFT of ELID, two consecutive ELLFT or two consecutive ELSHFT.

Relocations are a particular kind of substitutions that only contain variables. In particular, el_* enjoys similar 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 el_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 σ : Ξ.

Structural equality for lifts

Debugging utilities