diff options
Diffstat (limited to 'doc/Tutorial.tex')
| -rwxr-xr-x | doc/Tutorial.tex | 1563 |
1 files changed, 1563 insertions, 0 deletions
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$ |