\[\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}\]

The standard library¶

Survey¶

The standard library is structured into the following subdirectories:

Logic : Classical logic and dependent equality

Arith : Basic Peano arithmetic

PArith : Basic positive integer arithmetic

NArith : Basic binary natural number arithmetic

ZArith : Basic relative integer arithmetic

Numbers : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)

Bool : Booleans (basic functions and results)

Lists : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with coinductive types)

Sets : Sets (classical, constructive, finite, infinite, power set, etc.)

FSets : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)

Reals : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)

Floats : Machine implementation of floating-point arithmetic (for the binary64 format)

Relations : Relations (definitions and basic results)

Sorting : Sorted list (basic definitions and heapsort correctness)

Strings : 8-bits characters and strings

Wellfounded : Well-founded relations (basic results)

These directories belong to the initial load path of the system, and the modules they provide are compiled at installation time. So they are directly accessible with the command Require.

The different modules of the Coq standard library are documented online at https://coq.inria.fr/stdlib/.

Peano’s arithmetic (nat)¶

While in the initial state, many operations and predicates of Peano's arithmetic are defined, further operations and results belong to other modules. For instance, the decidability of the basic predicates are defined here. This is provided by requiring the module Arith.

The following table describes the notations available in scope nat_scope :

Notation	Interpretation
`_ < _`	`lt`
`_ <= _`	`le`
`_ > _`	`gt`
`_ >= _`	`ge`
`x < y < z`	`x < y /\ y < z`
`x < y <= z`	`x < y /\ y <= z`
`x <= y < z`	`x <= y /\ y < z`
`x <= y <= z`	`x <= y /\ y <= z`
`_ + _`	`plus`
`_ - _`	`minus`
`_ * _`	`mult`

Notations for integer arithmetic¶

The following table describes the syntax of expressions for integer arithmetic. It is provided by requiring and opening the module ZArith and opening scope Z_scope. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity.

Notation	Interpretation	Precedence	Associativity
`_ < _`	`Z.lt`
`_ <= _`	`Z.le`
`_ > _`	`Z.gt`
`_ >= _`	`Z.ge`
`x < y < z`	`x < y /\ y < z`
`x < y <= z`	`x < y /\ y <= z`
`x <= y < z`	`x <= y /\ y < z`
`x <= y <= z`	`x <= y /\ y <= z`
`_ ?= _`	`Z.compare`	70	no
`_ + _`	`Z.add`
`_ - _`	`Z.sub`
`_ * _`	`Z.mul`
`_ / _`	`Z.div`
`_ mod _`	`Z.modulo`	40	no
`- _`	`Z.opp`
`_ ^ _`	`Z.pow`

Example

From Stdlib Require Import ZArith.: [Loading ML file rocq-runtime.plugins.ring ... done] [Loading ML file rocq-runtime.plugins.zify ... done] [Loading ML file rocq-runtime.plugins.micromega_core ... done] [Loading ML file rocq-runtime.plugins.micromega ... done] [Loading ML file rocq-runtime.plugins.btauto ... done]
Check (2 + 3)%Z.: (2 + 3)%Z : Z
Open Scope Z_scope.
Check 2 + 3.: 2 + 3 : Z

Real numbers library¶

Notations for real numbers¶

This is provided by requiring and opening the module Reals and opening scope R_scope. This set of notations is very similar to the notation for integer arithmetic. The inverse function was added.

Notation	Interpretation
`_ < _`	`Rlt`
`_ <= _`	`Rle`
`_ > _`	`Rgt`
`_ >= _`	`Rge`
`x < y < z`	`x < y /\ y < z`
`x < y <= z`	`x < y /\ y <= z`
`x <= y < z`	`x <= y /\ y < z`
`x <= y <= z`	`x <= y /\ y <= z`
`_ + _`	`Rplus`
`_ - _`	`Rminus`
`_ * _`	`Rmult`
`_ / _`	`Rdiv`
`- _`	`Ropp`
`/ _`	`Rinv`
`_ ^ _`	`pow`

Example

From Stdlib Require Import Reals.
Check (2 + 3)%R.: (2 + 3)%R : R
Open Scope R_scope.
Check 2 + 3.: 2 + 3 : R

Some tactics for real numbers¶

In addition to the powerful ring, field and lra tactics (see Chapters ring and micromega), there are also:

Tactic discrR¶: Proves that two real integer constants are different.

Example

From Stdlib Require Import DiscrR.
Open Scope R_scope.
Goal 5 <> 0.: 1 goal ============================ 5 <> 0
discrR.

Tactic split_Rabs¶: Allows unfolding the Rabs constant and splits corresponding conjunctions.

Example

From Stdlib Require Import Reals.
Open Scope R_scope.
Goal forall x:R, x <= Rabs x.: 1 goal ============================ forall x : R, x <= Rabs x
intro; split_Rabs.: 2 goals x : R Hlt : x < 0 ============================ x <= - x goal 2 is: x <= x

Tactic split_Rmult¶: Splits a condition that a product is non-null into subgoals corresponding to the condition on each operand of the product.

Example

From Stdlib Require Import Reals.
Open Scope R_scope.
Goal forall x y z:R, x * y * z <> 0.: 1 goal ============================ forall x y z : R, x * y * z <> 0
intros; split_Rmult.: 3 goals x, y, z : R ============================ x <> 0 goal 2 is: y <> 0 goal 3 is: z <> 0

List library¶

Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module List.

It defines the following notions:

length

head : first element (with default)

tail : all but first element

app : concatenation

rev : reverse

nth : accessing n-th element (with default)

map : applying a function

flat_map : applying a function returning lists

fold_left : iterator (from head to tail)

fold_right : iterator (from tail to head)

The following table shows notations available when opening scope list_scope.

Notation	Interpretation	Precedence	Associativity
`_ ++ _`	`app`	60	right
`_ :: _`	`cons`	60	right

Floats library¶

The standard library has a small Floats module for accessing processor floating-point operations through the Coq kernel. However, while this module supports computation and has a bit-level specification, it doesn't include elaborate theorems, such as a link to real arithmetic or various error bounds. To do proofs by reflection, use Floats in conjunction with the complementary Flocq library, which provides many such theorems.

The library of primitive floating-point arithmetic can be loaded by requiring module Floats:

From Stdlib Require Import Floats.

It exports the module PrimFloat that provides a primitive type named float, defined in the kernel as well as two variant types float_comparison and float_class:

Print float.: *** [ float : Set ]
Print float_comparison.: Variant float_comparison : Set := FEq : float_comparison | FLt : float_comparison | FGt : float_comparison | FNotComparable : float_comparison.
Print float_class.: Variant float_class : Set := PNormal : float_class | NNormal : float_class | PSubn : float_class | NSubn : float_class | PZero : float_class | NZero : float_class | PInf : float_class | NInf : float_class | NaN : float_class.

It then defines the primitive operators below, using the processor floating-point operators for binary64 in rounding-to-nearest even:

abs
opp
sub
add
mul
div
sqrt
compare : compare two floats and return a float_comparison
classify : analyze a float and return a float_class
of_int63 : round a primitive integer and convert it into a float
normfr_mantissa : take a float in [0.5; 1.0) and return its mantissa
frshiftexp : convert a float to fractional part in [0.5; 1.0) and integer part
ldshiftexp : multiply a float by an integral power of 2
next_up : return the next float towards positive infinity
next_down : return the next float towards negative infinity

For special floating-point values, the following constants are also defined:

zero
neg_zero
one
two
infinity
neg_infinity
nan : Not a Number (assumed to be unique: the "payload" of NaNs is ignored)

The following table shows the notations available when opening scope float_scope.

Notation	Interpretation
`- _`	`opp`
`_ - _`	`sub`
`_ + _`	`add`
`_ * _`	`mul`
`_ / _`	`div`
`_ =? _`	`eqb`
`_ <? _`	`ltb`
`_ <=? _`	`leb`
`_ ?= _`	`compare`

Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition $\text{parse} \circ \text{print}$ amounts to the identity.

Warning The constant number is not a binary64 floating-point value. A closest value number will be used and unambiguously printed number. [inexact-float,parsing]¶: Not all decimal constants are floating-point values. This warning is generated when parsing such a constant (for instance 0.1).

Flag Printing Float¶: Turn this flag off (it is on by default) to deactivate decimal printing of floating-point constants. They will then be printed with an hexadecimal representation.

Example

Open Scope float_scope.
Eval compute in 1 + 0.5.: = 1.5 : float
Eval compute in 1 / 0.: = infinity : float
Eval compute in 1 / -0.: = neg_infinity : float
Eval compute in 0 / 0.: = nan : float
Eval compute in 0 ?= -0.: = FEq : float_comparison
Eval compute in nan ?= nan.: = FNotComparable : float_comparison
Eval compute in next_down (-1).: = -1.0000000000000002 : float

The primitive operators are specified with respect to their Gallina counterpart, using the variant type spec_float, and the injection Prim2SF:

Print spec_float.: Variant spec_float : Set := S754_zero : bool -> spec_float | S754_infinity : bool -> spec_float | S754_nan : spec_float | S754_finite : bool -> positive -> Z -> spec_float. Arguments S754_zero s%bool_scope Arguments S754_infinity s%bool_scope Arguments S754_finite s%bool_scope m%positive_scope e%Z_scope
Check Prim2SF.: Prim2SF : float -> spec_float
Check mul_spec.: mul_spec : forall x y : float, Prim2SF (x * y) = SF64mul (Prim2SF x) (Prim2SF y)

For more details on the available definitions and lemmas, see the online documentation of the Floats library.

Primitive strings library¶

The standard library provides a PrimString module declaring a primitive string type PrimString.string (corresponding to the OCaml string type), together with a small set of primitive functions:

max_length : gives the maximum length of a string
make : builds a string of the given length conly containing the given byte
length : gives the lenght of the given string
get : gives the byte at a given index in the given string
sub : extracts the sub-string from the given string that starts at the given offset and with the given length
cat : concatenates the two given strings
compare : compares the two strings and returns a comparison

Bytes are represented using the PrimString.char63, which is defined as Uint63.int, but primitive strings only store values fitting on 8 bits (i.e., values between 0 and 255).

Axiomatic specifications of these primitive string functions are provided in the PrimStringAxioms module. Additional properties, and relations to equivalent primitives defined in Gallina are provided in module PString (which exports PrimString and PrimStringAxioms.

A custom string notation is provided for the string and char63 types, in respective scopes pstring and char63.