diff options
Diffstat (limited to 'doc/tutorial/Tutorial.tex')
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 1584 |
1 files changed, 1584 insertions, 0 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex new file mode 100755 index 00000000..7c840509 --- /dev/null +++ b/doc/tutorial/Tutorial.tex @@ -0,0 +1,1584 @@ +\documentclass[11pt,a4paper]{book} +\usepackage[T1]{fontenc} +\usepackage[latin1]{inputenc} +\usepackage{pslatex} + +\input{../common/version.tex} +\input{../common/macros.tex} +\input{../common/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. For more advanced information, the reader could refer to +the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. +Bertot and P. Castéran on practical uses of the \Coq{} system. + +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. +Instructions on installation procedures, as well as more comprehensive +documentation, may be found in the standard distribution of \Coq, +which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}. + +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 +screen. The sequence of such examples is a valid \Coq~ session, unless +otherwise specified. This version of the tutorial has been prepared +on a PC workstation running Linux. +The standard invocation of \Coq\ delivers a message such as: + +\begin{small} +\begin{flushleft} +\begin{verbatim} +unix:~> coqtop +Welcome to Coq 8.0 (Mar 2004) + +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 hot-line \verb:coq-bugs@pauillac.inria.fr: or on our +bug-tracking system~:\verb:http://coq.inria.fr/bin/coq-bugs: + +\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 judgment 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 +notions which are defined in the arithmetic prelude, +automatically loaded when running the \Coq\ system. + +We start by introducing a so-called section name. The role of sections +is to structure the modelisation by limiting the scope of parameters, +hypotheses and definitions. It will also give a convenient way to +reset part of the development. + +\begin{coq_example} +Section Declaration. +\end{coq_example} +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 0). +\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 : nat := S two. +\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} +This definition introduces the constant \texttt{double} defined as the +expression \texttt{fun m:nat => plus m m}. +The abstraction introduced by \texttt{fun} is explained as follows. The expression +\verb+fun 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 \verb+x+ is a bound, or dummy variable in +the expression \verb+fun x:A => e+. For instance we could as well have +defined \verb:double: as \verb+fun 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+forall 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 (forall m:nat, gt m 0). +\end{coq_example} +We may clean-up the development by removing the contents of the +current section: +\begin{coq_example} +Reset Declaration. +\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} +Section Minimal_Logic. +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 judgment}. +%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 judgment, possibly from proofs of some +hypothetical judgments, which are then added to the current +list of conjectured judgments. +For instance, the \verb:intro: tactic is applicable to any judgment +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 judgments 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 judgment, which are still available for +the judgments 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 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 conjunction 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. +Qed. +\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:Hint 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} +The tactic \verb:trivial: works like \verb:auto: with the hints +database, but it only tries those tactics that can solve the goal in one +step. + +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. +Qed. +\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 \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, +corresponds +to \verb:intro H:, whereas a subterm such as +\verb:(or_intror: \verb:B H0): +corresponds to the sequence \verb:apply or_intror; exact H0:. +The generic combinator \verb:or_intror: needs to be instantiated by +the two properties \verb:B: and \verb:A:. Because \verb:A: can be +deduced from the type of \verb:H0:, only \verb:B: is printed. +The two instantiations 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. +Qed. +\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. +Qed. +\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 Import 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. +Qed. +\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. +Variables 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. +Qed. +\end{coq_example} +At that point \verb:NoMember: is a proof of the absurdity depending on +hypotheses. +We may end the section, in that case, the variables and hypotheses +will be discharged, and the type of \verb:NoMember: will be +generalised. + +\begin{coq_example} +End club. +Check NoMember. +\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 as we did before to +remove a section, or we may return to the initial state using~: +\begin{coq_example} +Reset Initial. +\end{coq_example} + +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 : forall x y:D, R x y -> R y x. +Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z. +\end{coq_example} + +Remark the syntax \verb+forall 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 : forall x:D, (exists 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+(exists x:D, P x)+ is just concrete syntax for +\verb+(ex D (fun 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:intros: treats universal quantification in the same way +as the premises 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 instantiate \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*} +Qed. +\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 : (forall x:D, P x) -> exists a, P a. + intro UnivP. +\end{coq_example} + +First of all, notice the pair of parentheses around +\verb+forall x:D, P x+ in +the statement of lemma \verb:weird:. +If we had omitted 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. +Qed. +\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 : forall A:Prop, A \/ ~ A. +Lemma drinker : exists x:D, P x -> forall 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 (exists 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-emptiness 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 (exists x, ~ P x); trivial. +exists Dick; trivial. +Qed. +\end{coq_example} + +Now, let us close the main section and look at the complete statements +we proved: +\begin{coq_example} +End Predicate_calculus. +Check refl_if. +Check weird. +Check drinker. +\end{coq_example} + +Remark how the three theorems are completely generic in 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 pretty-printer replaces +systematically a quantification such as \verb+forall 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} +Section Predicate_Calculus. +Variables P Q : nat -> Prop. +Variable R : nat -> nat -> Prop. +Lemma PQR : + forall 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} +We clean the goal by doing an \verb:Abort: command. +\begin{coq_example*} +Abort. +\end{coq_example*} + + +\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 0 = 0. +\end{coq_example} + +We want to prove the following conditional equality: +\begin{coq_example*} +Lemma L1 : forall k:nat, k = 0 -> 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:. + +Now \verb:apply foo: will finish the proof: + +\begin{coq_example} +apply foo. +Qed. +\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} +Hypothesis f10 : f 1 = f 0. +Lemma L2 : f (f 1) = 0. +replace (f 1) with 0. +\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 applying lemma \verb:foo:; the second one transitivity and then +symmetry of equality, for instance with tactics \verb:transitivity: and +\verb:symmetry:: +\begin{coq_example} +apply foo. +transitivity (f 0); symmetry; trivial. +\end{coq_example} +In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with: +$t$ is an assumption +(possibly modulo symmetry), it will be automatically proved and the +corresponding goal will not appear. For instance: +\begin{coq_example} +Restart. +replace (f 0) with 0. +rewrite f10; rewrite foo; trivial. +Qed. +\end{coq_example} + +\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 instantiates 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) := forall 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) := + forall 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 subset at 2. +\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. +Qed. +\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 | false. +\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 : forall 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:simple induction: tactic, which combines \verb:intro: and \verb:elim:, +with good old \verb:auto:: +\begin{coq_example} +Restart. +simple induction b; auto. +Qed. +\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 (fun 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 + ((fun _:nat => nat) O -> + (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) -> + forall n:nat, (fun _: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 (fun p 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/match} for generic primitive recursion, +and we could thus have defined directly addition as: + +\begin{coq_example} +Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | 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. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +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 : forall n:nat, n = n + 0. +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 +exactly Peano's induction scheme. Pattern-matching instantiated the +corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get +as subgoals the corresponding instantiations of the base case \verb:(P O): , +and of the inductive step \verb+forall 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. +Qed. +\end{coq_example} + +Here \verb:auto: succeeded, 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} +Hint 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 : forall n m:nat, S (n + m) = n + S m. +\end{coq_example} + +We now go faster, remembering that tactic \verb:simple 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} +simple induction n; simpl; auto. +Qed. +Hint Resolve plus_n_S . +\end{coq_example} + +Let us end this exercise with the commutativity of \verb:plus:: + +\begin{coq_example} +Lemma plus_com : forall n m:nat, n + m = 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} +simple induction m; simpl; auto. +\end{coq_example} + +Here \verb:auto: succeeded 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. +Qed. +\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) := match n with + | 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 : forall n:nat, Is_S (S n). +simpl; trivial. +Qed. +\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 : forall n:nat, 0 <> 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 0). +\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. +Qed. +\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 : forall 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 : forall 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. +Hint 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} +simple induction 1; auto. +Qed. +\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 : forall n:nat, le n 0 -> n = 0. +\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. +Qed. +\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 Import Arith. +\end{coq_example*} + +Such a command looks for a (compiled) module file \verb:Arith.vo: in +the libraries registered by \Coq. Libraries inherit the structure of +the file system of the operating system and are registered with the +command \verb:Add LoadPath:. Physical directories are mapped to +logical directories. Especially the standard library of \Coq~ is +pre-registered as a library of name \verb=Coq=. Modules have absolute +unique names denoting their place in \Coq~ libraries. An absolute +name is a sequence of single identifiers separated by dots. E.g. the +module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because +it resides in eponym subdirectory \verb=Arith= of the standard +library, it can be as well required by the command + +\begin{coq_example*} +Require Import Coq.Arith.Arith. +\end{coq_example*} + +This may be useful to avoid ambiguities if somewhere, in another branch +of the libraries known by Coq, another module is also called +\verb=Arith=. Notice that by default, when a library is registered, +all its contents, and all the contents of its subdirectories recursively are +visible and accessible by a short (relative) name as \verb=Arith=. +Notice also that modules or definitions not explicitly registered in +a library are put in a default library called \verb=Top=. + +The loading of a compiled file is quick, because the corresponding +development is not type-checked again. + +\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 Import my_module:. + +If a required module depends on other modules then the latters are +automatically required beforehand. However their contents is not +automatically visible. If you want a module \verb=M= required in a +module \verb=N= to be automatically visible when \verb=N= is required, +you should use \verb:Require Export M: in your module \verb:N:. + +\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:SearchAbout: 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, just ask: +\begin{coq_example} +SearchAbout le. +\end{coq_example} +Another command \verb:Search: displays only lemmas where the searched +predicate appears at the head position in the conclusion. +\begin{coq_example} +Search le. +\end{coq_example} + +A new and more convenient search tool is \textsf{SearchPattern} +developed by Yves Bertot. It allows to find the theorems with a +conclusion matching a given pattern, where \verb:\_: can be used in +place of an arbitrary term. We remark in this example, that \Coq{} +provides usual infix notations for arithmetic operators. + +\begin{coq_example} +SearchPattern (_ + _ = _). +\end{coq_example} + +% 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: Tutorial.tex 8607 2006-02-23 14:21:14Z herbelin $ |