The Coq library is structured into three parts:
-
The initial library:
- it contains
elementary logical notions and datatypes. 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 6.4.1);
- User contributions:
- Other specification and proof developments
coming from the Coq users' community. These libraries are no
longer distributed with the system. They are available by anonymous
FTP (see section 3.3).
This chapter briefly reviews these libraries.
3.1 The basic library
This section lists the basic notions and results which are directly
available in the standard Coq system
1.
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 precedence and
associativity of very common notations, and avoid users to use them
with other precedence, which may be confusing.
Notation |
Precedence |
Associativity |
_ <-> _ |
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 |
_ * _ |
40 |
left |
_ / _ |
40 |
left |
- _ |
35 |
right |
/ _ |
35 |
right |
_ ^ _ |
30 |
right |
Figure 3.1: Notations in the initial state
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) |
Figure 3.2: Syntax of formulas
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
extension is shown on figure 3.2.
Remark: 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:
Coq < Inductive True : Prop := I.
Coq < Inductive False : Prop := .
Coq < Definition not (A: Prop) := A -> False.
Coq < Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
Coq < Section Projections.
Coq < Variables A B : Prop.
Coq < Theorem proj1 : A /\ B -> A.
Coq < Theorem proj2 : A /\ B -> B.
Coq < End Projections.
Coq < Inductive or (A B:Prop) : Prop :=
Coq < | or_introl (_:A)
Coq < | or_intror (_:B).
Coq < Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
Coq < Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Quantifiers
Then we find first-order quantifiers:
Coq < Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
Coq < Inductive ex (A: Set) (P:A -> Prop) : Prop :=
Coq < ex_intro (x:A) (_:P x).
Coq < Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
Coq < ex_intro2 (x:A) (_:P x) (_:Q x).
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.
Coq < Inductive eq (A:Type) (x:A) : A -> Prop :=
Coq < refl_equal : eq A x x.
Lemmas
Finally, a few easy lemmas are provided.
Coq < Theorem absurd : forall A C:Prop, A -> ~ A -> C.
Coq < Section equality.
Coq < Variables A B : Type.
Coq < Variable f : A -> B.
Coq < Variables x y z : A.
Coq < Theorem sym_eq : x = y -> y = x.
Coq < Theorem trans_eq : x = y -> y = z -> x = z.
Coq < Theorem f_equal : x = y -> f x = f y.
Coq < Theorem sym_not_eq : x <> y -> y <> x.
Coq < End equality.
Coq < Definition eq_ind_r :
Coq < forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
Coq < Definition eq_rec_r :
Coq < forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
Coq < Definition eq_rect_r :
Coq < forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
Coq < Hint Immediate sym_eq sym_not_eq : 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.
Coq < Theorem f_equal3 :
Coq < forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
Coq < (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
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 } |
(sigS) |
|
| |
{ ident : specif & specif & specif } |
(sigS2) |
|
|
|
|
term |
::= |
( term , term ) |
(pair) |
Figure 3.3: Syntax of datatypes and specifications
In the basic library, we find the definition2 of the basic data-types of programming, again
defined as inductive constructions over the sort Set
. Some of
them come with a special syntax shown on Figure 3.3.
Programming
Coq < Inductive unit : Set := tt.
Coq < Inductive bool : Set := true | false.
Coq < Inductive nat : Set := O | S (n:nat).
Coq < Inductive option (A:Set) : Set := Some (_:A) | None.
Coq < Inductive identity (A:Type) (a:A) : A -> Type :=
Coq < refl_identity : identity A a a.
Note that zero is the letter O
, and not the numeral
0
.
identity is logically equivalent to equality but it lives in
sort Set. Computationaly, it behaves like unit.
We then define the disjoint sum of A+B
of two sets A
and
B
, and their product A*B
.
Coq < Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
Coq < Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
Coq < Section projections.
Coq < Variables A B : Set.
Coq < Definition fst (H: prod A B) := match H with
Coq < | pair x y => x
Coq < end.
Coq < Definition snd (H: prod A B) := match H with
Coq < | pair x y => y
Coq < end.
Coq < End projections.
3.1.4 Specification
The following notions3 allows to build new datatypes and specifications.
They are available with the syntax shown on
Figure 3.34.
For instance, given A:Set
and P:A->Prop
, the construct
{x:A | P x}
(in abstract syntax (sig A P)
) is a
Set
. 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.
Coq < Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
Coq < Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
Coq < exist2 (x:A) (_:P x) (_:Q x).
A ``strong (dependent) sum'' {x:A & (P x)}
may be also defined,
when the predicate P
is now defined as a Set
constructor.
Coq < Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x).
Coq < Section sigSprojections.
Coq < Variable A : Set.
Coq < Variable P : A -> Set.
Coq < Definition projS1 (H:sigS A P) := let (x, h) := H in x.
Coq < Definition projS2 (H:sigS A P) :=
Coq < match H return P (projS1 H) with
Coq < existS x h => h
Coq < end.
Coq < End sigSprojections.
Coq < Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
Coq < existS2 (x:A) (_:P x) (_:Q x).
A related non-dependent construct is the constructive sum
{A}+{B}
of two propositions A
and B
.
Coq < Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
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 Set
A+{B}
.
Coq < Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
We may define variants of the axiom of choice, like in Martin-Löf's
Intuitionistic Type Theory.
Coq < Lemma Choice :
Coq < forall (S S':Set) (R:S -> S' -> Prop),
Coq < (forall x:S, {y : S' | R x y}) ->
Coq < {f : S -> S' | forall z:S, R z (f z)}.
Coq < Lemma Choice2 :
Coq < forall (S S':Set) (R:S -> S' -> Set),
Coq < (forall x:S, {y : S' & R x y}) ->
Coq < {f : S -> S' & forall z:S, R z (f z)}.
Coq < Lemma bool_choice :
Coq < forall (S:Set) (R1 R2:S -> Prop),
Coq < (forall x:S, {R1 x} + {R2 x}) ->
Coq < {f : S -> bool |
Coq < forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
The next constructs builds a sum between a data type A:Set
and
an exceptional value encoding errors:
Coq < Definition Exc := option.
Coq < Definition value := Some.
Coq < Definition error := None.
This module ends with theorems,
relating the sorts Set
and
Prop
in a way which is consistent with the realizability
interpretation.
Coq < Definition except := False_rec.
Coq < Notation Except := (except _).
Coq < Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
Coq < Theorem and_rec :
Coq < forall (A B:Prop) (P:Set), (A -> B -> P) -> A /\ B -> P.
3.1.5 Basic Arithmetics
The basic library includes a few elementary properties of natural
numbers, together with the definitions of predecessor, addition and
multiplication5. It also
provides a scope nat_scope gathering standard notations for
common operations (+,*) and a decimal notation for numbers. That is he
can write 3 for (S (S (S O))). This also works on
the left hand side of a match expression (see for example
section 10.1). This scope is opened by default.
The following example is not part of the standard library, but it
shows the usage of the notations:
Coq < Fixpoint even (n:nat) : bool :=
Coq < match n with
Coq < | 0 => true
Coq < | 1 => false
Coq < | S (S n) => even n
Coq < end.
Coq < Theorem eq_S : forall x y:nat, x = y -> S x = S y.
Coq < Definition pred (n:nat) : nat :=
Coq < match n with
Coq < | 0 => 0
Coq < | S u => u
Coq < end.
Coq < Theorem pred_Sn : forall m:nat, m = pred (S m).
Coq < Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
Coq < Hint Immediate eq_add_S : core.
Coq < Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
Coq < Definition IsSucc (n:nat) : Prop :=
Coq < match n with
Coq < | 0 => False
Coq < | S p => True
Coq < end.
Coq < Theorem O_S : forall n:nat, 0 <> S n.
Coq < Theorem n_Sn : forall n:nat, n <> S n.
Coq < Fixpoint plus (n m:nat) {struct n} : nat :=
Coq < match n with
Coq < | 0 => m
Coq < | S p => S (plus p m)
Coq < end.
Coq < Lemma plus_n_O : forall n:nat, n = plus n 0.
Coq < Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m).
Coq < Fixpoint mult (n m:nat) {struct n} : nat :=
Coq < match n with
Coq < | 0 => 0
Coq < | S p => m + mult p m
Coq < end.
Coq < Lemma mult_n_O : forall n:nat, 0 = mult n 0.
Coq < Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m).
Finally, it gives the definition of the usual orderings le
,
lt
, ge
, and gt
.
Coq < Inductive le (n:nat) : nat -> Prop :=
Coq < | le_n : le n n
Coq < | le_S : forall m:nat, le n m -> le n (S m).
Coq < Infix "+" := plus : nat_scope.
Coq < Definition lt (n m:nat) := S n <= m.
Coq < Definition ge (n m:nat) := m <= n.
Coq < Definition gt (n m:nat) := m < n.
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.
Coq < Theorem nat_case :
Coq < forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
Coq < Theorem nat_double_ind :
Coq < forall R:nat -> nat -> Prop,
Coq < (forall n:nat, R 0 n) ->
Coq < (forall n:nat, R (S n) 0) ->
Coq < (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
3.1.6 Well-founded recursion
The basic library contains the basics of well-founded recursion and
well-founded induction6.
Coq < Section Well_founded.
Coq < Variable A : Set.
Coq < Variable R : A -> A -> Prop.
Coq < Inductive Acc : A -> Prop :=
Coq < Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
Coq < Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
Coq < Section AccRec.
Coq < Variable P : A -> Set.
Coq < Variable F :
Coq < forall x:A,
Coq < (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
Coq < Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
Coq < F x (Acc_inv x a)
Coq < (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
Coq < End AccRec.
Coq < Definition well_founded := forall a:A, Acc a.
Coq < Hypothesis Rwf : well_founded.
Coq < Theorem well_founded_induction :
Coq < forall P:A -> Set,
Coq < (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Coq < Theorem well_founded_ind :
Coq < forall P:A -> Prop,
Coq < (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Acc_rec 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.
Coq < Section FixPoint.
Coq < Variable P : A -> Set.
Coq < Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
Coq < Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
Coq < F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
Coq < Definition Fix (x:A) := Fix_F x (Rwf x).
Coq < Hypothesis F_ext :
Coq < forall (x:A) (f g:forall y:A, R y x -> P y),
Coq < (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
Coq < Lemma Fix_F_eq :
Coq < forall (x:A) (r:Acc x),
Coq < F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
Coq < Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
Coq < Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
Coq < End FixPoint.
Coq < End Well_founded.
3.1.7 Accessing the Type level
The basic library includes the definitions7 of the counterparts of some datatypes and logical
quantifiers at the Type
level: negation, pair, and properties
of identity.
Coq < Definition notT (A:Type) := A -> False.
Coq < Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
At the end, it defines datatypes at the Type level.
3.2 The standard library
The rest of the standard library is structured into the following
subdirectories:
Logic |
Classical logic and dependent equality |
Arith |
Basic Peano arithmetic |
ZArith |
Basic integer arithmetic |
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.) |
IntMap |
Representation of finite sets by an efficient
structure of map (trees indexed by binary integers). |
Reals |
Axiomatization of Real Numbers (classical, basic functions,
integer part, fractional part, limit, derivative, Cauchy
series, power series and results,... Requires the
ZArith library). |
Relations |
Relations (definitions and basic results). |
Sorting |
Sorted list (basic definitions and heapsort correctness). |
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
chapter 6).
The different modules of the Coq standard library are described in the
additional document Library.dvi
. They are also accessible on the WWW
through the Coq homepage
8.
3.2.2 Notations for integer arithmetics
On figure 3.2.2 is described the syntax of expressions
for integer arithmetics. It is provided by requiring and opening the
module ZArith and opening scope Z_scope.
Notation |
Interpretation |
Precedence |
Associativity |
_ < _ |
Zlt |
|
|
x <= y |
Zle |
|
|
_ > _ |
Zgt |
|
|
x >= y |
Zge |
|
|
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 |
|
|
_ ?= _ |
Zcompare |
70 |
no |
_ + _ |
Zplus |
|
|
_ - _ |
Zminus |
|
|
_ * _ |
Zmult |
|
|
_ / _ |
Zdiv |
|
|
_ mod _ |
Zmod |
40 |
no |
- _ |
Zopp |
|
|
_ ^ _ |
Zpower |
|
|
Figure 3.4: Definition of the scope for integer arithmetics (Z_scope)
Figure 3.2.2 shows the notations provided by Z_scope. It specifies how notations are interpreted and, when not
already reserved, the precedence and associativity.
Coq < Require Import ZArith.
Coq < Check (2 + 3)%Z.
(2 + 3)%Z
: Z
Coq < Open Scope Z_scope.
Coq < Check 2 + 3.
2 + 3
: Z
3.2.3 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.
Figure 3.2.3 describes notation available in scope nat_scope.
Notation |
Interpretation |
_ < _ |
lt |
x <= y |
le |
_ > _ |
gt |
x >= y |
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 |
Figure 3.5: Definition of the scope for natural numbers (nat_scope)
3.2.4 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 |
x <= y |
Rle |
_ > _ |
Rgt |
x >= y |
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 |
Figure 3.6: Definition of the scope for real arithmetics (R_scope)
Coq < Require Import Reals.
Coq < Check (2 + 3)%R.
(2 + 3)%R
: R
Coq < Open Scope R_scope.
Coq < Check 2 + 3.
2 + 3
: R
Some tactics
In addition to the ring
, field
and fourier
tactics (see Chapter 8) there are:
-
discrR
Proves that a real integer constant c1 is different from another
real integer constant c2.
Coq < Require Import DiscrR.
Coq < Goal 5 <> 0.
Coq < discrR.
Proof completed.
- split_Rabs allows to unfold Rabs constant and splits
corresponding conjonctions.
Coq < Require Import SplitAbsolu.
Coq < Goal forall x:R, x <= Rabs x.
Coq < intro; split_Rabs.
2 subgoals
x : R
r : x < 0
============================
x <= - x
subgoal 2 is:
x <= x
- split_Rmult allows to split a condition that a product is
non null into subgoals corresponding to the condition on each
operand of the product.
Coq < Require Import SplitRmult.
Coq < Goal forall x y z:R, x * y * z <> 0.
Coq < intros; split_Rmult.
3 subgoals
x : R
y : R
z : R
============================
x <> 0
subgoal 2 is:
y <> 0
subgoal 3 is:
z <> 0
All this tactics has been written with the tactic language Ltac
described in Chapter 9. More details are available
in document http://coq.inria.fr/~desmettr/Reals.ps.
3.2.5 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 |
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) |
Table show notations available when opening scope list_scope.
Notation |
Interpretation |
Precedence |
Associativity |
_ ++ _ |
app |
60 |
right |
_ :: _ |
cons |
60 |
right |
Figure 3.7: Definition of the scope for lists (list_scope)
3.3 Users' contributions
Numerous users' contributions have been collected and are available at
URL coq.inria.fr/contribs/. 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.
There is a small search engine to look for keywords in all
contributions. You will also find informations on how to submit a new
contribution.
The users' contributions may also be obtained by anonymous FTP from site
ftp.inria.fr
, in directory INRIA/coq/
and
searchable on-line at http://coq.inria.fr/contribs-eng.html
- 1
- 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,
and Wf.
Module Logic_Type also makes it in the initial state
- 2
- They are in Datatypes.v
- 3
- They are defined in module Specif.v
- 4
- This syntax can be found in the module
SpecifSyntax.v
- 5
- This is in module Peano.v
- 6
- This is defined in module Wf.v
- 7
- This is in module
Logic_Type.v
- 8
- http://coq.inria.fr