package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Explicit substitutions

type 'a subs

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.

Derived constructors granting basic invariants

val subs_id : int -> 'a subs

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

val subs_cons : 'a -> 'a subs -> 'a subs

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

val subs_shft : (int * 'a subs) -> 'a subs

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

val subs_lift : 'a subs -> 'a subs

Unary variant of subst_liftn.

val subs_liftn : int -> 'a subs -> 'a subs

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

val expand_rel : int -> 'a subs -> (int * 'a, int * int option) Util.union

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).

val is_subs_id : 'a subs -> bool

Tests whether a substitution behaves like the identity

Composition of substitutions: comp mk_clos s1 s2 computes a substitution equivalent to applying s2 then s1. Argument mk_clos is used when a closure has to be created, i.e. when s1 is applied on an element of s2.

type lift = private
  1. | ELID
  2. | ELSHFT of lift * int
  3. | ELLFT of int * lift

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_*.

val el_id : lift

For arbitrary Γ: Γ ⊢ el_id : Γ

val el_shft : int -> lift -> lift

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

val el_liftn : int -> lift -> lift

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

val el_lift : lift -> lift

Unary variant of subst_liftn.

val reloc_rel : int -> lift -> int

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

val is_lift_id : lift -> bool
val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs

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 σ : Ξ.

val eq_lift : lift -> lift -> bool

Equality for lifts

module Internal : sig ... end

Debugging utilities

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct