From b6018c78b25da14d4f44cf10de692f968cba1e98 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 12 Dec 2000 22:36:15 +0000
Subject: Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Tutorial.tex | 1563 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 1563 insertions(+)
 create mode 100755 doc/Tutorial.tex

(limited to 'doc/Tutorial.tex')

diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
new file mode 100755
index 0000000000..a2459384cf
--- /dev/null
+++ b/doc/Tutorial.tex
@@ -0,0 +1,1563 @@
+\documentclass[11pt]{book}
+\usepackage[T1]{fontenc}
+\usepackage[latin1]{inputenc}
+\usepackage{palatino}
+
+\input{./macros.tex}
+\input{./title.tex}
+
+%\makeindex
+
+\begin{document}
+\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}
+
+%\tableofcontents
+
+\chapter*{Getting started}
+
+\Coq\ is a Proof Assistant for a Logical Framework known as the Calculus
+of Inductive Constructions. It allows the interactive construction of
+formal proofs, and also the manipulation of functional programs 
+consistently with their specifications. It runs as a computer program
+on many architectures, and mainly on Unix machines. It is available
+with a variety of user interfaces. The present document does not attempt
+to present a comprehensive view of all the possibilities of \Coq, but rather
+to present in the most elementary manner a tutorial on the basic
+specification language, called Gallina, in which formal axiomatisations
+may be developed, and on the main proof tools.
+
+We assume here that the potential user has installed \Coq~ on his workstation,
+that he calls \Coq~ from a standard teletype-like shell window, and that
+he does not use any special interface such as Emacs or Centaur. 
+Instructions on installation procedures, as well as more comprehensive
+documentation, may be found in the standard distribution of \Coq,
+which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:,
+directory \verb:INRIA/coq/V6.3.1:. 
+
+In the following, all examples preceded by the prompting sequence
+\verb:Coq < : represent user input, terminated by a period. The
+following lines usually show \Coq's answer as it appears on the users's
+screen. The sequence of such examples is a valid \Coq~ session, unless
+otherwise specified. This version of the tutorial has been prepared 
+on a SPARC station running UNIX.
+The standard invocation of \Coq\ delivers a message such as:
+
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+unix: coqtop
+Welcome to Coq V6.3.1 (December 1999)
+
+Coq <
+\end{verbatim}
+\end{flushleft}
+\end{small}
+
+The first line gives a banner stating the precise version of \Coq~
+used. You should always return this banner when you report an
+anomaly to our hotline \verb:coq@pauillac.inria.fr:. 
+%The next lines are warnings which may be safely ignored for the time being.
+
+\chapter{Basic Predicate Calculus}
+
+\section{An overview of the specification language Gallina}
+
+A formal development in Gallina consists in a sequence of {\sl declarations}
+and {\sl definitions}. You may also send \Coq~ {\sl commands} which are
+not really part of the formal development, but correspond to information
+requests, or service routine invocations. For instance, the command:
+\begin{verbatim}
+Coq < Quit.
+\end{verbatim}
+terminates the current session.
+
+\subsection{Declarations}
+
+A declaration associates a {\sl name} with 
+a {\sl specification}. 
+A name corresponds roughly to an identifier in a programming
+language, i.e. to a string of letters, digits, and a few ASCII symbols like
+underscore (\verb"_") and prime (\verb"'"), starting with a letter. 
+We use case distinction, so that the names \verb"A" and \verb"a" are distinct.
+Certain strings are reserved as key-words of \Coq, and thus are forbidden 
+as user identifiers.
+
+A specification is a formal expression which classifies the notion which is
+being declared. There are basically three kinds of specifications: 
+{\sl logical propositions}, {\sl mathematical collections}, and
+{\sl abstract types}. They are classified by the three basic sorts
+of the system, called respectively \verb:Prop:, \verb:Set:, and
+\verb:Type:, which are themselves atomic abstract types.
+
+Every valid expression $e$ in Gallina is associated with a specification,
+itself a valid expression, called its {\sl type} $\tau(E)$. We write
+$e:\tau(E)$ for the judgement that $e$ is of type $E$. 
+%CP Le role de \tau n'est pas clair.
+You may request \Coq~ to return to you the type of a valid expression by using
+the command \verb:Check::
+
+\begin{coq_example}
+Check O.
+\end{coq_example}
+
+Thus we know that the identifier \verb:O: (the name `O', not to be
+confused with the numeral `0' which is not a proper identifier!) is
+known in the current context, and that its type is the specification 
+\verb:nat:. This specification is itself classified as a mathematical
+collection, as we may readily check:
+
+\begin{coq_example}
+Check nat.
+\end{coq_example}
+
+The specification \verb:Set: is an abstract type, one of the basic
+sorts of the Gallina language, whereas the notions $nat$ and $O$ are
+axiomatised notions which are defined in the arithmetic prelude,
+automatically loaded when running the \Coq\ system.
+
+With what we already know, we may now enter in the system a declaration,
+corresponding to the informal mathematics {\sl let n be a natural number}:
+
+\begin{coq_example}
+Variable n:nat.
+\end{coq_example}
+
+If we want to translate a more precise statement, such as
+{\sl let n be a positive natural number},
+we have to add another declaration, which will declare explicitly the
+hypothesis \verb:Pos_n:, with specification the proper logical
+proposition:
+\begin{coq_example}
+Hypothesis Pos_n : (gt n O).
+\end{coq_example}
+
+Indeed we may check that the relation \verb:gt: is known with the right type
+in the current context:
+
+\begin{coq_example}
+Check gt.
+\end{coq_example}
+
+which tells us that \verb:gt: is a function expecting two arguments of
+type \verb:nat: in order to build a logical proposition.
+What happens here is similar to what we are used to in a functional
+programming language: we may compose the (specification) type \verb:nat:
+with the (abstract) type \verb:Prop: of logical propositions through the
+arrow function constructor, in order to get a functional type
+\verb:nat->Prop::
+\begin{coq_example}
+Check nat->Prop.
+\end{coq_example}
+which may be composed again with \verb:nat: in order to obtain the
+type \verb:nat->nat->Prop: of binary relations over natural numbers.
+Actually \verb:nat->nat->Prop: is an abbreviation for 
+\verb:nat->(nat->Prop):. 
+
+Functional notions may be composed in the usual way. An expression $f$
+of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order
+to form the expression $(f~e)$ of type $B$. Here we get that
+the expression \verb:(gt n): is well-formed of type \verb:nat->Prop:,
+and thus that the expression \verb:(gt n O):, which abbreviates
+\verb:((gt n) O):, is a well-formed proposition.
+\begin{coq_example}
+Check (gt n O).
+\end{coq_example}
+
+\subsection{Definitions}
+
+The initial prelude contains a few arithmetic definitions:
+\verb:nat: is defined as a mathematical collection (type \verb:Set:), constants
+\verb:O:, \verb:S:, \verb:plus:, are defined as objects of types
+respectively \verb:nat:, \verb:nat->nat:, and \verb:nat->nat->nat:.
+You may introduce new definitions, which link a name to a well-typed value.
+For instance, we may introduce the constant \verb:one: as being defined
+to be equal to the successor of zero:
+\begin{coq_example}
+Definition one := (S O).
+\end{coq_example}
+We may optionally indicate the required type:
+\begin{coq_example}
+Definition two : nat := (S one).
+\end{coq_example}
+
+Actually \Coq~ allows several possible syntaxes:
+\begin{coq_example}
+Definition three := (S two) : nat.
+\end{coq_example}
+
+Here is a way to define the doubling function, which expects an
+argument \verb:m: of type \verb:nat: in order to build its result as
+\verb:(plus m m)::
+
+\begin{coq_example}
+Definition double := [m:nat](plus m m).
+\end{coq_example}
+The abstraction brackets are explained as follows. The expression
+\verb+[x:A]e+ is well formed of type \verb+A->B+ in a context
+whenever the expression \verb+e+ is well-formed of type \verb+B+ in 
+the given context to which we add the declaration that \verb+x+
+is of type \verb+A+. Here $x$ is a bound, or dummy variable in
+the expression \verb+[x:A]e+. For instance we could as well have
+defined \verb:double: as \verb+[n:nat](plus n n)+.
+
+Bound (local) variables and free (global) variables may be mixed.
+For instance, we may define the function which adds the constant \verb:n:
+to its argument as
+\begin{coq_example}
+Definition add_n := [m:nat](plus m n).
+\end{coq_example}
+However, note that here we may not rename the formal argument $m$ into $n$
+without capturing the free occurrence of $n$, and thus changing the meaning
+of the defined notion.
+
+Binding operations are well known for instance in logic, where they
+are called quantifiers.
+Thus we may universally quantify a proposition such as $m>0$ in order
+to get a universal proposition $\forall m\cdot m>0$. Indeed this
+operator is available in \Coq, with the following syntax:
+\verb+(m:nat)(gt m O)+. Similarly to the case of the functional abstraction
+binding, we are obliged to declare explicitly the type of the quantified
+variable. We check:
+\begin{coq_example}
+Check (m:nat)(gt m O).
+\end{coq_example}
+
+\section{Introduction to the proof engine: Minimal Logic}
+
+In the following, we are going to consider various propositions, built
+from atomic propositions $A, B, C$. This may be done easily, by
+introducing these atoms as global variables declared of type \verb:Prop:.
+It is easy to declare several names with the same specification:
+\begin{coq_example}
+Variables A,B,C:Prop.
+\end{coq_example}
+
+We shall consider simple implications, such as $A\ra B$, read as 
+``$A$ implies $B$''. Remark that we overload the arrow symbol, which
+has been used above as the functionality type constructor, and which
+may be used as well as propositional connective:
+\begin{coq_example}
+Check A->B.
+\end{coq_example}
+
+Let us now embark on a simple proof. We want to prove the easy tautology
+$((A\ra (B\ra C))\ra (A\ra B)\ra (A\ra C)$. 
+We enter the proof engine by the command
+\verb:Goal:, followed by the conjecture we want to verify:
+\begin{coq_example}
+Goal (A->(B->C))->(A->B)->(A->C).
+\end{coq_example}
+
+The system displays the current goal below a double line, local hypotheses
+(there are none initially) being displayed above the line. We call 
+the combination of local hypotheses with a goal a {\sl judgement}.
+The new prompt \verb:Unnamed_thm <: indicates that we are now in an inner 
+loop of the system, in proof mode. New commands are available in this
+mode, such as {\sl tactics}, which are proof combining primitives.
+A tactic operates on the current goal by attempting to construct a proof
+of the corresponding judgement, possibly from proofs of some
+hypothetical judgements, which are then added to the current
+list of conjectured judgements.
+For instance, the \verb:Intro: tactic is applicable to any judgement
+whose goal is an implication, by moving the proposition to the left
+of the application to the list of local hypotheses:
+\begin{coq_example}
+Intro H.
+\end{coq_example}
+
+%{\bf Warning} to users of \Coq~ previous versions: The display of a sequent in
+%older versions of \Coq~ is inverse of this convention: the goal is displayed
+%above the double line, the hypotheses below.
+
+Several introductions may be done in one step:
+\begin{coq_example}
+Intros H' HA.
+\end{coq_example}
+
+We notice that $C$, the current goal, may be obtained from hypothesis
+\verb:H:, provided the truth of $A$ and $B$ are established.
+The tactic \verb:Apply: implements this piece of reasoning:
+\begin{coq_example}
+Apply H.
+\end{coq_example}
+
+We are now in the situation where we have two judgements as conjectures
+that remain to be proved. Only the first is listed in full, for the
+others the system displays only the corresponding subgoal, without its
+local hypotheses list. Remark that \verb:Apply: has kept the local
+hypotheses of its father judgement, which are still available for
+the judgements it generated.
+
+In order to solve the current goal, we just have to notice that it is
+exactly available as hypothesis $HA$:
+\begin{coq_example}
+Exact HA.
+\end{coq_example}
+
+Now $H'$ applies:
+\begin{coq_example}
+Apply H'.
+\end{coq_example}
+
+And we may now conclude the proof as before, with \verb:Exact HA.:
+Actually, we may not bother with the name \verb:HA:, and just state that
+the current goal is solvable from the current local assumptions:
+\begin{coq_example}
+Assumption.
+\end{coq_example}
+
+The proof is now finished. We may either discard it, by using the
+command \verb:Abort: which returns to the standard \Coq~ toplevel loop
+without further ado, or else save it as a lemma in the current context,
+under name say \verb:trivial_lemma::
+\begin{coq_example}
+Save trivial_lemma.
+\end{coq_example}
+
+As a comment, the system shows the proof script listing all tactic
+commands used in the proof. % ligne blanche apres Exact HA??
+
+Let us redo the same proof with a few variations. First of all we may name
+the initial goal as a conjectured lemma:
+\begin{coq_example}
+Lemma distr_impl : (A->(B->C))->(A->B)->(A->C).
+\end{coq_example}
+
+%{\bf Warning} to users of \Coq~ older versions: In order to enter the proof
+%engine, at this point a dummy \verb:Goal.: command had to be typed in.
+
+Next, we may omit the names of local assumptions created by the introduction
+tactics, they can be automatically created by the proof engine as new
+non-clashing names.
+\begin{coq_example}
+Intros.
+\end{coq_example}
+
+The \verb:Intros: tactic, with no arguments, effects as many individual
+applications of \verb:Intro: as is legal.
+
+Then, we may compose several tactics together in sequence, or in parallel,
+through {\sl tacticals}, that is tactic combinators. The main constructions
+are the following:
+\begin{itemize}
+\item $T_1 ; T_2$ (read $T_1$ then $T_2$) applies tactic $T_1$ to the current
+goal, and then tactic $T_2$ to all the subgoals generated by $T_1$.
+\item $T; [T_1 | T_2 | ... | T_n]$ applies tactic $T$ to the current
+goal, and then tactic $T_1$ to the first newly generated subgoal, 
+..., $T_n$ to the nth.
+\end{itemize}
+
+We may thus complete the proof of \verb:distr_impl: with one composite tactic:
+\begin{coq_example}
+Apply H; [Assumption | Apply H0; Assumption].
+\end{coq_example}
+
+Let us now save lemma \verb:distr_impl::
+\begin{coq_example}
+Save.
+\end{coq_example}
+
+Here \verb:Save: needs no argument, since we gave the name \verb:distr_impl: 
+in advance;
+it is however possible to override the given name by giving a different 
+argument to command \verb:Save:.
+
+Actually, such an easy combination of tactics \verb:Intro:, \verb:Apply:
+and \verb:Assumption: may be found completely automatically by an automatic
+tactic, called \verb:Auto:, without user guidance:
+\begin{coq_example}
+Lemma distr_imp : (A->(B->C))->(A->B)->(A->C).
+Auto.
+\end{coq_example}
+
+This time, we do not save the proof, we just discard it with the \verb:Abort: 
+command:
+
+\begin{coq_example}
+Abort.
+\end{coq_example}
+
+At any point during a proof, we may use \verb:Abort: to exit the proof mode
+and go back to Coq's main loop. We may also use \verb:Restart: to restart
+from scratch the proof of the same lemma. We may also use \verb:Undo: to
+backtrack one step, and more generally \verb:Undo n: to
+backtrack n steps.
+
+We end this section by showing a useful command, \verb:Inspect n.:,
+which inspects the global \Coq~ environment, showing the last \verb:n: declared
+notions: % Attention ici ??
+\begin{coq_example}
+Inspect 3.
+\end{coq_example}
+
+The declarations, whether global parameters or axioms, are shown preceded by 
+\verb:***:; definitions and lemmas are stated with their specification, but
+their value (or proof-term) is omitted.
+
+\section{Propositional Calculus}
+
+\subsection{Conjunction}
+
+We have seen that how \verb:Intro: and \verb:Apply: tactics could be combined
+in order to prove implicational statements. More generally, \Coq~ favors a style
+of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into 
+so called {\sl introduction rules}, which tell how to prove a goal whose main 
+operator is a given propositional connective, and {\sl elimination rules},
+which tell how to use an hypothesis whose main operator is the propositional 
+connective. Let us show how to use these ideas for the propositional connectives
+\verb:/\: and \verb:\/:.
+
+\begin{coq_example}
+Lemma and_commutative : A /\ B -> B /\ A.
+Intro.
+\end{coq_example}
+
+We make use of the conjunctive hypothesis \verb:H: with the \verb:Elim: tactic,
+which breaks it into its components:
+\begin{coq_example}
+Elim H.
+\end{coq_example}
+
+We now use the conjuction introduction tactic \verb:Split:, which splits the 
+conjunctive goal into the two subgoals:
+\begin{coq_example}
+Split.
+\end{coq_example}
+
+and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
+\begin{coq_example}
+Restart.
+Intro H; Elim H; Auto.
+Save.
+\end{coq_example}
+
+The tactic \verb:Auto: succeeded here because it knows as a hint the 
+conjunction introduction operator \verb+conj+
+\begin{coq_example}
+Check conj.
+\end{coq_example}
+
+Actually, the tactic \verb+Split+ is just an abbreviation for \verb+Apply conj.+
+
+What we have just seen is that the \verb:Auto: tactic is more powerful than
+just a simple application of local hypotheses; it tries to apply as well 
+lemmas which have been specified as hints. A 
+\verb:Hints Resolve: command registers a
+lemma as a hint to be used from now on by the \verb:Auto: tactic, whose power 
+may thus be incrementally augmented.
+
+\subsection{Disjunction}
+
+In a similar fashion, let us consider disjunction:
+
+\begin{coq_example}
+Lemma or_commutative : A \/ B -> B \/ A.
+Intro H; Elim H.
+\end{coq_example}
+
+Let us prove the first subgoal in detail. We use \verb:Intro: in order to
+be left to prove \verb:B\/A: from \verb:A::
+
+\begin{coq_example}
+Intro HA.
+\end{coq_example}
+
+Here the hypothesis \verb:H: is not needed anymore. We could choose to
+actually erase it with the tactic \verb:Clear:; in this simple proof it
+does not really matter, but in bigger proof developments it is useful to
+clear away unnecessary hypotheses which may clutter your screen.
+\begin{coq_example}
+Clear H.
+\end{coq_example}
+
+The disjunction connective has two introduction rules, since \verb:P\/Q:
+may be obtained from \verb:P: or from \verb:Q:; the two corresponding
+proof constructors are called respectively \verb:or_introl: and
+\verb:or_intror:; they are applied to the current goal by tactics
+\verb:Left: and \verb:Right: respectively. For instance:
+\begin{coq_example}
+Right.
+Trivial.
+\end{coq_example}
+%CP Documenter Trivial ou mettre Assumption.
+
+As before, all these tedious elementary steps may be performed automatically,
+as shown for the second symmetric case:
+
+\begin{coq_example}
+Auto.
+\end{coq_example}
+
+However, \verb:Auto: alone does not succeed in proving the full lemma, because
+it does not try any elimination step.
+It is a bit disappointing that \verb:Auto: is not able to prove automatically 
+such a simple tautology. The reason is that we want to keep
+\verb:Auto: efficient, so that it is always effective to use. 
+
+\subsection{Tauto}
+
+A complete tactic for propositional
+tautologies is indeed available in \Coq~ as the \verb:Tauto: tactic. 
+%In order to get this facility, we have to import a library module 
+%called ``Dyckhoff'':
+\begin{coq_example}
+Restart.
+Tauto.
+Save.
+\end{coq_example}
+
+It is possible to inspect the actual proof tree constructed by \verb:Tauto:,
+using a standard command of the system, which prints the value of any notion 
+currently defined in the context:
+\begin{coq_example}
+Print or_commutative.
+\end{coq_example}
+
+It is not easy to understand the notation for proof terms without a few
+explanations. The square brackets, such as \verb+[HH1:A\/B]+, correspond
+to \verb:Intro HH1:, whereas a subterm such as 
+\verb:(or_intror: \linebreak \verb:B A HH6):
+corresponds to the sequence \verb:Apply or_intror; Exact HH6:. The extra
+arguments \verb:B: and \verb:A: correspond to instanciations to the generic
+combinator \verb:or_intror:, which are effected automatically by the tactic
+\verb:Apply: when pattern-matching a goal. The specialist will of course
+recognize our proof term as a $\lambda$-term, used as notation for the
+natural deduction proof term through the Curry-Howard isomorphism. The
+naive user of \Coq~ may safely ignore these formal details.
+
+Let us exercise the \verb:Tauto: tactic on a more complex example:
+\begin{coq_example}
+Lemma distr_and : A->(B/\C) -> (A->B /\ A->C).
+Tauto.
+Save.
+\end{coq_example}
+
+\subsection{Classical reasoning}
+
+\verb:Tauto: always comes back with an answer. Here is an example where it 
+fails:
+\begin{coq_example}
+Lemma Peirce : ((A->B)->A)->A.
+Try Tauto.
+\end{coq_example}
+
+Note the use of the \verb:Try: tactical, which does nothing if its tactic
+argument fails.
+
+This may come as a surprise to someone familiar with classical reasoning. 
+Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for 
+every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
+of Peirce's law may be proved in \Coq~ using \verb:Tauto::
+\begin{coq_example}
+Abort.
+Lemma NNPeirce : ~~(((A->B)->A)->A).
+Tauto.
+Save.
+\end{coq_example}
+
+In classical logic, the double negation of a proposition is equivalent to this 
+proposition, but in the constructive logic of \Coq~ this is not so. If you 
+want to use classical logic in \Coq, you have to import explicitly the
+\verb:Classical: module, which will declare the axiom \verb:classic:
+of excluded middle, and classical tautologies such as de Morgan's laws.
+The \verb:Require: command is used to import a module from \Coq's library:
+\begin{coq_example}
+Require Classical.
+Check NNPP.
+\end{coq_example}
+
+and it is now easy (although admittedly not the most direct way) to prove
+a classical law such as Peirce's:
+\begin{coq_example}
+Lemma Peirce : ((A->B)->A)->A.
+Apply NNPP; Tauto.
+Save.
+\end{coq_example}
+
+Here is one more example of propositional reasoning, in the shape of
+a scottish puzzle. A private club has the following rules:
+\begin{enumerate}
+\item Every non-scottish member wears red socks
+\item Every member wears a kilt or doesn't wear red socks
+\item The married members don't go out on sunday
+\item A member goes out on sunday if and only if he is scottish
+\item Every member who wears a kilt is scottish and married
+\item Every scottish member wears a kilt
+\end{enumerate}
+Now, we show that these rules are so strict that no one can be accepted.
+\begin{coq_example}
+Section club.
+Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop.
+Hypothesis rule1 : ~Scottish -> RedSocks.
+Hypothesis rule2 : WearKilt \/ ~RedSocks.
+Hypothesis rule3 : Married -> ~GoOutSunday.
+Hypothesis rule4 : GoOutSunday <-> Scottish.
+Hypothesis rule5 : WearKilt -> (Scottish /\ Married).
+Hypothesis rule6 : Scottish -> WearKilt.
+Lemma NoMember : False.
+Tauto.
+Save.
+End club.
+\end{coq_example}
+
+\section{Predicate Calculus}
+
+Let us now move into predicate logic, and first of all into first-order
+predicate calculus. The essence of predicate calculus is that to try to prove 
+theorems in the most abstract possible way, without using the definitions of 
+the mathematical notions, but by formal manipulations of uninterpreted 
+function and predicate symbols. 
+
+\subsection{Sections and signatures}
+
+Usually one works in some domain of discourse, over which range the individual 
+variables and function symbols. In \Coq~ we speak in a language with a rich 
+variety of types, so me may mix several domains of discourse, in our 
+multi-sorted language. For the moment, we just do a few exercises, over a 
+domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two 
+predicate symbols  \verb:P: and \verb:R: over \verb:D:, of arities 
+respectively 1 and 2. Such abstract entities may be entered in the context
+as global variables. But we must be careful about the pollution of our
+global environment by such declarations. For instance, we have already 
+polluted our \Coq~ session by declaring the variables
+\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. If we want to revert to the clean state of
+our initial session, we may use the \Coq~ \verb:Reset: command, which returns
+to the state just prior the given global notion.
+\begin{coq_example}
+Reset n.
+\end{coq_example}
+%CP-Parler de Reset Initial.
+
+We shall now declare a new \verb:Section:, which will allow us to define
+notions local to a well-delimited scope. We start by assuming a domain of
+discourse \verb:D:, and a binary relation \verb:R:  over \verb:D:: 
+\begin{coq_example}
+Section Predicate_calculus.
+Variable D:Set.
+Variable R: D -> D -> Prop.
+\end{coq_example}
+
+As a simple example of predicate calculus reasoning, let us assume
+that relation \verb:R: is symmetric and transitive, and let us show that
+\verb:R: is reflexive in any point \verb:x: which has an \verb:R: successor.
+Since we do not want to make the assumptions about \verb:R: global axioms of 
+a theory, but rather local hypotheses to a theorem, we open a specific
+section to this effect.
+\begin{coq_example}
+Section R_sym_trans.
+Hypothesis R_symmetric : (x,y:D) (R x y) -> (R y x).
+Hypothesis R_transitive : (x,y,z:D) (R x y) -> (R y z) -> (R x z).
+\end{coq_example}
+
+Remark the syntax \verb+(x:D)+ which stands for universal quantification
+$\forall x : D$.
+
+\subsection{Existential quantification}
+
+We now state our lemma, and enter proof mode.
+\begin{coq_example}
+Lemma refl_if : (x:D)(EX y | (R x y)) -> (R x x).
+\end{coq_example}
+
+Remark that the hypotheses which are local to the currently opened sections
+are listed as local hypotheses to the current goals.
+The rationale is that these hypotheses are going to be discharged, as we
+shall see, when we shall close the corresponding sections.
+
+Note the functional syntax for existential quantification. The existential
+quantifier is built from the operator \verb:ex:, which expects a 
+predicate as argument:
+\begin{coq_example}
+Check ex.
+\end{coq_example}
+and the notation \verb+(EX x | (P x))+ is just concrete syntax for 
+\verb+(ex D [x:D](P x))+. 
+Existential quantification is handled in \Coq~ in a similar
+fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
+the proof combinator \verb:ex_intro:, which is invoked by the specific 
+tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to
+\verb:P:, together with an assumption \verb+h:(P a)+ that indeed \verb+a+
+verifies \verb:P:. Let us see how this works on this simple example.
+\begin{coq_example}
+Intros x x_Rlinked.
+\end{coq_example}
+
+Remark that \verb:Intro: treats universal quantification in the same way
+as the premisses of implications. Renaming of bound variables occurs
+when it is needed; for instance, had we started with \verb:Intro y:,
+we would have obtained the goal:
+\begin{coq_eval}
+Undo.
+\end{coq_eval}
+\begin{coq_example}
+Intro y.
+\end{coq_example}
+\begin{coq_eval}
+Undo.
+Intros x x_Rlinked.
+\end{coq_eval}
+
+Let us now use the existential hypothesis \verb:x_Rlinked: to 
+exhibit an R-successor y of x. This is done in two steps, first with
+\verb:Elim:, then with \verb:Intros:
+
+\begin{coq_example}
+Elim x_Rlinked.
+Intros y Rxy.
+\end{coq_example}
+
+Now we want to use \verb:R_transitive:. The \verb:Apply: tactic will know
+how to match \verb:x: with \verb:x:, and \verb:z: with \verb:x:, but needs
+help on how to instanciate \verb:y:, which appear in the hypotheses of
+\verb:R_transitive:, but not in its conclusion. We give the proper hint
+to \verb:Apply: in a \verb:with: clause, as follows:
+\begin{coq_example}
+Apply R_transitive with y.
+\end{coq_example}
+
+The rest of the proof is routine:
+\begin{coq_example}
+Assumption.
+Apply R_symmetric; Assumption.
+\end{coq_example}
+\begin{coq_example*}
+Save.
+\end{coq_example*}
+
+Let us now close the current section.
+\begin{coq_example}
+End R_sym_trans. 
+\end{coq_example}
+
+Here \Coq's printout is a warning that all local hypotheses have been 
+discharged in the statement of \verb:refl_if:, which now becomes a general
+theorem in the first-order language declared in section 
+\verb:Predicate_calculus:. In this particular example, the use of section
+\verb:R_sym_trans: has not been really significant, since we could have
+instead stated theorem \verb:refl_if: in its general form, and done 
+basically the same proof, obtaining \verb:R_symmetric: and
+\verb:R_transitive: as local hypotheses by initial \verb:Intros: rather
+than as global hypotheses in the context. But if we had pursued the
+theory by proving more theorems about relation \verb:R:,
+we would have obtained all general statements at the closing of the section,
+with minimal dependencies on the hypotheses of symmetry and transitivity.
+
+\subsection{Paradoxes of classical predicate calculus}
+
+Let us illustrate this feature by pursuing our \verb:Predicate_calculus:
+section with an enrichment of our language: we declare a unary predicate
+\verb:P: and a constant \verb:d::
+\begin{coq_example}
+Variable P:D->Prop.
+Variable d:D.
+\end{coq_example}
+
+We shall now prove a well-known fact from first-order logic: a universal 
+predicate is non-empty, or in other terms existential quantification 
+follows from universal quantification.
+\begin{coq_example}
+Lemma weird : ((x:D)(P x)) -> (EX a | (P a)). 
+Intro UnivP.
+\end{coq_example}
+
+First of all, notice the pair of parentheses around \verb+(x:D)(P x)+ in
+the statement of lemma \verb:weird:.
+If we had ommitted them, \Coq's parser would have interpreted the
+statement as a truly trivial fact, since we would 
+postulate an \verb:x: verifying \verb:(P x):. Here the situation is indeed
+more problematic. If we have some element in \verb:Set: \verb:D:, we may
+apply \verb:UnivP: to it and conclude, otherwise we are stuck. Indeed
+such an element \verb:d: exists, but this is just by virtue of our
+new signature. This points out a subtle difference between standard
+predicate calculus and \Coq. In standard first-order logic,
+the equivalent of lemma \verb:weird: always holds, 
+because such a rule is wired in the inference rules for quantifiers, the
+semantic justification being that the interpretation domain is assumed to
+be non-empty. Whereas in \Coq, where types are not assumed to be 
+systematically inhabited, lemma \verb:weird: only holds in signatures
+which allow the explicit construction of an element in the domain of
+the predicate. 
+
+Let us conclude the proof, in order to show the use of the \verb:Exists:
+tactic:
+\begin{coq_example}
+Exists d; Trivial.
+Save.
+\end{coq_example}
+
+Another fact which illustrates the sometimes disconcerting rules of
+classical 
+predicate calculus is Smullyan's drinkers' paradox: ``In any non-empty
+bar, there is a person such that if she drinks, then everyone drinks''.
+We modelize the bar by Set \verb:D:, drinking by predicate \verb:P:.
+We shall need classical reasoning. Instead of loading the \verb:Classical:
+module as we did above, we just state the law of excluded middle as a
+local hypothesis schema at this point:
+\begin{coq_example}
+Hypothesis EM : (A:Prop) A \/ ~A.
+Lemma drinker : (EX x | (P x) -> (x:D)(P x)).
+\end{coq_example}
+The proof goes by cases on whether or not
+there is someone who does not drink. Such reasoning by cases proceeds
+by invoking the excluded middle principle, via \verb:Elim: of the
+proper instance of \verb:EM::
+\begin{coq_example}
+Elim (EM  (EX x | ~(P x))).
+\end{coq_example}
+
+We first look at the first case. Let Tom be the non-drinker:
+\begin{coq_example}
+Intro Non_drinker; Elim Non_drinker; Intros Tom Tom_does_not_drink.
+\end{coq_example}
+
+We conclude in that case by considering Tom, since his drinking leads to
+a contradiction:
+\begin{coq_example}
+Exists Tom; Intro Tom_drinks.
+\end{coq_example}
+
+There are several ways in which we may eliminate a contradictory case;
+a simple one is to use the \verb:Absurd: tactic as follows:
+\begin{coq_example}
+Absurd (P Tom); Trivial.
+\end{coq_example}
+
+We now proceed with the second case, in which actually any person will do;
+such a John Doe is given by the non-emptyness witness \verb:d::
+\begin{coq_example}
+Intro No_nondrinker; Exists d; Intro d_drinks.
+\end{coq_example}
+
+Now we consider any Dick in the bar, and reason by cases according to its
+drinking or not:
+\begin{coq_example}
+Intro Dick; Elim (EM (P Dick)); Trivial.
+\end{coq_example}
+
+The only non-trivial case is again treated by contradiction:
+\begin{coq_example}
+Intro Dick_does_not_drink; Absurd (EX x | ~(P x)); Trivial.
+Exists Dick; Trivial.
+Save.
+\end{coq_example}
+
+Now, let us close the main section:
+\begin{coq_example}
+End Predicate_calculus.
+\end{coq_example}
+
+Remark how the three theorems are completely generic is the most general 
+fashion;
+the domain \verb:D: is discharged in all of them, \verb:R: is discharged in
+\verb:refl_if: only, \verb:P: is discharged only in \verb:weird: and
+\verb:drinker:, along with the hypothesis that \verb:D: is inhabited. 
+Finally, the excluded middle hypothesis is discharged only in 
+\verb:drinker:.
+
+Note that the name \verb:d: has vanished as well from
+the statements of \verb:weird: and \verb:drinker:, 
+since \Coq's prettyprinter replaces
+systematically a quantification such as \verb+(d:D)E+, where \verb:d:
+does not occur in \verb:E:, by the functional notation \verb:D->E:. 
+Similarly the name \verb:EM: does not appear in \verb:drinker:. 
+
+Actually, universal quantification, implication, 
+as well as function formation, are
+all special cases of one general construct of type theory called
+{\sl dependent product}. This is the mathematical construction 
+corresponding to an indexed family of functions. A function 
+$f\in \Pi x:D\cdot Cx$ maps an element $x$ of its domain $D$ to its
+(indexed) codomain $Cx$. Thus a proof of $\forall x:D\cdot Px$ is
+a function mapping an element $x$ of $D$ to a proof of proposition $Px$.
+
+
+\subsection{Flexible use of local assumptions}
+
+Very often during the course of a proof we want to retrieve a local
+assumption and reintroduce it explicitly in the goal, for instance
+in order to get a more general induction hypothesis. The tactic
+\verb:Generalize: is what is needed here:
+
+\begin{coq_example}
+Variable P,Q:nat->Prop. Variable R: nat->nat->Prop.
+Lemma PQR : (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x).
+Intros.
+Generalize H0.
+\end{coq_example}
+
+Sometimes it may be convenient to use a lemma, although we do not have
+a direct way to appeal to such an already proven fact. The tactic \verb:Cut:
+permits to use the lemma at this point, keeping the corresponding proof
+obligation as a new subgoal:
+\begin{coq_example}
+Cut (R x x); Trivial.
+\end{coq_example}
+%CP pourquoi ne pas montrer les deux sous-buts engendres par Cut.
+
+\subsection{Equality}
+
+The basic equality provided in \Coq~ is Leibniz equality, noted infix like
+\verb+x=y+, when \verb:x: and \verb:y: are two expressions of
+type the same Set. The replacement of \verb:x: by \verb:y: in any
+term is effected by a variety of tactics, such as \verb:Rewrite:
+and \verb:Replace:. 
+
+Let us give a few examples of equality replacement. Let us assume that
+some arithmetic function \verb:f: is null in zero:
+\begin{coq_example}
+Variable f:nat->nat.
+Hypothesis foo : (f O)=O.
+\end{coq_example}
+
+We want to prove the following conditional equality:
+\begin{coq_example*}
+Lemma L1 : (k:nat)k=O->(f k)=k.
+\end{coq_example*}
+
+As usual, we first get rid of local assumptions with \verb:Intro::
+\begin{coq_example}
+Intros k E.
+\end{coq_example}
+
+Let us now use equation \verb:E: as a left-to-right rewriting:
+\begin{coq_example}
+Rewrite E.
+\end{coq_example}
+This replaced both occurrences of \verb:k: by \verb:O:. 
+
+\medskip
+{\bf Warning} to users of \Coq~ old versions: In \Coq V5.8 only the second
+occurrence of \verb:k: would have been replaced, and we would have had
+to use \verb:Rewrite: twice in order to get the same effect.
+\medskip
+
+%Actually, it is possible to rewrite both occurrences of \verb:k: at the
+%same time, provided one abstracts \verb:k: in the goal with tactic
+%\verb:Pattern:. Let us go back two steps:
+%\begin{coq_example}
+%L1 < Undo 2.
+%1 subgoal
+%
+%  k : nat
+%  E : k=O
+%  ============================
+%   (f k)=k
+%
+%L1 < Pattern k.
+%1 subgoal
+%
+%  k : nat
+%  E : k=O
+%  ============================
+%   ([n:nat](f n)=n k)
+%\end{coq_example}
+%What just happened is that \verb:Pattern: replaced the goal 
+%\verb:(f k)=k: by the equivalent one:
+%\verb+([n:nat](f n)=n k)+, which has the form \verb+(P k)+, with
+%\verb+P+ the predicate which maps \verb+n+ to proposition
+%\verb+(f n)=n+. The two goals are equivalent in the sense that
+%\verb+([n:nat](f n)=n k)+ {\sl reduces} to \verb:(f k)=k:
+%by the following computation rule:
+%$$ ([x:A]M~N) \leftarrow M\{x/N\} \eqno \beta$$
+%We may now proceed with our rewriting:
+%\begin{coq_example}
+%L1 < Rewrite E.
+%1 subgoal
+%
+%  k : nat
+%  E : k=O
+%  ============================
+%   (f O)=O
+
+Now \verb:Apply foo: will finish the proof:
+
+\begin{coq_example}
+Apply foo.
+Save.
+\end{coq_example}
+
+When one wants to rewrite an equality in a right to left fashion, we should
+use \verb:Rewrite <- E: rather than \verb:Rewrite E: or the equivalent
+\verb:Rewrite -> E:. 
+Let us now illustrate the tactic \verb:Replace:.
+\begin{coq_example}
+Lemma L2 : (f (f O))=O.
+Replace (f O) with O.
+\end{coq_example}
+What happened here is that the replacement left the first subgoal to be
+proved, but another proof obligation was generated by the \verb:Replace:
+tactic, as the second subgoal. The first subgoal is solved immediately
+by appying lemma \verb:foo:; the second one too, provided we apply first
+symmetry of equality, for instance with tactic \verb:Symmetry::
+\begin{coq_example}
+Apply foo.
+Symmetry; Apply foo.
+Save.
+\end{coq_example}
+
+\subsection{Predicate calculus over Type}
+
+We just explained the basis of first-order reasoning in the universe
+of mathematical Sets. Similar reasoning is available at the level of
+abstract Types. In order to develop such abtract reasoning, one must
+load the library \verb:Logic_Type:.
+
+\begin{coq_example}
+Require Logic_Type.
+\end{coq_example}
+
+New proof combinators are now available, such as the existential
+quantification \verb:exT: over a Type, available with syntax
+\verb:(EXT x | (P x)):. The corresponding introduction
+combinator may be invoked by the tactic \verb:Exists: as above.
+\begin{coq_example}
+Check exT_intro.
+\end{coq_example}
+
+Similarly, equality over Type is available, with notation 
+\verb:M==N:. The equality tactics process \verb:==: in the same way
+as \verb:=:.
+
+\section{Using definitions}
+
+The development of mathematics does not simply proceed by logical 
+argumentation from first principles: definitions are used in an essential way.
+A formal development proceeds by a dual process of abstraction, where one
+proves abstract statements in predicate calculus, and use of definitions, 
+which in the contrary one instanciates general statements with particular 
+notions in order to use the structure of mathematical values for the proof of
+more specialised properties.
+
+\subsection{Unfolding definitions}
+
+Assume that we want to develop the theory of sets represented as characteristic
+predicates over some universe \verb:U:. For instance:
+%CP Une petite explication pour le codage de element ?
+\begin{coq_example}
+Variable U:Type.
+Definition set := U->Prop.
+Definition element := [x:U][S:set](S x).
+Definition subset := [A,B:set](x:U)(element x A)->(element x B).
+\end{coq_example}
+
+Now, assume that we have loaded a module of general properties about
+relations over some abstract type \verb:T:, such as transitivity:
+
+\begin{coq_example}
+Definition transitive := [T:Type][R:T->T->Prop]
+                 (x,y,z:T)(R x y)->(R y z)->(R x z).
+\end{coq_example}
+
+Now, assume that we want to prove that \verb:subset: is a \verb:transitive:
+relation. 
+\begin{coq_example}
+Lemma subset_transitive : (transitive set subset).
+\end{coq_example}
+
+In order to make any progress, one needs to use the definition of 
+\verb:transitive:. The \verb:Unfold: tactic, which replaces all occurrences of a
+defined notion by its definition in the current goal, may be used here.
+\begin{coq_example}
+Unfold transitive.
+\end{coq_example}
+
+Now, we must unfold \verb:subset::
+\begin{coq_example}
+Unfold subset.
+\end{coq_example}
+Now, unfolding \verb:element: would be a mistake, because indeed a simple proof
+can be found by \verb:Auto:, keeping \verb:element: an abstract predicate:
+\begin{coq_example}
+Auto.
+\end{coq_example}
+
+Many variations on \verb:Unfold: are provided in \Coq. For instance,
+we may selectively unfold one designated occurrence:
+\begin{coq_example}
+Undo 2.
+Unfold 2 subset.
+\end{coq_example}
+
+One may also unfold a definition in a given local hypothesis, using the
+\verb:in: notation:
+\begin{coq_example}
+Intros.
+Unfold subset in H.
+\end{coq_example}
+
+Finally, the tactic \verb:Red: does only unfolding of the head occurrence
+of the current goal:
+\begin{coq_example}
+Red.
+Auto. Save.
+\end{coq_example}
+
+
+\subsection{Principle of proof irrelevance}
+
+Even though in principle the proof term associated with a verified lemma
+corresponds to a defined value of the corresponding specification, such
+definitions cannot be unfolded in \Coq: a lemma is considered an {\sl opaque}
+definition. This conforms to the mathematical tradition of {\sl proof
+irrelevance}: the proof of a logical proposition does not matter, and the
+mathematical justification of a logical development relies only on
+{\sl provability} of the lemmas used in the formal proof. 
+
+Conversely, ordinary mathematical definitions can be unfolded at will, they
+are {\sl transparent}. It is possible to enforce the reverse convention by
+declaring a definition as {\sl opaque} or a lemma as {\sl transparent}.
+
+\chapter{Induction}
+
+\section{Data Types as Inductively Defined Mathematical Collections}
+
+All the notions which were studied until now pertain to traditional
+mathematical logic. Specifications of objects were abstract properties
+used in reasoning more or less constructively; we are now entering
+the realm of inductive types, which specify the existence of concrete
+mathematical constructions.
+
+\subsection{Booleans}
+
+Let us start with the collection of booleans, as they are specified
+in the \Coq's \verb:Prelude: module: 
+\begin{coq_example}
+Inductive bool : Set := true : bool | false : bool.
+\end{coq_example}
+
+Such a declaration defines several objects at once. First, a new
+\verb:Set: is declared, with name \verb:bool:. Then the {\sl constructors}
+of this \verb:Set: are declared, called \verb:true: and \verb:false:.
+Those are analogous to introduction rules of the new Set \verb:bool:.
+Finally, a specific elimination rule for \verb:bool: is now available, which
+permits to reason by cases on \verb:bool: values. Three instances are
+indeed defined as new combinators in the global context: \verb:bool_ind:,
+a proof combinator corresponding to reasoning by cases,
+\verb:bool_rec:, an if-then-else programming construct,
+and \verb:bool_rect:, a similar combinator at the level of types.
+Indeed:
+\begin{coq_example}
+Check bool_ind.
+Check bool_rec.
+Check bool_rect.
+\end{coq_example}
+
+Let us for instance prove that every Boolean is true or false.
+\begin{coq_example}
+Lemma duality : (b:bool)(b=true \/ b=false).
+Intro b.
+\end{coq_example}
+
+We use the knowledge that \verb:b: is a \verb:bool: by calling tactic
+\verb:Elim:, which is this case will appeal to combinator \verb:bool_ind:
+in order to split the proof according to the two cases:
+\begin{coq_example}
+Elim b.
+\end{coq_example}
+
+It is easy to conclude in each case:
+\begin{coq_example}
+Left; Trivial.
+Right; Trivial.
+\end{coq_example}
+
+Indeed, the whole proof can be done with the combination of the
+\verb:Induction: tactic, which combines \verb:Intro: and \verb:Elim:,
+with good old \verb:Auto::
+\begin{coq_example}
+Restart.
+Induction b; Auto.
+Save.
+\end{coq_example}
+
+\subsection{Natural numbers}
+
+Similarly to Booleans, natural numbers are defined in the \verb:Prelude:
+module with constructors \verb:S: and \verb:O::
+\begin{coq_example}
+Inductive nat : Set := O : nat | S : nat->nat.
+\end{coq_example}
+
+The elimination principles which are automatically generated are Peano's
+induction principle, and a recursion operator:
+\begin{coq_example}
+Check nat_ind.
+Check nat_rec.
+\end{coq_example}
+
+Let us start by showing how to program the standard primitive recursion
+operator \verb:prim_rec: from the more general \verb:nat_rec::
+\begin{coq_example}
+Definition prim_rec := (nat_rec [i:nat]nat).
+\end{coq_example}
+
+That is, instead of computing for natural \verb:i: an element of the indexed
+\verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of 
+\verb:nat:. Let us check the type of \verb:prim_rec::
+\begin{coq_example}
+Check prim_rec.
+\end{coq_example}
+
+Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
+get an apparently more complicated expression. Indeed the type of
+\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may
+be checked in \Coq~ by command \verb:Eval Cbv Beta:, which $\beta$-reduces
+an expression to its {\sl normal form}:
+\begin{coq_example}
+Eval Cbv Beta in
+     ([_:nat]nat O)
+        ->((y:nat)([_:nat]nat y)->([_:nat]nat (S y)))
+           ->(n:nat)([_:nat]nat n).
+\end{coq_example}
+
+Let us now show how to program addition with primitive recursion:
+\begin{coq_example}
+Definition addition := [n,m:nat](prim_rec m [p:nat][rec:nat](S rec) n).
+\end{coq_example}
+
+That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
+according to its main constructor; when \verb:n=O:, we get \verb:m:;
+ when \verb:n=(S p):, we get \verb:(S rec):, where \verb:rec: is the result
+of the recursive computation \verb+(addition p m)+. Let us verify it by
+asking \Coq~to compute for us say $2+3$:
+\begin{coq_example}
+Eval Compute in (addition (S (S O)) (S (S (S O)))).
+\end{coq_example}
+
+Actually, we do not have to do all explicitly. {\Coq} provides a
+special syntax {\tt Fixpoint/Cases} for generic primitive recursion,
+and we could thus have defined directly addition as:
+
+\begin{coq_example}
+Fixpoint plus [n:nat] : nat -> nat := 
+   [m:nat]Cases n of 
+             O    => m 
+          | (S p) => (S (plus p m))
+          end.
+\end{coq_example}
+
+For the rest of the session, we shall clean up what we did so far with 
+types \verb:bool: and \verb:nat:, in order to use the initial definitions
+given in \Coq's \verb:Prelude: module, and not to get confusing error
+messages due to our redefinitions. We thus revert to the state before
+our definition of \verb:bool: with the \verb:Reset: command:
+\begin{coq_example}
+Reset bool.
+\end{coq_example}
+
+
+\subsection{Simple proofs by induction}
+%CP  Pourquoi ne pas commencer par des preuves d'egalite entre termes
+%    convertibles. 
+
+Let us now show how to do proofs by structural induction. We start with easy
+properties of the \verb:plus: function we just defined. Let us first
+show that $n=n+0$.
+\begin{coq_example}
+Lemma plus_n_O : (n:nat)n=(plus n O).
+Intro n; Elim n.
+\end{coq_example}
+
+What happened was that \verb:Elim n:, in order to construct a \verb:Prop:
+(the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
+corresponding induction principle \verb:nat_ind: which we saw was indeed
+excactly Peano's induction scheme. Pattern-matching instanciated the 
+corresponding predicate \verb:P: to \verb+[n:nat]n=(plus n O)+, and we get
+as subgoals the corresponding instanciations of the base case \verb:(P O): ,
+and of the inductive step \verb+(y:nat)(P y)->(P (S y))+.
+In each case we get an instance of function \verb:plus: in which its second
+argument starts with a constructor, and is thus amenable to simplification
+by primitive recursion. The \Coq~tactic \verb:Simpl: can be used for
+this purpose:
+\begin{coq_example}
+Simpl.
+Auto.
+\end{coq_example}
+
+We proceed in the same way for the base step:
+\begin{coq_example}
+Simpl; Auto.
+Save.
+\end{coq_example}
+
+Here \verb:Auto: succeded, because it used as a hint lemma \verb:eq_S:,
+which say that successor preserves equality:
+\begin{coq_example}
+Check eq_S.
+\end{coq_example}
+
+Actually, let us see how to declare our lemma \verb:plus_n_O: as a hint
+to be used by \verb:Auto::
+\begin{coq_example}
+Hints Resolve plus_n_O.
+\end{coq_example}
+
+We now proceed to the similar property concerning the other constructor
+\verb:S::
+\begin{coq_example}
+Lemma plus_n_S : (n,m:nat)(S (plus n m))=(plus n (S m)).
+\end{coq_example}
+
+We now go faster, remembering that tactic \verb:Induction: does the
+necessary \verb:Intros: before applying \verb:Elim:. Factoring simplification
+and automation in both cases thanks to tactic composition, we prove this
+lemma in one line:
+\begin{coq_example}
+Induction n; Simpl; Auto.
+Save.
+Hints Resolve plus_n_S.
+\end{coq_example}
+
+Let us end this exercise with the commutativity of \verb:plus::
+
+\begin{coq_example}
+Lemma plus_com : (n,m:nat)(plus n m)=(plus m n).
+\end{coq_example}
+
+Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the
+situation being symmetric. For instance:
+\begin{coq_example}
+Induction m; Simpl; Auto.
+\end{coq_example}
+
+Here \verb:Auto: succeded on the base case, thanks to our hint \verb:plus_n_O:,
+but the induction step requires rewriting, which \verb:Auto: does not handle:
+
+\begin{coq_example}
+Intros m' E; Rewrite <- E; Auto.
+Save.
+\end{coq_example}
+
+%CP - non ce n'est pas un bon exemple de Immediate.
+%A symmetric lemma such \verb:plus_com: should not be declared as a hint,
+%because \verb:Auto: would lose time by applying it repeatedly without progress.
+%A variant of command \verb:Hint:, called \verb:Immediate:, allows a restricted
+%use of such lemmas:
+%\begin{coq_example}
+%Immediate plus_com.
+%\end{coq_example}
+
+\subsection{Discriminate}
+
+It is also possible to define new propositions by primitive recursion.
+Let us for instance define the predicate which discriminates between
+the constructors \verb:O: and \verb:S:: it computes to \verb:False: 
+when its argument is \verb:O:, and to \verb:True: when its argument is 
+of the form \verb:(S n)::
+\begin{coq_example}
+Definition Is_S
+      := [n:nat]Cases n of O => False | (S p) => True end.
+\end{coq_example}
+
+Now we may use the computational power of \verb:Is_S: in order to prove
+trivially that \verb:(Is_S (S n))::
+\begin{coq_example}
+Lemma S_Is_S : (n:nat)(Is_S (S n)).
+Simpl; Trivial.
+Save.
+\end{coq_example}
+
+But we may also use it to transform a \verb:False: goal into 
+\verb:(Is_S O):. Let us show a particularly important use of this feature;
+we want to prove that \verb:O: and \verb:S: construct different values, one
+of Peano's axioms:
+\begin{coq_example}
+Lemma no_confusion : (n:nat)~(O=(S n)).
+\end{coq_example}
+
+First of all, we replace negation by its definition, by reducing the
+goal with tactic \verb:Red:; then we get contradiction by successive
+\verb:Intros::
+\begin{coq_example}
+Red; Intros n H.
+\end{coq_example}
+
+Now we use our trick:
+\begin{coq_example}
+Change (Is_S O).
+\end{coq_example}
+
+Now we use equality in order to get a subgoal which computes out to 
+\verb:True:, which finishes the proof:
+\begin{coq_example}
+Rewrite H; Trivial.
+Simpl; Trivial.
+\end{coq_example}
+
+Actually, a specific tactic \verb:Discriminate: is provided
+to produce mechanically such proofs, without the need for the user to define
+explicitly the relevant discrimination predicates:
+
+\begin{coq_example}
+Restart.
+Intro n; Discriminate.
+Save.
+\end{coq_example}
+
+
+\section{Logic programming}
+
+In the same way as we defined standard data-types above, we
+may define inductive families, and for instance inductive predicates.
+Here is the definition of predicate $\le$ over type \verb:nat:, as
+given in \Coq's \verb:Prelude: module:
+\begin{coq_example*}
+Inductive le [n:nat] : nat -> Prop
+   := le_n : (le n n)
+    | le_S : (m:nat)(le n m)->(le n (S m)).
+\end{coq_example*}
+
+This definition introduces a new predicate \verb+le:nat->nat->Prop+,
+and the two constructors \verb:le_n: and \verb:le_S:, which are the
+defining clauses of \verb:le:. That is, we get not only the ``axioms''
+\verb:le_n: and \verb:le_S:, but also the converse property, that 
+\verb:(le n m): if and only if this statement can be obtained as a
+consequence of these defining clauses; that is, \verb:le: is the
+minimal predicate verifying clauses \verb:le_n: and \verb:le_S:. This is
+insured, as in the case of inductive data types, by an elimination principle,
+which here amounts to an induction principle \verb:le_ind:, stating this 
+minimality property:
+\begin{coq_example}
+Check le.
+Check le_ind.
+\end{coq_example}
+
+Let us show how proofs may be conducted with this principle.
+First we show that $n\le m \Rightarrow n+1\le m+1$:
+\begin{coq_example}
+Lemma le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
+Intros n m n_le_m.
+Elim n_le_m.
+\end{coq_example}
+
+What happens here is similar to the behaviour of \verb:Elim: on natural
+numbers: it appeals to the relevant induction principle, here \verb:le_ind:,
+which generates the two subgoals, which may then be solved easily
+%as if ``backchaining'' the current goal
+with the help of the defining clauses of \verb:le:.
+\begin{coq_example}
+Apply le_n; Trivial.
+Intros; Apply le_S; Trivial.
+\end{coq_example}
+
+Now we know that it is a good idea to give the defining clauses as hints,
+so that the proof may proceed with a simple combination of 
+\verb:Induction: and \verb:Auto:.
+\begin{coq_example}
+Restart.
+Hints Resolve le_n le_S.
+\end{coq_example}
+
+We have a slight problem however. We want to say ``Do an induction on
+hypothesis \verb:(le n m):'', but we have no explicit name for it. What we
+do in this case is to say ``Do an induction on the first unnamed hypothesis'',
+as follows.
+\begin{coq_example}
+Induction 1; Auto.
+Save.
+\end{coq_example}
+
+Here is a more tricky problem. Assume we want to show that
+$n\le 0 \Rightarrow n=0$. This reasoning ought to follow simply from the
+fact that only the first defining clause of \verb:le: applies.
+\begin{coq_example} 
+Lemma tricky : (n:nat)(le n O)->n=O.
+\end{coq_example}
+
+However, here trying something like \verb:Induction 1: would lead
+nowhere (try it and see what happens). 
+An induction on \verb:n: would not be convenient either.
+What we must do here is analyse the definition of \verb"le" in order
+to match hypothesis \verb:(le n O): with the defining clauses, to find
+that only \verb:le_n: applies, whence the result. 
+This analysis may be performed by the ``inversion'' tactic
+\verb:Inversion_clear: as follows:
+\begin{coq_example} 
+Intros n H; Inversion_clear H.
+Trivial.
+Save.
+\end{coq_example}
+
+\chapter{Modules}
+
+\section{Opening library modules}
+
+When you start \Coq~ without further requirements in the command line,
+you get a bare system with few libraries loaded.  As we saw, a standard
+prelude module provides the standard logic connectives, and a few
+arithmetic notions. If you want to load and open other modules from
+the library, you have to use the \verb"Require" command, as we saw for
+classical logic above. For instance, if you want more arithmetic
+constructions, you should request:
+\begin{coq_example*}
+Require Arith.
+\end{coq_example*}
+
+Such a command looks for a (compiled) module file \verb:Arith.vo:
+on the current \verb:LoadPath:. This loadpath may be changed
+with the commands \verb:AddPath: and \verb:DelPath:.
+
+The loading of such a compiled file is quick, because the corresponding
+development is not typechecked again. This is a great saving compared
+to previous versions of our proof assistant.
+
+If you want to recursively import modules which are required for module
+M, you should use \verb:Require Export M:. 
+
+{\bf Warning} \Coq~ does not yet provides parametric modules.
+
+\section{Creating your own modules}
+
+You may create your own modules, by writing \Coq~ commands in a file,
+say \verb:my_module.v:. Such a module may be simply loaded in the current
+context, with command \verb:Load my_module:. It may also be compiled,
+using the command \verb:Compile Module my_module: directly at the
+\Coq~ toplevel, or else in ``batch'' mode, using the UNIX command
+\verb:coqc:. Compiling the module \verb:my_module.v: creates a 
+file \verb:my_module.vo: that can be reloaded with command
+\verb:Require my_module:. 
+
+%CP- Non compatible avec la version distribuee.
+%Compiling a module creates actually 2 files in the current version:
+%\verb:my_module.vi: and \verb:my_module.vo:. This last file is
+%bigger, because it stores the value of opaque constants, such as the
+%proofs of lemmas. If you want to be able to turn such constants as
+%transparent constants (whose definition may be unfolded), you must
+%use the command \verb:Require Implementation my_module:.
+
+\section{Managing the context}
+
+It is often difficult to remember the names of all lemmas and
+definitions available in the current context, especially if large
+libraries have been loaded. A convenient \verb:Search: command
+is available to lookup all known facts 
+concerning a given predicate. For instance, if you want to know all the
+known lemmas about the less or equal relation, juste ask:
+\begin{coq_example}
+Search le.
+\end{coq_example}
+
+A new and more convenient search tool is \textsf{SearchIsos}. The
+argument to give is a type and it searches in the current context all
+constants having the same type modulo certain notion of
+\textit{isomorphism}. For example~:
+
+\begin{coq_example}
+Require Arith.
+SearchIsos nat -> nat -> Prop.
+SearchIsos (x,y,z:nat)(le x y) -> (le y z) -> (le x z).
+\end{coq_example} 
+ 
+\section{Now you are on your own}
+
+This tutorial is necessarily incomplete. If you wish to pursue serious
+proving in \Coq, you should now get your hands on \Coq's Reference Manual,
+which contains a complete description of all the tactics we saw, 
+plus many more.
+You also should look in the library of developed theories which is distributed
+with \Coq, in order to acquaint yourself with various proof techniques.
+
+
+\end{document}
+
+% $Id$ 
-- 
cgit v1.2.3

