\[\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 Coq libraries

The core library contains definitions and theorems for the most commonly used elementary logical notions and data types, as well as primitive objects, support for tactics such as `setoid_rewrite` or commands such as Program, the proof language ssreflect, the tactic language Ltac2 and some compatibilty helpers for previous versions of Rocq. The content of the corelib can be browsed at https://rocq-prover.org/corelib/.

Rocq automatically loads many of these files when it starts. This set of preloaded files is called the prelude. Its content can be browsed at https://rocq-prover.org/corelib/Corelib.Init.Prelude.html.

Other libraries like the standard library are general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the `From Stdlib Require` command (see Compiled files). The content of the standard library can be browsed at https://rocq-prover.org/stdlib/.

There are many other libraries provided by the Rocq users' community. Many such libraries and developments are packaged in Nix or Opam. The Rocq Opam repository can be browsed at https://rocq-prover.org/packages/ (see Opam repository).

This chapter briefly reviews the prelude.

## The prelude

This section lists the basic notions and results which are directly available in the standard Coq system. Most of these constructions are defined in the `Prelude` module in directory `theories/Init` in the Coq root directory; this includes the modules `Notations`, `Logic`, `Datatypes`, `Specif`, `Peano`, `Wf` and `Tactics`.

### Notations

This module defines the parsing and pretty-printing of many symbols (infixes, prefixes, etc.). However, it does not assign a meaning to these notations. The purpose of this is to define and fix once for all the precedence and associativity of very common notations. The main notations fixed in the initial state are :

Notation | Precedence | Associativity
--- | --- | ---
`_ -> _` | 99 | right
`_ <-> _` | 95 | no
`_ \/ _` | 85 | right
`_ /\ _` | 80 | right
`~ _` | 75 | right
`_ = _` | 70 | no
`_ = _ = _` | 70 | no
`_ = _ :> _` | 70 | no
`_ <> _` | 70 | no
`_ <> _ :> _` | 70 | no
`_ < _` | 70 | no
`_ > _` | 70 | no
`_ <= _` | 70 | no
`_ >= _` | 70 | no
`_ < _ < _` | 70 | no
`_ < _ <= _` | 70 | no
`_ <= _ < _` | 70 | no
`_ <= _ <= _` | 70 | no
`_ + _` | 50 | left
`_ || _` | 50 | left
`_ - _` | 50 | left
`_ * _` | 40 | left
`_ && _` | 40 | left
`_ / _` | 40 | left
`- _` | 35 | right
`/ _` | 35 | right
`_ ^ _` | 30 | right

### Logic

`Logic.v` in the basic library of Coq has the definitions of standard (intuitionistic) logical connectives defined as inductive constructions. They are equipped with an appealing syntax enriching the subclass `form` of the syntactic class `term`. The constructs for `form` are:

True | True
False | False
`~ form` | not
`form /\ form` | and
`form \/ form` | or
`form -> form` | primitive implication
`form <-> form` | iff
`forall ident : type, form` | primitive for all
`exists ident specif?, form` | ex
`exists2 ident specif?, form & form` | ex2
`term = term` | eq
`term = term :> specif` | eq

Note

Implication is not defined but primitive (it is a non-dependent product of a proposition over another proposition). There is also a primitive universal quantification (it is a dependent product over a proposition). The primitive universal quantification allows both first-order and higher-order quantification.

#### Propositional Connectives

First, we find propositional calculus connectives. At times, it's helpful to know exactly what these notations represent.

Inductive True : Prop := I. Inductive False : Prop := . Definition not (A: Prop) := A -> False. Inductive and (A B:Prop) : Prop := conj (_:A) (_:B). Section Projections. Variables A B : Prop. Theorem proj1 : A /\ B -> A. Theorem proj2 : A /\ B -> B. End Projections. Inductive or (A B:Prop) : Prop := | or_introl (_:A) | or_intror (_:B). Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).

We also have the `Type` level negation:

Definition notT (A:Type) := A -> False.
  notT is defined

#### Quantifiers

Then we find first-order quantifiers:

Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
  all is defined
Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x).
  ex is defined ex_ind is defined ex_sind is defined
Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop := ex_intro2 (x:A) (_:P x) (_:Q x).
  ex2 is defined ex2_ind is defined ex2_sind is defined

The following abbreviations are allowed:

`exists x:A, P` | `ex A (fun x:A => P)`
`exists x, P` | `ex _ (fun x => P)`
`exists2 x:A, P & Q` | `ex2 A (fun x:A => P) (fun x:A => Q)`
`exists2 x, P & Q` | `ex2 _ (fun x => P) (fun x => Q)`

The type annotation `:A` can be omitted when `A` can be synthesized by the system.

#### Equality

Then, we find equality, defined as an inductive relation. That is, given a type `A` and an `x` of type `A`, the predicate `(eq A x)` is the smallest one which contains `x`. This definition, due to Christine Paulin-Mohring, is equivalent to define `eq` as the smallest reflexive relation, and it is also equivalent to Leibniz' equality.

Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.
  eq is defined eq_rect is defined eq_ind is defined eq_rec is defined eq_sind is defined

#### Lemmas

Finally, a few easy lemmas are provided.

Theorem absurd : forall A C:Prop, A -> ~ A -> C. Section equality. Variables A B : Type. Variable f : A -> B. Variables x y z : A. Theorem eq_sym : x = y -> y = x. Theorem eq_trans : x = y -> y = z -> x = z. Theorem f_equal : x = y -> f x = f y. Theorem not_eq_sym : x <> y -> y <> x. End equality. Definition eq_ind_r : forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y. Definition eq_rec_r : forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y. Definition eq_rect_r : forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y. Hint Immediate eq_sym not_eq_sym : core.

The theorem `f_equal` is extended to functions with two to five arguments. The theorem are names `f_equal2`, `f_equal3`, `f_equal4` and `f_equal5`. For instance `f_equal3` is defined the following way.

Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
  1 goal ============================ forall (A1 A2 A3 B : Type) (f : A1 -> A2 -> A3 -> B) (x1 y1 : A1) (x2 y2 : A2) (x3 y3 : A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3

### Datatypes

In the basic library, we find in `Datatypes.v` the definition of the basic data-types of programming, defined as inductive constructions over the sort `Set`. Some of them come with a special syntax shown below (this syntax table is common with the next section Specification). The constructs for `specif` are:

`specif * specif` | prod
`specif + specif` | sum
`specif + { specif }` | sumor
`{ specif } + { specif }` | sumbool
`{ ident : specif | form }` | sig
`{ ident : specif | form & form }` | sig2
`{ ident : specif & specif }` | sigT
`{ ident : specif & specif & specif }` | sigT2

The notation for pairs (elements of type prod) is: `(term, term)`

#### Programming

Inductive unit : Set := tt.
  unit is defined unit_rect is defined unit_ind is defined unit_rec is defined unit_sind is defined
Inductive bool : Set := true | false.
  bool is defined bool_rect is defined bool_ind is defined bool_rec is defined bool_sind is defined
Inductive nat : Set := O | S (n:nat).
  nat is defined nat_rect is defined nat_ind is defined nat_rec is defined nat_sind is defined
Inductive option (A:Set) : Set := Some (_:A) | None.
  option is defined option_rect is defined option_ind is defined option_rec is defined option_sind is defined

Note that zero is the letter `O`, and not the numeral `0`.

We then define the disjoint sum of `A+B` of two sets `A` and `B`, and their product `A*B`.

Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
  sum is defined sum_rect is defined sum_ind is defined sum_rec is defined sum_sind is defined
Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
  prod is defined prod_rect is defined prod_ind is defined prod_rec is defined prod_sind is defined
Section projections.
Variables A B : Set.
  A is declared B is declared
Definition fst (H: prod A B) := match H with | pair _ _ x y => x end.
  fst is defined
Definition snd (H: prod A B) := match H with | pair _ _ x y => y end.
  snd is defined
End projections.

Some operations on `bool` are also provided: `andb` (with infix notation `&&`), `orb` (with infix notation `||`), `xorb`, `implb` and `negb`.

### Specification

The following notions defined in module `Specif.v` allow to build new data-types and specifications. They are available with the syntax shown in the previous section Datatypes.

For instance, given `A:Type` and `P:A->Prop`, the construct `{x:A | P x}` (in abstract syntax `(sig A P)`) is a `Type`. We may build elements of this set as `(exist x p)` whenever we have a witness `x:A` with its justification `p:P x`.

From such a `(exist x p)` we may in turn extract its witness `x:A` (using an elimination construct such as `match`) but not its justification, which stays hidden, like in an abstract data-type. In technical terms, one says that `sig` is a weak (dependent) sum. A variant `sig2` with two predicates is also provided.

Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
  sig is defined sig_rect is defined sig_ind is defined sig_rec is defined sig_sind is defined
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x).
  sig2 is defined sig2_rect is defined sig2_ind is defined sig2_rec is defined sig2_sind is defined

A strong (dependent) sum `{x:A & P x}` may be also defined, when the predicate `P` is now defined as a constructor of types in `Type`.

Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x).
  sigT is defined sigT_rect is defined sigT_ind is defined sigT_rec is defined sigT_sind is defined
Section Projections2.
Variable A : Type.
  A is declared
Variable P : A -> Type.
  P is declared
Definition projT1 (H:sigT A P) := let (x, h) := H in x.
  projT1 is defined
Definition projT2 (H:sigT A P) := match H return P (projT1 H) with existT _ _ x h => h end.
  projT2 is defined
End Projections2.
Inductive sigT2 (A: Type) (P Q:A -> Type) : Type := existT2 (x:A) (_:P x) (_:Q x).
  sigT2 is defined sigT2_rect is defined sigT2_ind is defined sigT2_rec is defined sigT2_sind is defined

A related non-dependent construct is the constructive sum `{A}+{B}` of two propositions `A` and `B`.

Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
  sumbool is defined sumbool_rect is defined sumbool_ind is defined sumbool_rec is defined sumbool_sind is defined

This `sumbool` construct may be used as a kind of indexed boolean data-type. An intermediate between `sumbool` and `sum` is the mixed `sumor` which combines `A:Set` and `B:Prop` in the construction `A+{B}` in `Set`.

Inductive sumor (A:Set) (B:Prop) : Set := | inleft (_:A) | inright (_:B).
  sumor is defined sumor_rect is defined sumor_ind is defined sumor_rec is defined sumor_sind is defined

We may define variants of the axiom of choice, like in Martin-Löf's Intuitionistic Type Theory.

Lemma Choice : forall (S S':Set) (R:S -> S' -> Prop), (forall x:S, {y : S' | R x y}) -> {f : S -> S' | forall z:S, R z (f z)}. Lemma Choice2 : forall (S S':Set) (R:S -> S' -> Set), (forall x:S, {y : S' & R x y}) -> {f : S -> S' & forall z:S, R z (f z)}. Lemma bool_choice : forall (S:Set) (R1 R2:S -> Prop), (forall x:S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.

The next construct builds a sum between a data-type `A:Type` and an exceptional value encoding errors:

Definition Exc := option.
  Exc is defined
Definition value := Some.
  value is defined
Definition error := None.
  error is defined

This module ends with theorems, relating the sorts `Set` or `Type` and `Prop` in a way which is consistent with the realizability interpretation.

Definition except := False_rec. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Theorem and_rect2 : forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.

### Basic Arithmetic

The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and multiplication, in module `Peano.v`. It also provides a scope `nat_scope` gathering standard notations for common operations (`+`, `*`) and a decimal notation for numbers, allowing, for instance, writing `3` for `S (S (S O))`. This also works on the left hand side of a `match` expression (see for example section `refine`). This scope is opened by default.

Example

The following example is not part of the standard library, but it shows the usage of the notations:

Fixpoint even (n:nat) : bool := match n with | 0 => true | 1 => false | S (S n) => even n end.
  even is defined even is recursively defined (guarded on 1st argument)

Now comes the content of module `Peano`:

Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with | 0 => 0 | S u => u end. Theorem pred_Sn : forall m:nat, m = pred (S m). Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. Hint Immediate eq_add_S : core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Definition IsSucc (n:nat) : Prop := match n with | 0 => False | S p => True end. Theorem O_S : forall n:nat, 0 <> S n. Theorem n_Sn : forall n:nat, n <> S n. Fixpoint plus (n m:nat) {struct n} : nat := match n with | 0 => m | S p => S (p + m) end where "n + m" := (plus n m) : nat_scope. Lemma plus_n_O : forall n:nat, n = n + 0. Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Fixpoint mult (n m:nat) {struct n} : nat := match n with | 0 => 0 | S p => m + p * m end where "n * m" := (mult n m) : nat_scope. Lemma mult_n_O : forall n:nat, 0 = n * 0. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).

Finally, it gives the definition of the usual orderings `le`, `lt`, `ge` and `gt`.

Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope.
  Toplevel input, characters 0-137: > Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default] le is defined le_ind is defined le_sind is defined Toplevel input, characters 0-137: > Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Definition lt (n m:nat) := S n <= m.
  lt is defined
Definition ge (n m:nat) := m <= n.
  ge is defined
Definition gt (n m:nat) := m < n.
  gt is defined

Properties of these relations are not initially known, but may be required by the user from modules `Le` and `Lt`. Finally, `Peano` gives some lemmas allowing pattern matching, and a double induction principle.

Theorem nat_case : forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, (forall n:nat, R 0 n) -> (forall n:nat, R (S n) 0) -> (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.

### Well-founded recursion

The basic library contains the basics of well-founded recursion and well-founded induction, in module `Wf.v`.

Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. Inductive Acc (x:A) : Prop := Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y. Definition well_founded := forall a:A, Acc a. Hypothesis Rwf : well_founded. Theorem well_founded_induction : forall P:A -> Set, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. Theorem well_founded_ind : forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.

The automatically generated scheme `Acc_rect` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the fixpoint equation can be proved.

Section FixPoint. Variable P : A -> Type. Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x := F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)). Definition Fix (x:A) := Fix_F x (Rwf x). Hypothesis F_ext : forall (x:A) (f g:forall y:A, R y x -> P y), (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g. Lemma Fix_F_eq : forall (x:A) (r:Acc x), F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r. Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). End FixPoint. End Well_founded.

### Tactics

A few tactics defined at the user level are provided in the initial state, in module `Tactics` of `Corelib` (documentation).

## Opam repository

Numerous users' contributions have been packaged and are available at URL https://rocq-prover.org/packages/. On this web page, you can browse all contributions with informations (author, institution, quick description, etc.) and the possibility to download their sources or install them with their dependencies through the Opam package manager. You will also find informations on how to submit a new package.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF