diff options
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 1105 |
1 files changed, 0 insertions, 1105 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex deleted file mode 100644 index f4cd9a6f..00000000 --- a/doc/refman/RefMan-lib.tex +++ /dev/null @@ -1,1105 +0,0 @@ -\chapter{The {\Coq} library} -\index{Theories}\label{Theories} - -The \Coq\ library is structured into three parts: - -\begin{description} -\item[The initial library:] it contains - elementary logical notions and datatypes. 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}); - -\item[User contributions:] Other specification and proof developments - coming from the \Coq\ users' community. These libraries are - available for download at \texttt{http://coq.inria.fr} (see - section~\ref{Contributions}). -\end{description} - -This chapter briefly reviews these libraries. - -\section{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}, -and {\tt Wf}. -Module {\tt Logic\_Type} also makes it in the initial state}. - -\subsection{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 precedence and -associativity of very common notations, and avoid users to use them -with other precedence, which may be confusing. - -\begin{figure} -\begin{center} -\begin{tabular}{|cll|} -\hline -Notation & Precedence & Associativity \\ -\hline -\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!_ * _! & 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} -\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} \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 Projections. -\end{coq_example*} -\begin{coq_eval} -Abort All. -\end{coq_eval} -\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} \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} \label{Equality} -\index{Equality} - -Then, we find equality, defined as an inductive relation. That is, -given a \verb: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{refl\_equal} - -\begin{coq_example*} -Inductive eq (A:Type) (x:A) : A -> Prop := - refl_equal : eq A x x. -\end{coq_example*} - -\subsubsection{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{sym\_eq} -\ttindex{trans\_eq} -\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 sym_eq : x = y -> y = x. -Theorem trans_eq : x = y -> y = z -> x = z. -Theorem f_equal : x = y -> f x = f y. -Theorem sym_not_eq : 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 sym_eq sym_not_eq : 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} -\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 sigS})\\ - & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt - \&} {\specif} {\tt \}} & ({\tt sigS2})\\ - & & & \\ -{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair}) -\end{tabular} -\end{centerframe} -\caption{Syntax of datatypes 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} -\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:. - -{\tt identity} is logically equivalent to equality but it lives in -sort {\tt Set}. Computationaly, it behaves like {\tt unit}. - -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*} - -\subsection{Specification} - -The following notions\footnote{They are defined in module {\tt -Specif.v}} allows to build new datatypes and specifications. -They are available with the syntax shown on -Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module -{\tt SpecifSyntax.v}}. - -For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct -\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a -\verb:Set:. 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. - -\index{\{x:A "| (P x)\}} -\index{"|} -\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 \verb:Set: -constructor. - -\ttindex{\{x:A \& (P x)\}} -\ttindex{\&} -\ttindex{sigS} -\ttindex{existS} -\ttindex{projS1} -\ttindex{projS2} -\ttindex{sigS2} -\ttindex{existS2} - -\begin{coq_example*} -Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x). -Section sigSprojections. -Variable A : Set. -Variable P : A -> Set. -Definition projS1 (H:sigS A P) := let (x, h) := H in x. -Definition projS2 (H:sigS A P) := - match H return P (projS1 H) with - existS x h => h - end. -End sigSprojections. -Inductive sigS2 (A: Set) (P Q:A -> Set) : Set := - existS2 (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 constructs builds a sum between a data type \verb|A:Set| 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: and -\verb:Prop: in a way which is consistent with the realizability -interpretation. -\ttindex{False\_rec} -\ttindex{eq\_rec} -\ttindex{Except} -\ttindex{absurd\_set} -\ttindex{and\_rec} - -%Lemma False_rec : (P:Set)False->P. -%Lemma False_rect : (P:Type)False->P. -\begin{coq_example*} -Definition except := False_rec. -Notation Except := (except _). -Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. -Theorem and_rec : - forall (A B:Prop) (P:Set), (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 (plus p m) - end. -Lemma plus_n_O : forall n:nat, n = plus n 0. -Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus 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 + mult p m - end. -Lemma mult_n_O : forall n:nat, 0 = mult n 0. -Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult 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, le n m -> le n (S m). -Infix "+" := plus : 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\_rec} -\ttindex{well\_founded} - -\begin{coq_example*} -Section Well_founded. -Variable A : Set. -Variable R : A -> A -> Prop. -Inductive Acc : A -> Prop := - Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x. -Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. -\end{coq_example*} -\begin{coq_eval} -simple destruct 1; trivial. -Defined. -\end{coq_eval} -\begin{coq_example*} -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. -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} -{\tt 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. -\ttindex{Fix\_F} -\ttindex{fix\_eq} -\ttindex{Fix\_F\_inv} -\ttindex{Fix\_F\_eq} -\begin{coq_example*} -Section FixPoint. -Variable P : A -> Set. -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 datatypes 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 datatypes at the {\Type} level. - -\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 NArith} & Basic positive integer arithmetic \\ - {\bf ZArith} & Basic relative integer arithmetic \\ - {\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 IntMap} & Representation of finite sets by an efficient - structure of map (trees indexed by binary integers).\\ - {\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{\texttt{http://coq.inria.fr}}. - -\subsection{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 Zlt} &&\\ -\verb!x <= y! & {\tt Zle} &&\\ -\verb!_ > _! & {\tt Zgt} &&\\ -\verb!x >= y! & {\tt Zge} &&\\ -\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 Zcompare} & 70 & no\\ -\verb!_ + _! & {\tt Zplus} &&\\ -\verb!_ - _! & {\tt Zminus} &&\\ -\verb!_ * _! & {\tt Zmult} &&\\ -\verb!_ / _! & {\tt Zdiv} &&\\ -\verb!_ mod _! & {\tt Zmod} & 40 & no \\ -\verb!- _! & {\tt Zopp} &&\\ -\verb!_ ^ _! & {\tt Zpower} &&\\ -\end{tabular} -\end{center} -\label{zarith-syntax} -\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})} -\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. -Check (2 + 3)%Z. -Open Scope Z_scope. -Check 2 + 3. -\end{coq_example} - -\subsection{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} -\label{nat-syntax} -\caption{Definition of the scope for natural numbers ({\tt nat\_scope})} -\end{figure} - -\subsection{Real numbers library} - -\subsubsection{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. -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 to unfold {\tt Rabs} constant and splits -corresponding conjonctions. -\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} allows to split 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} - -All this tactics has been written with the tactic language Ltac -described in Chapter~\ref{TacticLanguage}. More details are available -in document \url{http://coq.inria.fr/~desmettr/Reals.ps}. - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\subsection{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} -\index{Contributions} -\label{Contributions} - -Numerous users' contributions have been collected and are available at -URL \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 -\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and -searchable on-line at \url{http://coq.inria.fr/contribs-eng.html} - -% $Id: RefMan-lib.tex 9312 2006-10-28 21:08:35Z herbelin $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |