diff options
author | 2018-03-15 15:30:36 +0100 | |
---|---|---|
committer | 2018-03-15 15:30:36 +0100 | |
commit | 5370917e88bd9936c34e218c6db9fd82b262d863 (patch) | |
tree | 5d72460929a2d2f989ddb813df7741cea2792c03 /doc | |
parent | fc7d5f49ec7aab1454cb0df10ea244af745b696d (diff) | |
parent | e3750fc9b94f003ea9b9474345925e7f6fcf57de (diff) |
Merge PR #6997: Sphinx doc chapter 3
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-lib.tex | 1112 | ||||
-rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
-rw-r--r-- | doc/sphinx/index.rst | 1 | ||||
-rw-r--r-- | doc/sphinx/language/coq-library.rst | 988 |
4 files changed, 989 insertions, 1113 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex deleted file mode 100644 index 89f5be843..000000000 --- a/doc/refman/RefMan-lib.tex +++ /dev/null @@ -1,1112 +0,0 @@ -\chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}} -%HEVEA\cutname{stdlib.html} - -The \Coq\ library is structured into two parts: - -\begin{description} -\item[The initial library:] it contains - elementary logical notions and data-types. It constitutes the - basic state of the system directly available when running - \Coq; - -\item[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 \verb!Require! command - (see Section~\ref{Require}); -\end{description} - -In addition, user-provided libraries or developments are provided by -\Coq\ users' community. These libraries and developments are available -for download at \url{http://coq.inria.fr} (see -Section~\ref{Contributions}). - -The chapter briefly reviews the \Coq\ libraries whose contents can -also be browsed at \url{http://coq.inria.fr/stdlib}. - -\section[The basic library]{The basic library\label{Prelude}} - -This section lists the basic notions and results which are directly -available in the standard \Coq\ system\footnote{Most -of these constructions are defined in the -{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq} -root directory; this includes the modules -{\tt Notations}, -{\tt Logic}, -{\tt Datatypes}, -{\tt Specif}, -{\tt Peano}, -{\tt Wf} and -{\tt Tactics}. -Module {\tt Logic\_Type} also makes it in the initial state}. - -\subsection[Notations]{Notations\label{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 listed on -Figure~\ref{init-notations}. - -\begin{figure} -\begin{center} -\begin{tabular}{|cll|} -\hline -Notation & Precedence & Associativity \\ -\hline -\verb!_ -> _! & 99 & right \\ -\verb!_ <-> _! & 95 & no \\ -\verb!_ \/ _! & 85 & right \\ -\verb!_ /\ _! & 80 & right \\ -\verb!~ _! & 75 & right \\ -\verb!_ = _! & 70 & no \\ -\verb!_ = _ = _! & 70 & no \\ -\verb!_ = _ :> _! & 70 & no \\ -\verb!_ <> _! & 70 & no \\ -\verb!_ <> _ :> _! & 70 & no \\ -\verb!_ < _! & 70 & no \\ -\verb!_ > _! & 70 & no \\ -\verb!_ <= _! & 70 & no \\ -\verb!_ >= _! & 70 & no \\ -\verb!_ < _ < _! & 70 & no \\ -\verb!_ < _ <= _! & 70 & no \\ -\verb!_ <= _ < _! & 70 & no \\ -\verb!_ <= _ <= _! & 70 & no \\ -\verb!_ + _! & 50 & left \\ -\verb!_ || _! & 50 & left \\ -\verb!_ - _! & 50 & left \\ -\verb!_ * _! & 40 & left \\ -\verb!_ && _! & 40 & left \\ -\verb!_ / _! & 40 & left \\ -\verb!- _! & 35 & right \\ -\verb!/ _! & 35 & right \\ -\verb!_ ^ _! & 30 & right \\ -\hline -\end{tabular} -\end{center} -\caption{Notations in the initial state} -\label{init-notations} -\end{figure} - -\subsection[Logic]{Logic\label{Logic}} - -\begin{figure} -\begin{centerframe} -\begin{tabular}{lclr} -{\form} & ::= & {\tt True} & ({\tt True})\\ - & $|$ & {\tt False} & ({\tt False})\\ - & $|$ & {\tt\char'176} {\form} & ({\tt not})\\ - & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\ - & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\ - & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\ - & $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\ - & $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,} - {\form} & (\em{primitive for all})\\ - & $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt - ,} {\form} & ({\tt ex})\\ - & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt - ,} {\form} {\tt \&} {\form} & ({\tt ex2})\\ - & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\ - & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq}) -\end{tabular} -\end{centerframe} -\caption{Syntax of formulas} -\label{formulas-syntax} -\end{figure} - -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~\ref{formulas-syntax}. - -% 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 \footnote{This syntax is defined in module {\tt -% LogicSyntax}} is shown on Figure~\ref{formulas-syntax}. - -\Rem 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. - -\subsubsection[Propositional Connectives]{Propositional Connectives\label{Connectives} -\index{Connectives}} - -First, we find propositional calculus connectives: -\ttindex{True} -\ttindex{I} -\ttindex{False} -\ttindex{not} -\ttindex{and} -\ttindex{conj} -\ttindex{proj1} -\ttindex{proj2} - -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -\begin{coq_example*} -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{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -End Projections. -\end{coq_example*} -\ttindex{or} -\ttindex{or\_introl} -\ttindex{or\_intror} -\ttindex{iff} -\ttindex{IF\_then\_else} -\begin{coq_example*} -Inductive or (A B:Prop) : Prop := - | or_introl (_:A) - | or_intror (_:B). -Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P). -Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. -\end{coq_example*} - -\subsubsection[Quantifiers]{Quantifiers\label{Quantifiers} -\index{Quantifiers}} - -Then we find first-order quantifiers: -\ttindex{all} -\ttindex{ex} -\ttindex{exists} -\ttindex{ex\_intro} -\ttindex{ex2} -\ttindex{exists2} -\ttindex{ex\_intro2} - -\begin{coq_example*} -Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. -Inductive ex (A: Set) (P:A -> Prop) : Prop := - ex_intro (x:A) (_:P x). -Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop := - ex_intro2 (x:A) (_:P x) (_:Q x). -\end{coq_example*} - -The following abbreviations are allowed: -\begin{center} - \begin{tabular}[h]{|l|l|} - \hline - \verb+exists x:A, P+ & \verb+ex A (fun x:A => P)+ \\ - \verb+exists x, P+ & \verb+ex _ (fun x => P)+ \\ - \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\ - \verb+exists2 x, P & Q+ & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\ - \hline - \end{tabular} -\end{center} - -The type annotation ``\texttt{:A}'' can be omitted when \texttt{A} can be -synthesized by the system. - -\subsubsection[Equality]{Equality\label{Equality} -\index{Equality}} - -Then, we find equality, defined as an inductive relation. That is, -given a type \verb:A: and an \verb:x: of type \verb:A:, the -predicate \verb:(eq A x): is the smallest one which contains \verb:x:. -This definition, due to Christine Paulin-Mohring, is equivalent to -define \verb:eq: as the smallest reflexive relation, and it is also -equivalent to Leibniz' equality. - -\ttindex{eq} -\ttindex{eq\_refl} - -\begin{coq_example*} -Inductive eq (A:Type) (x:A) : A -> Prop := - eq_refl : eq A x x. -\end{coq_example*} - -\subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}} - -Finally, a few easy lemmas are provided. - -\ttindex{absurd} - -\begin{coq_example*} -Theorem absurd : forall A C:Prop, A -> ~ A -> C. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} -\ttindex{eq\_sym} -\ttindex{eq\_trans} -\ttindex{f\_equal} -\ttindex{sym\_not\_eq} -\begin{coq_example*} -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{coq_example*} -\begin{coq_eval} -Abort. -Abort. -Abort. -Abort. -\end{coq_eval} -\ttindex{eq\_ind\_r} -\ttindex{eq\_rec\_r} -\ttindex{eq\_rect} -\ttindex{eq\_rect\_r} -%Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y). -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort. -Abort. -Abort. -\end{coq_eval} -%Abort (for now predefined eq_rect) -\begin{coq_example*} -Hint Immediate eq_sym not_eq_sym : core. -\end{coq_example*} -\ttindex{f\_equal$i$} - -The theorem {\tt f\_equal} is extended to functions with two to five -arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, -{\tt f\_equal4} and {\tt f\_equal5}. -For instance {\tt f\_equal3} is defined the following way. -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection[Datatypes]{Datatypes\label{Datatypes} -\index{Datatypes}} - -\begin{figure} -\begin{centerframe} -\begin{tabular}{rclr} -{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\ - & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\ - & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\ - & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} & - ({\tt sumbool})\\ - & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}} - & ({\tt sig})\\ - & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \&} - {\form} {\tt \}} & ({\tt sig2})\\ - & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt - \}} & ({\tt sigT})\\ - & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt - \&} {\specif} {\tt \}} & ({\tt sigT2})\\ - & & & \\ -{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair}) -\end{tabular} -\end{centerframe} -\caption{Syntax of data-types and specifications} -\label{specif-syntax} -\end{figure} - - -In the basic library, we find the definition\footnote{They are in {\tt - Datatypes.v}} of the basic data-types of programming, again -defined as inductive constructions over the sort \verb:Set:. Some of -them come with a special syntax shown on Figure~\ref{specif-syntax}. - -\subsubsection[Programming]{Programming\label{Programming} -\index{Programming} -\label{libnats} -\ttindex{unit} -\ttindex{tt} -\ttindex{bool} -\ttindex{true} -\ttindex{false} -\ttindex{nat} -\ttindex{O} -\ttindex{S} -\ttindex{option} -\ttindex{Some} -\ttindex{None} -\ttindex{identity} -\ttindex{refl\_identity}} - -\begin{coq_example*} -Inductive unit : Set := tt. -Inductive bool : Set := true | false. -Inductive nat : Set := O | S (n:nat). -Inductive option (A:Set) : Set := Some (_:A) | None. -Inductive identity (A:Type) (a:A) : A -> Type := - refl_identity : identity A a a. -\end{coq_example*} - -Note that zero is the letter \verb:O:, and {\sl not} the numeral -\verb:0:. - -The predicate {\tt identity} is logically -equivalent to equality but it lives in sort {\tt - Type}. It is mainly maintained for compatibility. - -We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and -\verb:B:, and their product \verb:A*B:. -\ttindex{sum} -\ttindex{A+B} -\ttindex{+} -\ttindex{inl} -\ttindex{inr} -\ttindex{prod} -\ttindex{A*B} -\ttindex{*} -\ttindex{pair} -\ttindex{fst} -\ttindex{snd} - -\begin{coq_example*} -Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B). -Inductive prod (A B:Set) : Set := pair (_:A) (_:B). -Section projections. -Variables A B : Set. -Definition fst (H: prod A B) := match H with - | pair _ _ x y => x - end. -Definition snd (H: prod A B) := match H with - | pair _ _ x y => y - end. -End projections. -\end{coq_example*} - -Some operations on {\tt bool} are also provided: {\tt andb} (with -infix notation {\tt \&\&}), {\tt orb} (with -infix notation {\tt ||}), {\tt xorb}, {\tt implb} and {\tt negb}. - -\subsection{Specification} - -The following notions\footnote{They are defined in module {\tt -Specif.v}} allow to build new data-types and specifications. -They are available with the syntax shown on -Figure~\ref{specif-syntax}. - -For instance, given \verb|A:Type| and \verb|P:A->Prop|, the construct -\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a -\verb:Type:. We may build elements of this set as \verb:(exist x p): -whenever we have a witness \verb|x:A| with its justification -\verb|p:P x|. - -From such a \verb:(exist x p): we may in turn extract its witness -\verb|x:A| (using an elimination construct such as \verb:match:) but -{\sl not} its justification, which stays hidden, like in an abstract -data-type. In technical terms, one says that \verb:sig: is a ``weak -(dependent) sum''. A variant \verb:sig2: with two predicates is also -provided. - -\ttindex{\{x:A $\mid$ (P x)\}} -\ttindex{sig} -\ttindex{exist} -\ttindex{sig2} -\ttindex{exist2} - -\begin{coq_example*} -Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). -Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := - exist2 (x:A) (_:P x) (_:Q x). -\end{coq_example*} - -A ``strong (dependent) sum'' \verb+{x:A & P x}+ may be also defined, -when the predicate \verb:P: is now defined as a -constructor of types in \verb:Type:. - -\ttindex{\{x:A \& (P x)\}} -\ttindex{\&} -\ttindex{sigT} -\ttindex{existT} -\ttindex{projT1} -\ttindex{projT2} -\ttindex{sigT2} -\ttindex{existT2} - -\begin{coq_example*} -Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x). -Section Projections2. -Variable A : Type. -Variable P : A -> Type. -Definition projT1 (H:sigT A P) := let (x, h) := H in x. -Definition projT2 (H:sigT A P) := - match H return P (projT1 H) with - existT _ _ x h => h - end. -End Projections2. -Inductive sigT2 (A: Type) (P Q:A -> Type) : Type := - existT2 (x:A) (_:P x) (_:Q x). -\end{coq_example*} - -A related non-dependent construct is the constructive sum -\verb"{A}+{B}" of two propositions \verb:A: and \verb:B:. -\label{sumbool} -\ttindex{sumbool} -\ttindex{left} -\ttindex{right} -\ttindex{\{A\}+\{B\}} - -\begin{coq_example*} -Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B). -\end{coq_example*} - -This \verb"sumbool" construct may be used as a kind of indexed boolean -data-type. An intermediate between \verb"sumbool" and \verb"sum" is -the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop" -in the \verb"Set" \verb"A+{B}". -\ttindex{sumor} -\ttindex{inleft} -\ttindex{inright} -\ttindex{A+\{B\}} - -\begin{coq_example*} -Inductive sumor (A:Set) (B:Prop) : Set := -| inleft (_:A) -| inright (_:B). -\end{coq_example*} - -We may define variants of the axiom of choice, like in Martin-Löf's -Intuitionistic Type Theory. -\ttindex{Choice} -\ttindex{Choice2} -\ttindex{bool\_choice} - -\begin{coq_example*} -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}. -\end{coq_example*} -\begin{coq_eval} -Abort. -Abort. -Abort. -\end{coq_eval} - -The next construct builds a sum between a data-type \verb|A:Type| and -an exceptional value encoding errors: - -\ttindex{Exc} -\ttindex{value} -\ttindex{error} - -\begin{coq_example*} -Definition Exc := option. -Definition value := Some. -Definition error := None. -\end{coq_example*} - - -This module ends with theorems, -relating the sorts \verb:Set: or \verb:Type: and -\verb:Prop: in a way which is consistent with the realizability -interpretation. -\ttindex{False\_rect} -\ttindex{False\_rec} -\ttindex{eq\_rect} -\ttindex{absurd\_set} -\ttindex{and\_rect} - -\begin{coq_example*} -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. -\end{coq_example*} -%\begin{coq_eval} -%Abort. -%Abort. -%\end{coq_eval} - -\subsection{Basic Arithmetics} - -The basic library includes a few elementary properties of natural -numbers, together with the definitions of predecessor, addition and -multiplication\footnote{This is in module {\tt Peano.v}}. It also -provides a scope {\tt nat\_scope} gathering standard notations for -common operations (+, *) and a decimal notation for numbers. That is he -can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on -the left hand side of a \texttt{match} expression (see for example -section~\ref{refine-example}). This scope is opened by default. - -%Remove the redefinition of nat -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -The following example is not part of the standard library, but it -shows the usage of the notations: - -\begin{coq_example*} -Fixpoint even (n:nat) : bool := - match n with - | 0 => true - | 1 => false - | S (S n) => even n - end. -\end{coq_example*} - - -\ttindex{eq\_S} -\ttindex{pred} -\ttindex{pred\_Sn} -\ttindex{eq\_add\_S} -\ttindex{not\_eq\_S} -\ttindex{IsSucc} -\ttindex{O\_S} -\ttindex{n\_Sn} -\ttindex{plus} -\ttindex{plus\_n\_O} -\ttindex{plus\_n\_Sm} -\ttindex{mult} -\ttindex{mult\_n\_O} -\ttindex{mult\_n\_Sm} - -\begin{coq_example*} -Theorem eq_S : forall x y:nat, x = y -> S x = S y. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -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). -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} - -Finally, it gives the definition of the usual orderings \verb:le:, -\verb:lt:, \verb:ge:, and \verb:gt:. -\ttindex{le} -\ttindex{le\_n} -\ttindex{le\_S} -\ttindex{lt} -\ttindex{ge} -\ttindex{gt} - -\begin{coq_example*} -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. -Definition lt (n m:nat) := S n <= m. -Definition ge (n m:nat) := m <= n. -Definition gt (n m:nat) := m < n. -\end{coq_example*} - -Properties of these relations are not initially known, but may be -required by the user from modules \verb:Le: and \verb:Lt:. Finally, -\verb:Peano: gives some lemmas allowing pattern-matching, and a double -induction principle. - -\ttindex{nat\_case} -\ttindex{nat\_double\_ind} - -\begin{coq_example*} -Theorem nat_case : - forall (n:nat) (P:nat -> Prop), - P 0 -> (forall m:nat, P (S m)) -> P n. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} - -\subsection{Well-founded recursion} - -The basic library contains the basics of well-founded recursion and -well-founded induction\footnote{This is defined in module {\tt Wf.v}}. -\index{Well foundedness} -\index{Recursion} -\index{Well founded induction} -\ttindex{Acc} -\ttindex{Acc\_inv} -\ttindex{Acc\_rect} -\ttindex{well\_founded} - -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -destruct 1; trivial. -Defined. -\end{coq_eval} -%% Acc_rect now primitively defined -%% Section AccRec. -%% Variable P : A -> Set. -%% Variable F : -%% forall x:A, -%% (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. -%% Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x := -%% F x (Acc_inv x a) -%% (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)). -%% End AccRec. -\begin{coq_example*} -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. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -The automatically generated scheme {\tt 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. -\ttindex{Fix\_F} -\ttindex{fix\_eq} -\ttindex{Fix\_F\_inv} -\ttindex{Fix\_F\_eq} -\begin{coq_example*} -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{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\begin{coq_example*} -End FixPoint. -End Well_founded. -\end{coq_example*} - -\subsection{Accessing the {\Type} level} - -The basic library includes the definitions\footnote{This is in module -{\tt Logic\_Type.v}} of the counterparts of some data-types and logical -quantifiers at the \verb:Type: level: negation, pair, and properties -of {\tt identity}. - -\ttindex{notT} -\ttindex{prodT} -\ttindex{pairT} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Definition notT (A:Type) := A -> False. -Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). -\end{coq_example*} - -At the end, it defines data-types at the {\Type} level. - -\subsection{Tactics} - -A few tactics defined at the user level are provided in the initial -state\footnote{This is in module {\tt Tactics.v}}. They are listed at -\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt - Tactics}). - -\section{The standard library} - -\subsection{Survey} - -The rest of the standard library is structured into the following -subdirectories: - -\begin{tabular}{lp{12cm}} - {\bf Logic} & Classical logic and dependent equality \\ - {\bf Arith} & Basic Peano arithmetic \\ - {\bf PArith} & Basic positive integer arithmetic \\ - {\bf NArith} & Basic binary natural number arithmetic \\ - {\bf ZArith} & Basic relative integer arithmetic \\ - {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\ - {\bf Bool} & Booleans (basic functions and results) \\ - {\bf Lists} & Monomorphic and polymorphic lists (basic functions and - results), Streams (infinite sequences defined with co-inductive - types) \\ - {\bf Sets} & Sets (classical, constructive, finite, infinite, power set, - etc.) \\ - {\bf FSets} & Specification and implementations of finite sets and finite - maps (by lists and by AVL trees)\\ - {\bf Reals} & Axiomatization of real numbers (classical, basic functions, - integer part, fractional part, limit, derivative, Cauchy - series, power series and results,...)\\ - {\bf Relations} & Relations (definitions and basic results) \\ - {\bf Sorting} & Sorted list (basic definitions and heapsort correctness) \\ - {\bf Strings} & 8-bits characters and strings\\ - {\bf Wellfounded} & Well-founded relations (basic results) \\ - -\end{tabular} -\medskip - -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 \verb!Require! (see -Chapter~\ref{Other-commands}). - -The different modules of the \Coq\ standard library are described in the -additional document \verb!Library.dvi!. They are also accessible on the WWW -through the \Coq\ homepage -\footnote{\url{http://coq.inria.fr}}. - -\subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}} - -On Figure~\ref{zarith-syntax} is described the syntax of expressions -for integer arithmetics. It is provided by requiring and opening the -module {\tt ZArith} and opening scope {\tt Z\_scope}. - -\ttindex{+} -\ttindex{*} -\ttindex{-} -\ttindex{/} -\ttindex{<=} -\ttindex{>=} -\ttindex{<} -\ttindex{>} -\ttindex{?=} -\ttindex{mod} - -\begin{figure} -\begin{center} -\begin{tabular}{l|l|l|l} -Notation & Interpretation & Precedence & Associativity\\ -\hline -\verb!_ < _! & {\tt Z.lt} &&\\ -\verb!x <= y! & {\tt Z.le} &&\\ -\verb!_ > _! & {\tt Z.gt} &&\\ -\verb!x >= y! & {\tt Z.ge} &&\\ -\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\ -\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\ -\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\ -\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\ -\verb!_ ?= _! & {\tt Z.compare} & 70 & no\\ -\verb!_ + _! & {\tt Z.add} &&\\ -\verb!_ - _! & {\tt Z.sub} &&\\ -\verb!_ * _! & {\tt Z.mul} &&\\ -\verb!_ / _! & {\tt Z.div} &&\\ -\verb!_ mod _! & {\tt Z.modulo} & 40 & no \\ -\verb!- _! & {\tt Z.opp} &&\\ -\verb!_ ^ _! & {\tt Z.pow} &&\\ -\end{tabular} -\end{center} -\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})} -\label{zarith-syntax} -\end{figure} - -Figure~\ref{zarith-syntax} shows the notations provided by {\tt -Z\_scope}. It specifies how notations are interpreted and, when not -already reserved, the precedence and associativity. - -\begin{coq_example*} -Require Import ZArith. -\end{coq_example*} -\begin{coq_example} -Check (2 + 3)%Z. -Open Scope Z_scope. -Check 2 + 3. -\end{coq_example} - -\subsection[Peano's arithmetic (\texttt{nat})]{Peano's arithmetic (\texttt{nat})\index{Peano's arithmetic} -\ttindex{nat\_scope}} - -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 {\tt Arith}. - -Figure~\ref{nat-syntax} describes notation available in scope {\tt -nat\_scope}. - -\begin{figure} -\begin{center} -\begin{tabular}{l|l} -Notation & Interpretation \\ -\hline -\verb!_ < _! & {\tt lt} \\ -\verb!x <= y! & {\tt le} \\ -\verb!_ > _! & {\tt gt} \\ -\verb!x >= y! & {\tt ge} \\ -\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\ -\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\ -\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\ -\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\ -\verb!_ + _! & {\tt plus} \\ -\verb!_ - _! & {\tt minus} \\ -\verb!_ * _! & {\tt mult} \\ -\end{tabular} -\end{center} -\caption{Definition of the scope for natural numbers ({\tt nat\_scope})} -\label{nat-syntax} -\end{figure} - -\subsection{Real numbers library} - -\subsubsection[Notations for real numbers]{Notations for real numbers\index{Notations for real numbers}} - -This is provided by requiring and opening the module {\tt Reals} and -opening scope {\tt R\_scope}. This set of notations is very similar to -the notation for integer arithmetics. The inverse function was added. -\begin{figure} -\begin{center} -\begin{tabular}{l|l} -Notation & Interpretation \\ -\hline -\verb!_ < _! & {\tt Rlt} \\ -\verb!x <= y! & {\tt Rle} \\ -\verb!_ > _! & {\tt Rgt} \\ -\verb!x >= y! & {\tt Rge} \\ -\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\ -\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\ -\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\ -\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\ -\verb!_ + _! & {\tt Rplus} \\ -\verb!_ - _! & {\tt Rminus} \\ -\verb!_ * _! & {\tt Rmult} \\ -\verb!_ / _! & {\tt Rdiv} \\ -\verb!- _! & {\tt Ropp} \\ -\verb!/ _! & {\tt Rinv} \\ -\verb!_ ^ _! & {\tt pow} \\ -\end{tabular} -\end{center} -\label{reals-syntax} -\caption{Definition of the scope for real arithmetics ({\tt R\_scope})} -\end{figure} - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Require Import Reals. -\end{coq_example*} -\begin{coq_example} -Check (2 + 3)%R. -Open Scope R_scope. -Check 2 + 3. -\end{coq_example} - -\subsubsection{Some tactics} - -In addition to the \verb|ring|, \verb|field| and \verb|fourier| -tactics (see Chapter~\ref{Tactics}) there are: -\begin{itemize} -\item {\tt discrR} \tacindex{discrR} - - Proves that a real integer constant $c_1$ is different from another - real integer constant $c_2$. - -\begin{coq_example*} -Require Import DiscrR. -Goal 5 <> 0. -\end{coq_example*} - -\begin{coq_example} -discrR. -\end{coq_example} - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\item {\tt split\_Rabs} allows unfolding the {\tt Rabs} constant and splits -corresponding conjunctions. -\tacindex{split\_Rabs} - -\begin{coq_example*} -Require Import SplitAbsolu. -Goal forall x:R, x <= Rabs x. -\end{coq_example*} - -\begin{coq_example} -intro; split_Rabs. -\end{coq_example} - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\item {\tt split\_Rmult} splits a condition that a product is - non null into subgoals corresponding to the condition on each - operand of the product. -\tacindex{split\_Rmult} - -\begin{coq_example*} -Require Import SplitRmult. -Goal forall x y z:R, x * y * z <> 0. -\end{coq_example*} - -\begin{coq_example} -intros; split_Rmult. -\end{coq_example} - -\end{itemize} - -These tactics has been written with the tactic language Ltac -described in Chapter~\ref{TacticLanguage}. - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\subsection[List library]{List library\index{Notations for lists} -\ttindex{length} -\ttindex{head} -\ttindex{tail} -\ttindex{app} -\ttindex{rev} -\ttindex{nth} -\ttindex{map} -\ttindex{flat\_map} -\ttindex{fold\_left} -\ttindex{fold\_right}} - -Some elementary operations on polymorphic lists are defined here. They -can be accessed by requiring module {\tt List}. - -It defines the following notions: -\begin{center} -\begin{tabular}{l|l} -\hline -{\tt length} & length \\ -{\tt head} & first element (with default) \\ -{\tt tail} & all but first element \\ -{\tt app} & concatenation \\ -{\tt rev} & reverse \\ -{\tt nth} & accessing $n$-th element (with default) \\ -{\tt map} & applying a function \\ -{\tt flat\_map} & applying a function returning lists \\ -{\tt fold\_left} & iterator (from head to tail) \\ -{\tt fold\_right} & iterator (from tail to head) \\ -\hline -\end{tabular} -\end{center} - -Table show notations available when opening scope {\tt list\_scope}. - -\begin{figure} -\begin{center} -\begin{tabular}{l|l|l|l} -Notation & Interpretation & Precedence & Associativity\\ -\hline -\verb!_ ++ _! & {\tt app} & 60 & right \\ -\verb!_ :: _! & {\tt cons} & 60 & right \\ -\end{tabular} -\end{center} -\label{list-syntax} -\caption{Definition of the scope for lists ({\tt list\_scope})} -\end{figure} - - -\section[Users' contributions]{Users' contributions\index{Contributions} -\label{Contributions}} - -Numerous users' contributions have been collected and are available at -URL \url{http://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. -You will also find informations on how to submit a new -contribution. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index a6a3670bd..5122b2a36 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -95,7 +95,6 @@ Options A and B of the licence are {\em not} elected.} \defaultheaders %END LATEX \include{RefMan-gal.v}% Gallina -\include{RefMan-lib.v}% The coq library \part{The proof engine} diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 84c670175..b3f160df1 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -17,6 +17,7 @@ Table of contents :caption: The language language/gallina-extensions + language/coq-library language/cic language/module-system diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst new file mode 100644 index 000000000..29053d6a5 --- /dev/null +++ b/doc/sphinx/language/coq-library.rst @@ -0,0 +1,988 @@ +.. include:: ../replaces.rst + +.. _thecoqlibrary: + +The |Coq| library +================= + +:Source: https://coq.inria.fr/distrib/current/refman/stdlib.html +:Converted by: Pierre Letouzey + +.. index:: + single: Theories + + +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 :ref:`TODO-6.5.1-Require`); + +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 :ref:`userscontributions`). + +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: + +.. /!\ Please keep the blanks in the lines below, experimentally they produce + a nice last column. Or even better, find a proper way to do this! + +.. productionlist:: + 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 ++++++++++++++++++++++++++ + +.. index:: + single: Connectives + single: True (term) + single: I (term) + single: False (term) + single: not (term) + single: and (term) + single: conj (term) + single: proj1 (term) + single: proj2 (term) + single: or (term) + single: or_introl (term) + single: or_intror (term) + single: iff (term) + single: IF_then_else (term) + +First, we find propositional calculus connectives: + +.. coqtop:: in + + 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). + Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. + +Quantifiers ++++++++++++ + +.. index:: + single: Quantifiers + single: all (term) + single: ex (term) + single: exists (term) + single: ex_intro (term) + single: ex2 (term) + single: exists2 (term) + single: ex_intro2 (term) + +Then we find first-order quantifiers: + +.. coqtop:: in + + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. + Inductive ex (A: Set) (P:A -> Prop) : Prop := + ex_intro (x:A) (_:P x). + Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop := + 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 +++++++++ + +.. index:: + single: Equality + single: eq (term) + single: eq_refl (term) + +Then, we find equality, defined as an inductive relation. That is, +given a type ``A`` and an ``x`` of type ``A``, the +predicate :g:`(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. + +.. coqtop:: in + + Inductive eq (A:Type) (x:A) : A -> Prop := + eq_refl : eq A x x. + +Lemmas +++++++ + +Finally, a few easy lemmas are provided. + +.. index:: + single: absurd (term) + single: eq_sym (term) + single: eq_trans (term) + single: f_equal (term) + single: sym_not_eq (term) + single: eq_ind_r (term) + single: eq_rec_r (term) + single: eq_rect (term) + single: eq_rect_r (term) + +.. coqtop:: in + + 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. + +.. index:: + single: f_equal2 ... f_equal5 (term) + +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. + +.. coqtop:: in + + 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. + +.. _datatypes: + +Datatypes +~~~~~~~~~ + +.. index:: + single: 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 :ref:`specification`): + +.. productionlist:: + 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 ++++++++++++ + +.. index:: + single: Programming + single: unit (term) + single: tt (term) + single: bool (term) + single: true (term) + single: false (term) + single: nat (term) + single: O (term) + single: S (term) + single: option (term) + single: Some (term) + single: None (term) + single: identity (term) + single: refl_identity (term) + +.. coqtop:: in + + Inductive unit : Set := tt. + Inductive bool : Set := true | false. + Inductive nat : Set := O | S (n:nat). + Inductive option (A:Set) : Set := Some (_:A) | None. + Inductive identity (A:Type) (a:A) : A -> Type := + refl_identity : identity A a a. + +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``. + +.. index:: + single: sum (term) + single: A+B (term) + single: + (term) + single: inl (term) + single: inr (term) + single: prod (term) + single: A*B (term) + single: * (term) + single: pair (term) + single: fst (term) + single: snd (term) + +.. coqtop:: in + + Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B). + Inductive prod (A B:Set) : Set := pair (_:A) (_:B). + Section projections. + Variables A B : Set. + Definition fst (H: prod A B) := match H with + | pair _ _ x y => x + end. + Definition snd (H: prod A B) := match H with + | pair _ _ x y => y + end. + End projections. + +Some operations on ``bool`` are also provided: ``andb`` (with +infix notation ``&&``), ``orb`` (with +infix notation ``||``), ``xorb``, ``implb`` and ``negb``. + +.. _specification: + +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 :ref:`datatypes`. + +For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct +:g:`{x:A | P x}` (in abstract syntax :g:`(sig A P)`) is a +``Type``. We may build elements of this set as :g:`(exist x p)` +whenever we have a witness :g:`x:A` with its justification +:g:`p:P x`. + +From such a :g:`(exist x p)` we may in turn extract its witness +:g:`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. + +.. index:: + single: {x:A | P x} (term) + single: sig (term) + single: exist (term) + single: sig2 (term) + single: exist2 (term) + +.. coqtop:: in + + Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + exist2 (x:A) (_:P x) (_:Q x). + +A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, +when the predicate ``P`` is now defined as a +constructor of types in ``Type``. + +.. index:: + single: {x:A & P x} (term) + single: sigT (term) + single: existT (term) + single: sigT2 (term) + single: existT2 (term) + single: projT1 (term) + single: projT2 (term) + +.. coqtop:: in + + Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x). + Section Projections2. + Variable A : Type. + Variable P : A -> Type. + Definition projT1 (H:sigT A P) := let (x, h) := H in x. + Definition projT2 (H:sigT A P) := + match H return P (projT1 H) with + existT _ _ x h => h + end. + End Projections2. + Inductive sigT2 (A: Type) (P Q:A -> Type) : Type := + existT2 (x:A) (_:P x) (_:Q x). + +A related non-dependent construct is the constructive sum +:g:`{A}+{B}` of two propositions ``A`` and ``B``. + +.. index:: + single: sumbool (term) + single: left (term) + single: right (term) + single: {A}+{B} (term) + +.. coqtop:: in + + 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 :g:`A:Set` and :g:`B:Prop` +in the construction :g:`A+{B}` in ``Set``. + +.. index:: + single: sumor (term) + single: inleft (term) + single: inright (term) + single: A+{B} (term) + +.. coqtop:: in + + 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. + +.. index:: + single: Choice (term) + single: Choice2 (term) + single: bool_choice (term) + +.. coqtop:: in + + 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 :g:`A:Type` and +an exceptional value encoding errors: + +.. index:: + single: Exc (term) + single: value (term) + single: error (term) + +.. coqtop:: in + + Definition Exc := option. + Definition value := Some. + Definition error := None. + +This module ends with theorems, relating the sorts ``Set`` or +``Type`` and ``Prop`` in a way which is consistent with the +realizability interpretation. + +.. index:: + single: False_rect (term) + single: False_rec (term) + single: eq_rect (term) + single: absurd_set (term) + single: and_rect (term) + +.. coqtop:: in + + 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 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 :g:`S (S (S O)))`. This also works on +the left hand side of a ``match`` expression (see for example +section :ref:`TODO-refine-example`). 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: + + .. coqtop:: in + + Fixpoint even (n:nat) : bool := + match n with + | 0 => true + | 1 => false + | S (S n) => even n + end. + +.. index:: + single: eq_S (term) + single: pred (term) + single: pred_Sn (term) + single: eq_add_S (term) + single: not_eq_S (term) + single: IsSucc (term) + single: O_S (term) + single: n_Sn (term) + single: plus (term) + single: plus_n_O (term) + single: plus_n_Sm (term) + single: mult (term) + single: mult_n_O (term) + single: mult_n_Sm (term) + +Now comes the content of module ``Peano``: + +.. coqtop:: in + + 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``. + +.. index:: + single: le (term) + single: le_n (term) + single: le_S (term) + single: lt (term) + single: ge (term) + single: gt (term) + +.. coqtop:: in + + 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. + Definition lt (n m:nat) := S n <= m. + Definition ge (n m:nat) := m <= n. + 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. + +.. index:: + single: nat_case (term) + single: nat_double_ind (term) + +.. coqtop:: in + + 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``. + +.. index:: + single: Well foundedness + single: Recursion + single: Well founded induction + single: Acc (term) + single: Acc_inv (term) + single: Acc_rect (term) + single: well_founded (term) + +.. coqtop:: in + + 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. + +.. index:: + single: Fix_F (term) + single: fix_eq (term) + single: Fix_F_inv (term) + single: Fix_F_eq (term) + +.. coqtop:: in + + 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. + +Accessing the Type level +~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic library includes the definitions of the counterparts of some data-types and logical +quantifiers at the ``Type``: level: negation, pair, and properties +of ``identity``. This is the module ``Logic_Type.v``. + +.. index:: + single: notT (term) + single: prodT (term) + single: pairT (term) + +.. coqtop:: in + + Definition notT (A:Type) := A -> False. + Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). + +At the end, it defines data-types at the ``Type`` level. + +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 :ref:`TODO-6.5.1-Require`). + +The different modules of the |Coq| standard library are documented +online at http://coq.inria.fr/stdlib. + +Peano’s arithmetic (nat) +~~~~~~~~~~~~~~~~~~~~~~~~ + +.. index:: + single: Peano's arithmetic + single: nat_scope + +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 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. index:: + single: Arithmetical notations + single: + (term) + single: * (term) + single: - (term) + singel: / (term) + single: <= (term) + single: >= (term) + single: < (term) + single: > (term) + single: ?= (term) + single: mod (term) + + +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:: + .. coqtop:: all reset + + Require Import ZArith. + Check (2 + 3)%Z. + Open Scope Z_scope. + Check 2 + 3. + + +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:: + .. coqtop:: all reset + + Require Import Reals. + Check (2 + 3)%R. + Open Scope R_scope. + Check 2 + 3. + +Some tactics for real numbers ++++++++++++++++++++++++++++++ + +In addition to the powerful ``ring``, ``field`` and ``fourier`` +tactics (see Chapter :ref:`tactics`), there are also: + +.. tacn:: discrR + :name: discrR + + Proves that two real integer constants are different. + +.. example:: + .. coqtop:: all reset + + Require Import DiscrR. + Open Scope R_scope. + Goal 5 <> 0. + discrR. + +.. tacn:: split_Rabs + :name: split_Rabs + + Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. + +.. example:: + .. coqtop:: all reset + + Require Import Reals. + Open Scope R_scope. + Goal forall x:R, x <= Rabs x. + intro; split_Rabs. + +.. tacn:: split_Rmult + :name: split_Rmult + + Splits a condition that a product is non null into subgoals + corresponding to the condition on each operand of the product. + +.. example:: + .. coqtop:: all reset + + Require Import Reals. + Open Scope R_scope. + Goal forall x y z:R, x * y * z <> 0. + intros; split_Rmult. + +These tactics has been written with the tactic language Ltac +described in Chapter :ref:`thetacticlanguage`. + + +List library +~~~~~~~~~~~~ + +.. index:: + single: Notations for lists + single: length (term) + single: head (term) + single: tail (term) + single: app (term) + single: rev (term) + single: nth (term) + single: map (term) + single: flat_map (term) + single: fold_left (term) + single: fold_right (term) + +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 +========== ============== ========== ============= + +.. _userscontributions: + +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. |