From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- doc/refman/RefMan-lib.tex | 1102 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1102 insertions(+) create mode 100644 doc/refman/RefMan-lib.tex (limited to 'doc/refman/RefMan-lib.tex') diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex new file mode 100644 index 00000000..f9a5f975 --- /dev/null +++ b/doc/refman/RefMan-lib.tex @@ -0,0 +1,1102 @@ +\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 no + longer distributed with the system. They are available by anonymous + FTP (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{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*} +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. +\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 ZArith} & Basic 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 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,... Requires the + \textbf{ZArith} library).\\ + {\bf Relations} & Relations (definitions and basic results). \\ + {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\ + {\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 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3