\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Primitive objects

Primitive Integers

The language of terms features 63-bit machine integers as values. The type of such a value is axiomatized; it is declared through the following sentence (excerpt from the PrimInt63 module):

Primitive int := #int63_type.

This type can be understood as representing either unsigned or signed integers, depending on which module is imported or, more generally, which scope is open. Uint63 and uint63_scope refer to the unsigned version, while Sint63 and sint63_scope refer to the signed one.

The PrimInt63 module declares the available operators for this type. For instance, equality of two unsigned primitive integers can be determined using the Uint63.eqb function, declared and specified as follows:

Primitive eqb := #int63_eq. Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : uint63_scope. Axiom eqb_correct : forall i j, (i == j)%uint63 = true -> i = j.

The complete set of such operators can be found in the PrimInt63 module. The specifications and notations are in the Uint63 and Sint63 modules.

These primitive declarations are regular axioms. As such, they must be trusted and are listed by the Print Assumptions command, as in the following example.

From Coq Require Import Uint63.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file zify_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Lemma one_minus_one_is_zero : (1 - 1 = 0)%uint63.
1 goal ============================ (1 - 1)%uint63 = 0%uint63
Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
No more goals.
Print Assumptions one_minus_one_is_zero.
Axioms: sub : int -> int -> int eqb_correct : forall i j : int, (i =? j)%uint63 = true -> i = j eqb : int -> int -> bool

The reduction machines implement dedicated, efficient rules to reduce the applications of these primitive operations.

The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlInt63 module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Uint63 module (including signed functions for Sint63 despite the name). That OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq.

Literal values (at type Uint63.int) are extracted to literal OCaml values wrapped into the Uint63.of_int (resp. Uint63.of_int64) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function Uint63.compile from the kernel).

Primitive Floats

The language of terms features Binary64 floating-point numbers as values. The type of such a value is axiomatized; it is declared through the following sentence (excerpt from the PrimFloat module):

Primitive float := #float64_type.

This type is equipped with a few operators, that must be similarly declared. For instance, the product of two primitive floats can be computed using the PrimFloat.mul function, declared and specified as follows:

Primitive mul := #float64_mul. Notation "x * y" := (mul x y) : float_scope. Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y).

where Prim2SF is defined in the FloatOps module.

The set of such operators is described in section Floats library.

These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the Print Assumptions command.

The reduction machines (vm_compute, native_compute) implement dedicated, efficient rules to reduce the applications of these primitive operations, using the floating-point processor operators that are assumed to comply with the IEEE 754 standard for floating-point arithmetic.

The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlFloats module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Float64 module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq.

Literal values (of type Float64.t) are extracted to literal OCaml values (of type float) written in hexadecimal notation and wrapped into the Float64.of_float constructor, e.g.: Float64.of_float (0x1p+0).

Primitive Arrays

The language of terms features persistent arrays as values. The type of such a value is axiomatized; it is declared through the following sentence (excerpt from the PArray module):

Primitive array := #array_type.

This type is equipped with a few operators, that must be similarly declared. For instance, elements in an array can be accessed and updated using the PArray.get and PArray.set functions, declared and specified as follows:

Primitive get := #array_get. Primitive set := #array_set. Notation "t .[ i ]" := (get t i). Notation "t .[ i <- a ]" := (set t i a). Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].

The rest of these operators can be found in the PArray module.

These primitive declarations are regular axioms. As such, they must be trusted and are listed by the Print Assumptions command.

The reduction machines (vm_compute, native_compute) implement dedicated, efficient rules to reduce the applications of these primitive operations.

The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlPArray module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Parray module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq (see kernel/parray.ml).

Coq's primitive arrays are persistent data structures. Semantically, a set operation t.[i <- a] represents a new array that has the same values as t, except at position i where its value is a. The array t still exists, can still be used and its values were not modified. Operationally, the implementation of Coq's primitive arrays is optimized so that the new array t.[i <- a] does not copy all of t. The details are in section 2.3 of [CF07]. In short, the implementation keeps one version of t as an OCaml native array and other versions as lists of modifications to t. Accesses to the native array version are constant time operations. However, accesses to versions where all the cells of the array are modified have O(n) access time, the same as a list. The version that is kept as the native array changes dynamically upon each get and set call: the current list of modifications is applied to the native array and the lists of modifications of the other versions are updated so that they still represent the same values.