package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Occur checks
val closedn : int -> Constr.constr -> bool

closedn n M is true iff M is a (de Bruijn) closed term under n binders

val closed0 : Constr.constr -> bool

closed0 M is true iff M is a (de Bruijn) closed term

val noccurn : int -> Constr.constr -> bool

noccurn n M returns true iff Rel n does NOT occur in term M

val noccur_between : int -> int -> Constr.constr -> bool

noccur_between n m M returns true iff Rel p does NOT occur in term M for n <= p < n+m

val noccur_with_meta : int -> int -> Constr.constr -> bool

Checking function for terms containing existential- or meta-variables. The function noccur_with_meta does not consider meta-variables applied to some terms (intended to be its local context) (for existential variables, it is necessarily the case)

Relocation and substitution

exliftn el c lifts c with arbitrary complex lifting el

val liftn : int -> int -> Constr.constr -> Constr.constr

liftn n k c lifts by n indices greater than or equal to k in c Note that with respect to substitution calculi's terminology, n is the _shift_ and k is the _lift_.

val lift : int -> Constr.constr -> Constr.constr

lift n c lifts by n the positive indexes in c

val liftn_rel_context : int -> int -> Constr.rel_context -> Constr.rel_context

Same as liftn for a context

val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context

Same as lift for a context

The type substl is the type of substitutions u₁..un of type some well-typed context Δ and defined in some environment Γ. Typing of substitutions is defined by:

  • Γ ⊢ ∅ : ∅,
  • Γ ⊢ u₁..un-1 : Δ and Γ ⊢ un : An[u₁..un-1] implies Γ ⊢ u₁..un : Δ,xn:An
  • Γ ⊢ u₁..un-1 : Δ and Γ ⊢ un : An[u₁..un-1] implies Γ ⊢ u₁..un : Δ,xn:=cn:An when Γ ⊢ un ≡ cn[u₁..un-1]

Note that u₁..un is represented as a list with un at the head of the list, i.e. as [un;...;u₁].

A substl differs from an instance in that it includes the terms bound by lets while the latter does not. Also, their internal representations are in opposite order.

type substl = Constr.constr list

The type instance is the type of instances u₁..un of a well-typed context Δ (relatively to some environment Γ). Typing of instances is defined by:

  • Γ ⊢ ∅ : ∅,
  • Γ ⊢ u₁..un : Δ and Γ ⊢ un+1 : An+1[ϕ(Δ,u₁..un)] implies Γ ⊢ u₁..un+1 : Δ,xn+1:An+1
  • Γ ⊢ u₁..un : Δ implies Γ ⊢ u₁..un : Δ,xn+1:=cn+1:An+1 where ϕ(Δ,u₁..u{_n}) is the substitution obtained by adding lets of Δ to the instance so as to get a substitution (see subst_of_rel_context_instance below).

Note that u₁..un is represented as an array with u1 at the head of the array, i.e. as [u₁;...;un]. In particular, it can directly be used with mkApp to build an applicative term f u₁..un whenever f is of some type forall Δ, T.

An instance differs from a substl in that it does not include the terms bound by lets while the latter does. Also, their internal representations are in opposite order.

An instance_list is the same as an instance but using a list instead of an array.

type instance = Constr.constr array
type instance_list = Constr.constr list
val subst_of_rel_context_instance : Constr.rel_context -> instance -> substl

Let Γ be a context interleaving declarations x₁:T₁..xn:Tn and definitions y₁:=c₁..yp:=cp in some context Γ₀. Let u₁..un be an instance of Γ, i.e. an instance in Γ₀ of the xi. Then, subst_of_rel_context_instance_list Γ u₁..un returns the corresponding substitution of Γ, i.e. the appropriate interleaving σ of the u₁..un with the c₁..cp, all of them in Γ₀, so that a derivation Γ₀, Γ, Γ₁|- t:T can be instantiated into a derivation Γ₀, Γ₁ |- t[σ]:T[σ] using substnl σ |Γ₁| t. Note that the instance u₁..un is represented starting with u₁, as if usable in applist while the substitution is represented the other way round, i.e. ending with either u₁ or c₁, as if usable for substl.

val subst_of_rel_context_instance_list : Constr.rel_context -> instance_list -> substl
val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int

Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in x:A;y:=b;z:C is 3, i.e. a reference to z)

val substnl : substl -> int -> Constr.constr -> Constr.constr

substnl [a₁;...;an] k c substitutes in parallel a₁,...,an for respectively Rel(k+1),...,Rel(k+n) in c; it relocates accordingly indexes in an,...,a1 and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ' ⊢ c : T with |Γ'|=k, then Γ, Γ' ⊢ substnl [a₁;...;an] k c : substnl [a₁;...;an] k T.

substl σ c is a short-hand for substnl σ 0 c

substl a c is a short-hand for substnl [a] 0 c

val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration

substnl_decl [a₁;...;an] k Ω substitutes in parallel a₁, ..., an for respectively Rel(k+1), ..., Rel(k+n) in a declaration Ω; it relocates accordingly indexes in a₁,...,an and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=k, then Γ, Γ', substnl_decl [a₁;...;an] k Ω ⊢.

substl_decl σ Ω is a short-hand for substnl_decl σ 0 Ω

subst1_decl a Ω is a short-hand for substnl_decl [a] 0 Ω

val substnl_rel_context : substl -> int -> Constr.rel_context -> Constr.rel_context

substnl_rel_context [a₁;...;an] k Ω substitutes in parallel a₁, ..., an for respectively Rel(k+1), ..., Rel(k+n) in a context Ω; it relocates accordingly indexes in a₁,...,an and c. In terms of typing, if Γ ⊢ an..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=k, then Γ, Γ', substnl_rel_context [a₁;...;an] k Ω ⊢.

val substl_rel_context : substl -> Constr.rel_context -> Constr.rel_context

substl_rel_context σ Ω is a short-hand for substnl_rel_context σ 0 Ω

val subst1_rel_context : Constr.constr -> Constr.rel_context -> Constr.rel_context

subst1_rel_context a Ω is a short-hand for substnl_rel_context [a] 0 Ω

val esubst : (int -> 'a -> Constr.constr) -> 'a Esubst.subs -> Constr.constr -> Constr.constr

esubst lift σ c substitutes c with arbitrary complex substitution σ, using lift to lift subterms where necessary.

val replace_vars : (Names.Id.t * Constr.constr) list -> Constr.constr -> Constr.constr

replace_vars k [(id₁,c₁);...;(idn,cn)] t substitutes Var idj by cj in t.

val substn_vars : int -> Names.Id.t list -> Constr.constr -> Constr.constr

substn_vars k [id₁;...;idn] t substitutes Var idj by Rel j+k-1 in t. If two names are identical, the one of least index is kept. In terms of typing, if Γ,xn:Un,...,x₁:U₁,Γ' ⊢ t:T, together with idj:Tj and Γ,xn:Un,...,x₁:U₁,Γ' ⊢ Tj[idj+1..idn:=xj+1..xn] ≡ Uj, then Γ\{id₁,...,idn},xn:Un,...,x₁:U₁,Γ' ⊢ substn_vars (|Γ'|+1) [id₁;...;idn] t : substn_vars (|Γ'|+1) [id₁;...;idn] T.

val subst_vars : Names.Id.t list -> Constr.constr -> Constr.constr

subst_vars [id1;...;idn] t is a short-hand for substn_vars [id1;...;idn] 1 t: it substitutes Var idj by Rel j in t. If two names are identical, the one of least index is kept.

val subst_var : Names.Id.t -> Constr.constr -> Constr.constr

subst_var id t is a short-hand for substn_vars [id] 1 t: it substitutes Var id by Rel 1 in t.

val smash_rel_context : Constr.rel_context -> Constr.rel_context

Expand lets in context

Substitution of universes

Level substitutions for polymorphism.

val subst_univs_level_constr : UVars.sort_level_subst -> Constr.constr -> Constr.constr
val subst_univs_level_context : UVars.sort_level_subst -> Constr.rel_context -> Constr.rel_context
val subst_instance_constr : UVars.Instance.t -> Constr.constr -> Constr.constr

Instance substitution for polymorphism.

val subst_instance_context : UVars.Instance.t -> Constr.rel_context -> Constr.rel_context

Ignores the constraints carried by univ_abstracted.

val map_constr_relevance : (Sorts.relevance -> Sorts.relevance) -> Constr.t -> Constr.t

Modifies the relevances in the head node (not in subterms)

val sort_and_universes_of_constr : Constr.constr -> Sorts.QVar.Set.t * Univ.Level.Set.t
val universes_of_constr : Constr.constr -> Univ.Level.Set.t

Low-level cached lift type

type substituend
val make_substituend : Constr.constr -> substituend
val lift_substituend : int -> substituend -> Constr.constr
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