aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-28 17:37:48 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-28 17:37:48 +0200
commit38bfc475b03194c5717ecab581cf9fb75422ea1a (patch)
tree6e473e82436667d06d704350d45c66bb03926554
parent4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (diff)
Update the Tutorial.
-rw-r--r--doc/tutorial/Tutorial.tex218
1 files changed, 106 insertions, 112 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 30b6304c1..75318c896 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -23,7 +23,7 @@ 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
@@ -33,23 +33,23 @@ proof tools. For more advanced information, the reader could refer to
the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y.
Bertot and P. Castéran on practical uses of the \Coq{} system.
-Coq can be used from a standard teletype-like shell window but
-preferably through the graphical user interface
-CoqIde\footnote{Alternative graphical interfaces exist: Proof General
-and Pcoq.}.
+Coq can be tested through a REPL (Read-Eval-Print-Loop) called
+\texttt{coqtop} but for actual developments it is preferable to use
+a graphical user interface such as CoqIDE or
+Proof General\footnote{See \url{https://proofgeneral.github.io/}.}.
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 \url{https://coq.inria.fr/}.
-In the following, we assume that \Coq{} is called from a standard
-teletype-like shell window. All examples preceded by the prompting
+The following examples are executed within \texttt{coqtop}.
+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. When used from a graphical user interface such as
-CoqIde, the prompt is not displayed: user input is given in one window
+CoqIDE, the prompt is not displayed: user input is given in one window
and \Coq's answers are displayed in a different window.
The sequence of such examples is a valid \Coq{}
@@ -61,7 +61,7 @@ invocation of \Coq{} delivers a message such as:
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
-Welcome to Coq 8.2 (January 2009)
+Welcome to Coq 8.7 (June 2017)
Coq <
\end{verbatim}
@@ -69,8 +69,8 @@ Coq <
\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 bug-tracking system
+used. You should always return this version number when you report an
+anomaly to our bug-tracking system
\url{https://coq.inria.fr/bugs/}.
\chapter{Basic Predicate Calculus}
@@ -175,7 +175,7 @@ arrow function constructor, in order to get a functional type
\begin{coq_example}
Check (nat -> Prop).
\end{coq_example}
-which may be composed one more times with \verb:nat: in order to obtain the
+which may be composed once more with \verb:nat: in order to obtain the
type \verb:nat->nat->Prop: of binary relations over natural numbers.
Actually the type \verb:nat->nat->Prop: is an abbreviation for
\verb:nat->(nat->Prop):.
@@ -340,17 +340,12 @@ the current goal is solvable from the current local assumptions:
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::
+The proof is now finished. We are now going to ask to \Coq{}'s kernel
+to check and save the proof.
\begin{coq_example}
-Save trivial_lemma.
+Qed.
\end{coq_example}
-As a comment, the system shows the proof script listing all tactic
-commands used in the proof.
-
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}
@@ -383,14 +378,14 @@ We may thus complete the proof of \verb:distr_impl: with one composite tactic:
apply H; [ assumption | apply H0; assumption ].
\end{coq_example}
+It is discouraged though to rely on automatically generated names in finished
+proof scripts. And be careful not to abuse \verb:;:.
+
Let us now save lemma \verb:distr_impl::
\begin{coq_example}
Qed.
\end{coq_example}
-Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl:
-in advance.
-
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:
@@ -410,18 +405,8 @@ 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:
-\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.
+backtrack n steps. None of these commands should be left in a finished proof
+document.
\section{Propositional Calculus}
@@ -438,7 +423,7 @@ connective. Let us show how to use these ideas for the propositional connectives
\begin{coq_example}
Lemma and_commutative : A /\ B -> B /\ A.
-intro.
+intro H.
\end{coq_example}
We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic,
@@ -465,7 +450,7 @@ conjunction introduction operator \verb+conj+
Check conj.
\end{coq_example}
-Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+
+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
@@ -498,6 +483,14 @@ clear away unnecessary hypotheses which may clutter your screen.
clear H.
\end{coq_example}
+The tactic \verb:destruct: combines the effects of \verb:elim:, \verb:intros:,
+and \verb:clear::
+
+\begin{coq_example}
+Restart.
+intros H; destruct 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
@@ -542,7 +535,7 @@ 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 =>+,
+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):
@@ -572,7 +565,7 @@ 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
+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.
@@ -652,15 +645,11 @@ function and predicate symbols.
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
+variety of types, so we 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:.
+respectively 1 and 2.
\begin{coq_example}
Reset Initial.
@@ -669,8 +658,7 @@ Reset Initial.
Set Printing Width 60.
\end{coq_eval}
-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
+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.
@@ -686,18 +674,18 @@ 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.
+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
+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.
+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
@@ -711,13 +699,13 @@ 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
-the expression \verb+(ex D (fun x:D => P x))+.
+and the notation \verb+(exists x : D, P x)+ is just concrete syntax for
+the expression \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
+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+
+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.
@@ -802,7 +790,7 @@ Lemma weird : (forall x:D, P x) -> exists a, P a.
\end{coq_example}
First of all, notice the pair of parentheses around
-\verb+forall x:D, P x+ in
+\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
@@ -820,7 +808,7 @@ 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:
+Let us conclude the proof, in order to show the use of the \verb:exists:
tactic:
\begin{coq_example}
exists d; trivial.
@@ -836,8 +824,8 @@ 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.
+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
@@ -847,10 +835,11 @@ proper instance of \verb:EM::
elim (EM (exists x, ~ P x)).
\end{coq_example}
-We first look at the first case. Let Tom be the non-drinker:
+We first look at the first case. Let Tom be the non-drinker.
+The following combines at once the effect of \verb:intros: and
+\verb:destruct::
\begin{coq_example}
-intro Non_drinker; elim Non_drinker;
- intros Tom Tom_does_not_drink.
+intros (Tom, Tom_does_not_drink).
\end{coq_example}
We conclude in that case by considering Tom, since his drinking leads to
@@ -860,9 +849,10 @@ 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:
+in this case, we use \verb:contradiction: to let \Coq{} find out the
+two contradictory hypotheses:
\begin{coq_example}
-absurd (P Tom); trivial.
+contradiction.
\end{coq_example}
We now proceed with the second case, in which actually any person will do;
@@ -935,12 +925,12 @@ 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:
+Sometimes it may be convenient to state an intermediate fact.
+The tactic \verb:assert: does this and introduces a new subgoal
+for this fact to be proved first. The tactic \verb:enough: does
+the same while keeping this goal for later.
\begin{coq_example}
-cut (R x x); trivial.
+enough (R x x) by auto.
\end{coq_example}
We clean the goal by doing an \verb:Abort: command.
\begin{coq_example*}
@@ -951,7 +941,7 @@ Abort.
\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
+\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:.
@@ -1011,8 +1001,8 @@ $t$ is an assumption
corresponding goal will not appear. For instance:
\begin{coq_example}
Restart.
-replace (f 0) with 0.
-rewrite f10; rewrite foo; trivial.
+replace (f 1) with (f 0).
+replace (f 0) with 0; trivial.
Qed.
\end{coq_example}
@@ -1033,20 +1023,20 @@ predicates over some universe \verb:U:. For instance:
\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.
+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.
+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:
+We want to prove that \verb:subset: is a \verb:transitive:
relation.
\begin{coq_example}
Lemma subset_transitive : transitive set subset.
@@ -1166,11 +1156,11 @@ right; trivial.
\end{coq_example}
Indeed, the whole proof can be done with the combination of the
- \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
+ \verb:destruct:, which combines \verb:intro: and \verb:elim:,
with good old \verb:auto::
\begin{coq_example}
Restart.
-simple induction b; auto.
+destruct b; auto.
Qed.
\end{coq_example}
@@ -1194,7 +1184,7 @@ Check nat_rec.
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).
+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
@@ -1205,22 +1195,25 @@ About 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}:
+get an apparently more complicated expression.
+In fact, the two types are convertible and one way of having the proper
+type would be to do some computation before actually defining \verb:prim_rec:
+as such:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
\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).
+Definition prim_rec :=
+ Eval compute in nat_rec (fun i : nat => nat).
+About prim_rec.
\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.
+ 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:
@@ -1269,9 +1262,9 @@ 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
+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)+.
+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
@@ -1305,12 +1298,12 @@ We now proceed to the similar property concerning the other constructor
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
+We now go faster, using the tactic \verb:induction: which 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.
+induction n; simpl; auto.
Qed.
Hint Resolve plus_n_S .
\end{coq_example}
@@ -1324,7 +1317,7 @@ Lemma plus_com : forall n m:nat, n + m = m + n.
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.
+induction m; simpl; auto.
\end{coq_example}
Here \verb:auto: succeeded on the base case, thanks to our hint
@@ -1332,7 +1325,7 @@ Here \verb:auto: succeeded on the base case, thanks to our hint
\verb:auto: does not handle:
\begin{coq_example}
-intros m' E; rewrite <- E; auto.
+rewrite <- IHm; auto.
Qed.
\end{coq_example}
@@ -1344,10 +1337,10 @@ 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.
+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
@@ -1403,12 +1396,13 @@ 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 :=
+Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
- | le_S : forall m:nat, le n m -> le n (S m).
+ | 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+,
+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
@@ -1442,10 +1436,11 @@ intros; apply le_S; trivial.
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:.
+\verb:induction: and \verb:auto:. \verb:Hint Constructors le:
+is just an abbreviation for \verb:Hint Resolve le_n le_S:.
\begin{coq_example}
Restart.
-Hint Resolve le_n le_S .
+Hint Constructors le.
\end{coq_example}
We have a slight problem however. We want to say ``Do an induction on
@@ -1453,7 +1448,7 @@ 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.
+induction 1; auto.
Qed.
\end{coq_example}
@@ -1562,14 +1557,13 @@ predicate appears at the head position in the conclusion.
SearchHead le.
\end{coq_example}
-A new and more convenient search tool is \verb:SearchPattern:
-developed by Yves Bertot. It allows finding the theorems with a
-conclusion matching a given pattern, where \verb:_: can be used in
+The \verb:Search: commands also allows finding the theorems
+containing 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 (_ + _ = _).
+Search (_ + _ = _).
\end{coq_example}
\section{Now you are on your own}