\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \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{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \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{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal 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}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

The Coq library

The Coq library is structured into two parts:

• The initial library: it contains elementary logical notions and data-types. It constitutes the basic state of the system directly available when running Coq;
• The standard library: general-purpose libraries containing various developments of Coq axiomatizations about sets, lists, sorting, arithmetic, etc. This library comes with the system and its modules are directly accessible through the Require command (see Section Compiled files);

In addition, user-provided libraries or developments are provided by Coq users' community. These libraries and developments are available for download at http://coq.inria.fr (see Section Users’ contributions).

This chapter briefly reviews the Coq libraries whose contents can also be browsed at http://coq.inria.fr/stdlib.

The basic library

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 at the Coq root directory; this includes the modules Notations, Logic, Datatypes, Specif, Peano, Wf and Tactics. Module Logic_Type also makes it in the initial state.

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

The basic library of Coq comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the subclass form of the syntactic class term. The syntax of form is shown below:

form ::=    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:

Inductive True : Prop := I.

True is defined True_rect is defined True_ind is defined True_rec is defined

Inductive False : Prop := .

False is defined False_rect is defined False_ind is defined False_rec is defined

Definition not (A: Prop) := A -> False.

not is defined

Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).

and is defined and_rect is defined and_ind is defined and_rec is defined

Section Projections.

Variables A B : Prop.

A is declared B is declared

Theorem proj1 : A /\ B -> A.

1 subgoal A, B : Prop ============================ A /\ B -> A

Theorem proj2 : A /\ B -> B.

1 subgoal A, B : Prop ============================ A /\ B -> B

End Projections.

Toplevel input, characters 0-16: > End Projections. > ^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: proj2 proj1. Use "Abort All" first or complete proof(s).

Inductive or (A B:Prop) : Prop := | or_introl (_:A) | or_intror (_:B).

or is defined or_ind is defined

Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).

or is defined or_ind is defined iff is defined

Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.

IF_then_else 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

Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=  ex_intro2 (x:A) (_:P x) (_:Q x).

ex2 is defined ex2_ind 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

Lemmas

Finally, a few easy lemmas are provided.

Theorem absurd : forall A C:Prop, A -> ~ A -> C.

ex is defined ex_ind is defined ex2 is defined ex2_ind is defined eq is defined eq_rect is defined eq_ind is defined eq_rec is defined 1 subgoal A, B : Prop ============================ forall A0 C : Prop, A0 -> ~ A0 -> C

Section equality.

Toplevel input, characters 0-17: > Section equality. > ^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Variables A B : Type.

Toplevel input, characters 0-21: > Variables A B : Type. > ^^^^^^^^^^^^^^^^^^^^^ Error: A already exists.

Variable f : A -> B.

f is declared Variable f is not visible from current goals

Variables x y z : A.

x is declared Variable x is not visible from current goals y is declared Variable y is not visible from current goals z is declared Variable z is not visible from current goals

Theorem eq_sym : x = y -> y = x.

f is declared Variable f is not visible from current goals x is declared Variable x is not visible from current goals y is declared Variable y is not visible from current goals z is declared Variable z is not visible from current goals 1 subgoal A, B : Prop f : A -> B x, y, z : A ============================ x = y -> y = x

Theorem eq_trans : x = y -> y = z -> x = z.

1 subgoal A, B : Prop f : A -> B x, y, z : A ============================ x = y -> y = z -> x = z

Theorem f_equal : x = y -> f x = f y.

1 subgoal A, B : Prop f : A -> B x, y, z : A ============================ x = y -> f x = f y

Theorem not_eq_sym : x <> y -> y <> x.

End equality.

Toplevel input, characters 0-13: > End equality. > ^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Definition eq_ind_r :  forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.

1 subgoal A, B : Prop f : A -> B x, y, z : A ============================ forall (A0 : Type) (x0 : A0) (P : A0 -> Prop), P x0 -> forall y0 : A0, y0 = x0 -> P y0

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 subgoal A, B : Prop f : A -> B x, y, z : A ============================ forall (A1 A2 A3 B0 : Type) (f0 : A1 -> A2 -> A3 -> B0) (x1 y1 : A1) (x2 y2 : A2) (x3 y3 : A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f0 x1 x2 x3 = f0 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):

specif ::=   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)
term   ::=  (term, term)                               (pair)

Programming

Inductive unit : Set := tt.

unit is defined unit_rect is defined unit_ind is defined unit_rec is defined

Inductive bool : Set := true | false.

bool is defined bool_rect is defined bool_ind is defined bool_rec is defined

Inductive nat : Set := O | S (n:nat).

nat is defined nat_rect is defined nat_ind is defined nat_rec 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

Inductive identity (A:Type) (a:A) : A -> Type :=   refl_identity : identity A a a.

identity is defined identity_rect is defined identity_ind is defined identity_rec is defined

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

The predicate identity is logically equivalent to equality but it lives in sort Type. It is mainly maintained for compatibility.

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

Inductive prod (A B:Set) : Set := pair (_:A) (_:B).

prod is defined prod_rect is defined prod_ind is defined prod_rec is defined

Section projections.

Toplevel input, characters 0-20: > Section projections. > ^^^^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Variables A B : Set.

Toplevel input, characters 0-20: > Variables A B : Set. > ^^^^^^^^^^^^^^^^^^^^ Error: A already exists.

Definition fst (H: prod A B) := match H with                               | pair _ _ x y => x                               end.

unit is defined unit_rect is defined unit_ind is defined unit_rec is defined bool is defined bool_rect is defined bool_ind is defined bool_rec is defined nat is defined nat_rect is defined nat_ind is defined nat_rec is defined option is defined option_rect is defined option_ind is defined option_rec is defined identity is defined identity_rect is defined identity_ind is defined identity_rec is defined sum is defined sum_rect is defined sum_ind is defined sum_rec is defined prod is defined prod_rect is defined prod_ind is defined prod_rec is defined fst is defined

Definition snd (H: prod A B) := match H with                               | pair _ _ x y => y                               end.

snd is defined

End projections.

Toplevel input, characters 0-16: > End projections. > ^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

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

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

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

Section Projections2.

Toplevel input, characters 0-21: > Section Projections2. > ^^^^^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Variable A : Type.

Toplevel input, characters 0-18: > Variable A : Type. > ^^^^^^^^^^^^^^^^^^ Error: A already exists.

Variable P : A -> Type.

P is declared Variable P is not visible from current goals

Definition projT1 (H:sigT A P) := let (x, h) := H in x.

sig is defined sig_rect is defined sig_ind is defined sig_rec is defined sig2 is defined sig2_rect is defined sig2_ind is defined sig2_rec is defined sigT is defined sigT_rect is defined sigT_ind is defined sigT_rec is defined P is declared Variable P is not visible from current goals 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.

Toplevel input, characters 0-17: > End Projections2. > ^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

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

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

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

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

sigT2 is defined sigT2_rect is defined sigT2_ind is defined sigT2_rec is defined sumbool is defined sumbool_rect is defined sumbool_ind is defined sumbool_rec is defined sumor is defined sumor_rect is defined sumor_ind is defined sumor_rec is defined 1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ forall (S0 S' : Set) (R : S0 -> S' -> Prop), (forall x0 : S0, {y0 : S' | R x0 y0}) -> {f0 : S0 -> S' | forall z0 : S0, R z0 (f0 z0)}

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

1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ forall (S0 : Set) (R1 R2 : S0 -> Prop), (forall x0 : S0, {R1 x0} + {R2 x0}) -> {f0 : S0 -> bool | forall x0 : S0, f0 x0 = true /\ R1 x0 \/ f0 x0 = false /\ R2 x0}

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.

except is defined

Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.

1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ forall (A0 : Prop) (C : Set), A0 -> ~ A0 -> C

Theorem and_rect2 :  forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.

Basic Arithmetics

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 to write 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.

Toplevel input, characters 62-63: > Fixpoint even (n:nat) : bool := match n with | 0 => true | 1 => false | S (S n) => even n end. > ^ Error: Found a constructor of inductive type Datatypes.nat while a constructor of nat is expected.

Now comes the content of module Peano:

Theorem eq_S : forall x y:nat, x = y -> S x = S y.

1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ forall x0 y0 : nat, x0 = y0 -> S x0 = S y0

Definition pred (n:nat) : nat :=  match n with  | 0 => 0  | S u => u  end.

Toplevel input, characters 50-51: > Definition pred (n:nat) : nat := match n with | 0 => 0 | S u => u end. > ^ Error: Found a constructor of inductive type Datatypes.nat while a constructor of nat is expected.

Theorem pred_Sn : forall m:nat, m = pred (S m).

Toplevel input, characters 42-45: > Theorem pred_Sn : forall m:nat, m = pred (S m). > ^^^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type m : nat The term "S m" has type "nat" while it is expected to have type "Datatypes.nat".

Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.

1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ 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.

Toplevel input, characters 53-54: > Definition IsSucc (n:nat) : Prop := match n with | 0 => False | S p => True end. > ^ Error: Found a constructor of inductive type Datatypes.nat while a constructor of nat is expected.

Theorem O_S : forall n:nat, 0 <> S n.

Toplevel input, characters 33-36: > Theorem O_S : forall n:nat, 0 <> S n. > ^^^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat The term "S n" has type "nat" while it is expected to have type "Datatypes.nat".

Theorem n_Sn : forall n:nat, n <> S n.

1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type ============================ 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.

Toplevel input, characters 0-133: > 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. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation _ + _ was already used in scope nat_scope. [notation-overridden,parsing] Toplevel input, characters 61-62: > 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. > ^ Error: Found a constructor of inductive type Datatypes.nat while a constructor of nat is expected.

Lemma plus_n_O : forall n:nat, n = n + 0.

Toplevel input, characters 35-36: > Lemma plus_n_O : forall n:nat, n = n + 0. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat The term "n" has type "nat" while it is expected to have type "Datatypes.nat".

Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.

Toplevel input, characters 37-38: > Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat m : nat The term "n" has type "nat" while it is expected to have type "Datatypes.nat".

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.

Toplevel input, characters 0-133: > 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. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Notation _ * _ was already used in scope nat_scope. [notation-overridden,parsing] Toplevel input, characters 61-62: > 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. > ^ Error: Found a constructor of inductive type Datatypes.nat while a constructor of nat is expected.

Lemma mult_n_O : forall n:nat, 0 = n * 0.

Toplevel input, characters 35-36: > Lemma mult_n_O : forall n:nat, 0 = n * 0. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat The term "n" has type "nat" while it is expected to have type "Datatypes.nat".

Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).

Toplevel input, characters 34-35: > Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m). > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat m : nat The term "n" has type "nat" while it is expected to have type "Datatypes.nat".

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

Toplevel input, characters 77-78: > Inductive le (n:nat) : nat -> Prop := | le_n : le n n | le_S : forall m:nat, n <= m -> n <= (S m). > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type le : nat -> nat -> Prop n : nat m : nat The term "n" has type "nat" while it is expected to have type "Datatypes.nat".

where "n <= m" := (le n m) : nat_scope.

Toplevel input, characters 0-5: > where "n <= m" := (le n m) : nat_scope. > ^^^^^ Error: Syntax error: illegal begin of vernac.

Definition lt (n m:nat) := S n <= m.

Toplevel input, characters 27-30: > Definition lt (n m:nat) := S n <= m. > ^^^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat m : nat The term "S n" has type "nat" while it is expected to have type "Datatypes.nat".

Definition ge (n m:nat) := m <= n.

Toplevel input, characters 27-28: > Definition ge (n m:nat) := m <= n. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat m : nat The term "m" has type "nat" while it is expected to have type "Datatypes.nat".

Definition gt (n m:nat) := m < n.

Toplevel input, characters 27-28: > Definition gt (n m:nat) := m < n. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat m : nat The term "m" has type "nat" while it is expected to have type "Datatypes.nat".

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.

Toplevel input, characters 55-56: > Theorem nat_case : forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type n : nat P0 : nat -> Prop The term "0" has type "Datatypes.nat" while it is expected to have type "nat".

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.

Toplevel input, characters 74-75: > 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. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : nat -> nat -> Prop n : nat The term "0" has type "Datatypes.nat" while it is expected to have type "nat".

Well-founded recursion

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

Section Well_founded.

Toplevel input, characters 0-21: > Section Well_founded. > ^^^^^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: n_Sn not_eq_S eq_S and_rect2 f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Variable A : Type.

Toplevel input, characters 0-18: > Variable A : Type. > ^^^^^^^^^^^^^^^^^^ Error: A already exists.

Variable R : A -> A -> Prop.

R is declared Variable R is not visible from current goals

Inductive Acc (x:A) : Prop :=   Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

Acc is defined Acc_rect is defined Acc_ind is defined Acc_rec is defined

Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y.

R is declared Variable R is not visible from current goals Acc is defined Acc_rect is defined Acc_ind is defined Acc_rec is defined Toplevel input, characters 0-54: > Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: x is already used.

Definition well_founded := forall a:A, Acc a.

well_founded is defined

Hypothesis Rwf : well_founded.

Rwf is declared Variable Rwf is not visible from current goals

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.

Rwf is declared Variable Rwf is not visible from current goals 1 subgoal A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded ============================ forall P0 : A -> Set, (forall x0 : A, (forall y0 : A, R y0 x0 -> P0 y0) -> P0 x0) -> forall a : A, P0 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.

Toplevel input, characters 0-17: > Section FixPoint. > ^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: well_founded_ind n_Sn not_eq_S eq_S and_rect2 f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Variable P : A -> Type.

Toplevel input, characters 0-23: > Variable P : A -> Type. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: P already exists.

Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.

F is declared Variable F is not visible from current goals

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

Toplevel input, characters 98-99: > 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)). > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x Fix_F : forall x : A, Acc x -> P x x0 : A r : Acc x0 y0 : A p : R y0 x0 The term "x0" has type "A" while it is expected to have type "Wf.Acc ?R ?x".

Definition Fix (x:A) := Fix_F x (Rwf x).

F is declared Variable F is not visible from current goals Toplevel input, characters 30-31: > Definition Fix (x:A) := Fix_F x (Rwf x). > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x x0 : A The term "x0" has type "A" while it is expected to have type "?A -> Type".

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.

F_ext is declared Variable F_ext is not visible from current goals

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.

F_ext is declared Variable F_ext is not visible from current goals Toplevel input, characters 79-80: > 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. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x 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 x0 : A r : Acc x0 y0 : A p : R y0 x0 The term "y0" has type "A" while it is expected to have type "?A0 -> Type".

Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.

Toplevel input, characters 50-51: > Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x 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 x0 : A r : Acc x0 s : Acc x0 The term "x0" has type "A" while it is expected to have type "?A0 -> Type".

Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).

Toplevel input, characters 31-32: > Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x 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 x0 : A The term "x0" has type "A" while it is expected to have type "Wf.well_founded ?R".

End FixPoint.

Toplevel input, characters 0-13: > End FixPoint. > ^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: well_founded_ind n_Sn not_eq_S eq_S and_rect2 f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

End Well_founded.

Toplevel input, characters 0-17: > End Well_founded. > ^^^^^^^^^^^^^^^^^ Error: Proof editing in progress. Proofs currently edited: well_founded_ind n_Sn not_eq_S eq_S and_rect2 f_equal3 not_eq_sym absurd proj2 proj1. Use "Abort All" first or complete proof(s).

Accessing the Type level

The standard library includes Type level definitions of counterparts of some logic concepts and basic lemmas about them.

The module Datatypes defines identity, which is the Type level counterpart of equality:

Inductive identity (A:Type) (a:A) : A -> Type :=   identity_refl : identity a a.

Toplevel input, characters 76-77: > Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. > ^ Error: In environment A, B : Prop f : A -> B x, y, z : A P : A -> Type R : A -> A -> Prop Rwf : well_founded F : forall x : A, (forall y : A, R y x -> P y) -> P x 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 identity : forall A : Type, A -> A -> Type A0 : Type a : A0 The term "a" has type "A0" while it is expected to have type "Type".

Some properties of identity are proved in the module Logic_Type, which also provides the definition of Type level negation:

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

notT is defined

Tactics

A few tactics defined at the user level are provided in the initial state, in module Tactics.v. They are listed at http://coq.inria.fr/stdlib, in paragraph Init, link Tactics.

The standard library

Survey

The rest of 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 co-inductive 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,...)
• 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 (see Section Compiled files).

The different modules of the Coq standard library are documented online at http://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 arithmetics

The following table describes the syntax of expressions for integer arithmetics. 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

Require Import ZArith.

[Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... 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 arithmetics. 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

Require Import Reals.

[Loading ML file r_syntax_plugin.cmxs ... done] [Loading ML file fourier_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done]

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 fourier tactics (see Chapter Tactics), there are also:

discrR

Proves that two real integer constants are different.

Example

Require Import DiscrR.

Open Scope R_scope.

Goal 5 <> 0.

1 subgoal ============================ 5 <> 0

discrR.

No more subgoals.

split_Rabs

Allows unfolding the Rabs constant and splits corresponding conjunctions.

Example

Require Import Reals.

Open Scope R_scope.

Goal forall x:R, x <= Rabs x.

1 subgoal ============================ forall x : R, x <= Rabs x

intro; split_Rabs.

2 subgoals x : R Hlt : x < 0 ============================ x <= - x subgoal 2 is: x <= x

split_Rmult

Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product.

Example

Require Import Reals.

Open Scope R_scope.

Goal forall x y z:R, x * y * z <> 0.

1 subgoal ============================ forall x y z : R, x * y * z <> 0

intros; split_Rmult.

3 subgoals x, y, z : R ============================ x <> 0 subgoal 2 is: y <> 0 subgoal 3 is: z <> 0

These tactics has been written with the tactic language L_tac described in Chapter The tactic language.

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

Users’ contributions

Numerous users' contributions have been collected and are available at URL http://coq.inria.fr/opam/www/. On this web page, you have a list of all contributions with informations (author, institution, quick description, etc.) and the possibility to download them one by one. You will also find informations on how to submit a new contribution.