Skip to content

Instantly share code, notes, and snippets.

@ppedrot

ppedrot/RefMan-gal.tex

Created July 18, 2022 15:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ppedrot/2c77536a7fe70416624e9b63c0e3d54c to your computer and use it in GitHub Desktop.
Save ppedrot/2c77536a7fe70416624e9b63c0e3d54c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
RefMan-gal.tex
\chapter{The {\sf Gallina} specification language}\label{Gallina}\index{Gallina}
\section{Lexical conventions}\label{lexical}\index{Lexical conventions}
\paragraph{Blanks}
Space, newline and horizontal tabulation are considered as blanks.
Blanks are ignored but they separate tokens.
\paragraph{Comments}
Comments in {\Coq} are enclosed between {\tt (*} and {\tt
*)}\index{Comments}, and can be nested. Comments are treated as
blanks.
\paragraph{Identifiers}
Identifiers are sequences of letters, digits, \verb!_!, \verb!$! %$
and \verb!'!, that do not start with a digit or \verb!'!. That is,
they are recognized by the following regular expression
\def\ml#1{\hbox{\tt#1}}%
\def\op{\,|\,}%
\begin{center}
\begin{tabular}{r@{\ ::=\ }l}
{\sl ident} & $(\,\ml{a..z}\op\ml{A..Z}\op\ml{\_}\op\ml{\$}\,) %$
\{\,\ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}%
\op\ml{\$}\op\ml{'}\,\}^+$ %$
\end{tabular}
\end{center}
Identifiers can contain at most 80 characters, and all characters are
meaningful.
\paragraph{Integers}
Integers are sequences of digits, optionally preceded by a minus sign,
that is
\begin{center}
\begin{tabular}{r@{\quad::=\quad}l}
{\sl integer} & $[\ml{-}]\,\{\,\ml{0..9}\,\}^+$
\end{tabular}
\end{center}
\paragraph{Strings}
Strings are delimited by \verb!"! (double quote), and enclose a
sequence of any characters different from \verb!"! and \verb!\!, or
one of the following sequences
\begin{center}
\begin{tabular}{|l|l|}
\hline
Sequence & Character denoted \\
\hline
\verb"\\" & backslash (\verb"\") \\
\verb'\"' & double quote (\verb'"') \\
\verb"\n" & newline (LF) \\
\verb"\r" & return (CR) \\
\verb"\t" & horizontal tabulation (TAB) \\
\verb"\b" & backspace (BS) \\
\verb"\"$ddd$ & the character with ASCII code $ddd$ in decimal \\
\hline
\end{tabular}
\end{center}
Strings can be split on several lines using a backslash (\verb!\!) at
the end of each line, just before the newline. For instance,
\begin{coq_example*}
AddPath "$COQTOP/\
contrib/Rocq/LAMBDA".
\end{coq_example*}
is correctly parsed, and equivalent to
\begin{coq_example*}
AddPath "$COQTOP/contrib/Rocq/LAMBDA".
\end{coq_example*}
\paragraph{Keywords}
The following identifiers are reserved keywords, and cannot be
employed otherwise:
\begin{center}
\begin{tabular}{lllll}
\verb!AddPath! &
\verb!Definition! &
\verb!DelPath! &
\verb!Dependent! &
\verb!end! \\
\verb!Grammar! &
\verb!Inductive! &
\verb!CoInductive! &
\verb!in! &
\verb!Load! \\
\verb!LoadPath! &
\verb!NewSyntax! &
\verb!Non! &
\verb!Orelse! &
\verb!Proof! \\
\verb!Qed! &
\verb!Quit! &
\verb!Remove! &
\verb!Reset! &
\verb!Restore! \\
\verb!State! &
\verb!Syntax! &
\verb!with! &
\verb!using!
\end{tabular}
\end{center}
Although they are not considered as keywords, it is inadvisable to use
words of the following list as identifiers:
\begin{center}
\begin{tabular}{lllll}
\verb!Abort! &
\verb!Abstraction! &
\verb!All! &
\verb!Axiom! &
\verb!Begin! \\
\verb!Cd! &
\verb!Chapter! &
\verb!Check! &
\verb!CheckGuard! &
\verb!CoFixpoint! \\
\verb!Compute! &
\verb!Defined! &
\verb!Definition! &
\verb!Drop! &
\verb!Elimination! \\
\verb!End! &
\verb!Eval! &
\verb!Explain! &
\verb!Extraction! &
\verb!Fact! \\
\verb!Fixpoint! &
\verb!Focus! &
\verb!for! &
\verb!Go! &
\verb!Goal! \\
\verb!Hint! &
\verb!Hypothesis! &
\verb!Immediate! &
\verb!Induction! &
\verb!Infix! \\
\verb!Inspect! &
\verb!Lemma! &
\verb!Let! &
\verb!Local! &
\verb!Minimality! \\
\verb!ML! &
\verb!Module! &
\verb!Modules! &
\verb!Mutual! &
\verb!Node! \\
\verb!Opaque! &
\verb!Parameter! &
\verb!Parameters! &
\verb!Print! &
\verb!Proofs! \\
\verb!Prop! &
\verb!Pwd! &
\verb!Qed! &
\verb!Remark! &
\verb!Require! \\
\verb!Restart! &
\verb!Resume! &
\verb!Save! &
\verb!Scheme! &
\verb!Script! \\
\verb!Search! &
\verb!Section! &
\verb!Set! &
\verb!Show! &
\verb!Silent! \\
\verb!States! &
\verb!Suspend! &
\verb!Syntactic! &
\verb!Theorem! &
\verb!Token! \\
\verb!Transparent! &
\verb!Tree! &
\verb!Type! &
\verb!Typeset! &
\verb!Undo! \\
\verb!Unfocus! &
\verb!Variable! &
\verb!Variables! &
\verb!Write!
\end{tabular}
\end{center}
\paragraph{Other keywords and user's tokens}
The following sequences of characters are also keywords:
\begin{center}
\begin{tabular}{lllllll}
\verb!|! &
\verb!:! &
\verb!:=! &
\verb!=! &
\verb!>! &
\verb!>>! &
\verb!<>! \\
\verb!<<! &
\verb!<! &
\verb!->! &
\verb!;! &
\verb!#! &
\verb!*! &
\verb!,! \\
\verb!?! &
\verb!@! &
\verb!::! &
\verb!/! &
\verb!<-! & &
\end{tabular}
\end{center}
You can add new tokens with the command {\tt Token} (see
section~\ref{Token}). New tokens must be sequences, without blanks,
of characters taken from the following list:
\begin{center}
\verb"< > / \ - + = ; , | ! @ # % ^ & ? * : ~ $ _ a..z A..Z ' 0..9" %$
\end{center}
that do not start with a character from
\begin{center}
\verb!$ _ a..z A..Z ' 0..9! %$
\end{center}
Lexical ambiguities are resolved according to the ``longest match''
rule: when a sequence of the previous characters can be decomposed
into several different ways, then the first token is the longest
possible one (among all tokens defined at this moment), and so on.
\section{Basic syntax of terms}\label{term}\index{Terms}
The basic set of terms form the {\em Calculus of Inductive
Constructions} also called {\sc Cic}. The formal presentation of
{\sc Cic} is given in chapter \ref{Cic}. We give here (an
approximation of) the syntax available in \Coq.
\\[0.3cm]
\begin{tabular}{lcl}
{\term} & ::= & \ident\\
& $|$ & \sort \\
& $|$ & {\tt (} {\binder} {\tt )} {\term}\\
& $|$ & {\tt [} {\binder} {\tt ]} {\term}\\
& $|$ & {\tt [} {\lident} {\tt ]} {\term}\\
& $|$ & {\tt [} {\ident} {\tt =} {\term} {\tt ]} {\term}\\
& $|$ & {\tt (} {\terms} {\tt )}\\
& $|$ & {\tt <} {\term} {\tt >Case} {\term} {\tt of}
{\terms} {\tt end}\\
& $|$ & {\tt Fix} {\ident} \verb.{. {\rm\sl fixdecls} \verb.}.\\
& $|$ & {\tt <} {\term} {\tt >Match} {\term} {\tt with}
{\terms} {\tt end}\\
& $|$ & {\tt <} {\term} {\tt >let (} {\params} {\tt ) =}
{\term} {\tt in} {\term} \\
& $|$ & {\tt <} {\term} {\tt >let (} {\lident} {\tt ) =}
{\term} {\tt in} {\term} \\
& $|$ & {\tt <} {\term} {\tt >if} {\term} {\tt then}
{\term} {\tt else} {\term}\\
{\terms} & ::= & \term \\
& $|$ & {\term} {\terms}\\
{\lident} & ::= & \ident \\
& $|$ & {\ident} {\tt ,} {\lident}\\
{\binder} & ::= & {\lident} {\tt :} {\term}\\
{\params} & ::= & {\binder} \\
& $|$ & {\binder} {\tt ;} {\params}\\
{\sort} & ::= & {\tt Prop} \\
& $|$ & {\tt Set} \\
& $|$ & {\tt Type} \\
& $|$ & {\tt Typeset} \\
{\rm\sl fixdecls} & ::= & {\rm\sl fixdecl} \\
& $|$ & {\rm\sl fixdecl} \verb.with. {\rm\sl fixdecls} \\
{\rm\sl fixdecl} & ::= & {\ident} \verb./. {\num} \verb.:. {\term}
\verb.:=. {\term}
\end{tabular}
\\[0.3cm]
\noindent {\bf Remarks : }
\begin{enumerate}
\item {\tt (} {\terms} {\tt )} associates to the left.
\item The syntax {\tt [} {\lident} {\tt ]} {\term} allows not to
give types in abstractions.
\item The syntax {\tt [} {\ident} {\tt =} {\term} {\tt ]}
{\term} allows to define a $\beta$-redex.
\Example
[x=T$_1$]T$_2$ is equivalent to ([x]T$_2$~T$_1$).
\item The syntax {\tt <} {\term} {\tt >Case} {\term} {\tt of}
{\terms} {\tt end} does case analysis over a term in an
inductive definition. The rules are explained in
section~\ref{Caseexpr}.
\item The syntax {\tt Fix} is used for the internal representation of
fixpoints. It is intended to be used by the commands {\tt Fixpoint}
(see section~\ref{Fixpoint}), {\tt Recursive Definition}
(see section \ref{Recursive-Definition}) and {\tt Scheme} (see
section~\ref{Scheme}). A more precise description of terms built
with {\tt Fix} can be found in section~\ref{Fix-term}.
\item The syntax {\tt <} {\term} {\tt >Match} {\term} {\tt with}
{\terms} {\tt end} is a macro generating a combination of
{\tt Case} with {\tt Fix} implementing a combinator for
primitive recursion equivalent to the {\tt Match}
construction of \Coq\ V5.8. It is explained in
section~\ref{Matchexpr}.
\item The syntax {\tt <} {\term} {\tt >let (} {\params}
{\tt ) =} {\term} {\tt in} {\term} is a macro for
a {\tt Case} with one only case.
\\[0.3cm]
\Variant
The syntax {\tt <} {\term} {\tt >let (} {\lident} {\tt ) =}
{\term} {\tt in} {\term} is a variant of the precedent but
types are not needed in {\lident}.
\item The syntax {\tt <} \term {\tt >if} \term {\tt then}
\term {\tt else} \term is a macro for
a {\tt Case} with two only cases.
\end{enumerate}
\section{Declarations}\index{Declarations}\label{Declarations}
The declaration mechanism allows the user to specify his own basic
objects. Declared objects play the role of axioms or parameters in
mathematics. A declared object is an {\ident} associated to a \term. A
declaration is accepted by {\Coq} iff this {\term} is a well-typed
specification in the current context of the declaration and \ident\ was
not previously defined in the same module. This {\term}
is considered to be the type, or specification, of the \ident.
\subsection{{\tt Axiom {\ident} : {\term}}.}
\label{Axiom}
\index{Axiom@{\tt Axiom}}
\index{Parameter@{\tt Parameter}}
This command links {\term} to the name {\ident} as its specification in the
global context. The fact asserted by {\term} is thus assumed
%without any proof of it.\\
as a postulate.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Clash with previous constant {\ident}}
\end{enumerate}
\Variant
\begin{enumerate}
%\item {\tt Axiom {\lident} : {\term}.}\\
% links {\term} to the names comprising the list {\lident}
% Non documented - useless
\item {\tt Parameter {\ident} : {\term}.}\\ Is equivalent to {\tt
Axiom {\ident} : {\term}}
\item {\tt Parameters {\lident} : {\term}.} \\
% Is equivalent to {\tt Axiom {\lident} : {\term}}
Links {\term} to the names comprising the list {\lident}
\end{enumerate}
\subsection{{\tt Variable {\ident} : {\term}}.}
\index{Variable@{\tt Variable}}
\index{Variables@{\tt Variables}}
This command links {\term} to the name {\ident} in the context of the
current section. The name {\ident} will be unknown when the current
section will be closed. One says that the variable is {\em
discharged}. Using the {\tt Variable} command out of any section is
equivalent to {\tt Axiom}.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Clash with previous constant {\ident}}
\end{enumerate}
\Variant
\begin{enumerate}
\item {\tt Variables {\lident} : {\term}.}\\ Links {\term} to the
names comprising the list {\lident}
\item {\tt Hypothesis {\lident} : {\term}.} \\ Is equivalent to {\tt
Variables {\lident} : {\term}}
\end{enumerate}
\SeeAlso section \ref{Section}
It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis:
for logical postulates (i.e. when the assertion {\term} is of sort
\verb:Prop:), and to use the keywords \verb:Parameter: and
\verb:Variable: in other cases (corresponding to the declaration of an
abstract mathematical entity).
\section{Definitions}\index{Definitions}\label{Simpl-definitions}
Definitions differ from declarations since they allow to give a name
to a term whereas declarations were just giving a type to a name. That
is to say that the name of a defined object can be replaced at any
time by its definition. This replacement is called
$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see section
\ref{delta}). A defined object is accepted by the system iff the
defining term is well-typed in the current context of the definition.
Then the type of the name is the type of term. The defined name is
called a {\em constant}\index{Constant} and one says that {\it the
constant is added to the environment}\index{Environment}.
A formal presentation of constants and environment is given in
section \ref{Cic-definitions}.
\subsection{\tt Definition {\ident} := {\term}.}
\index{Definition@{\tt Definition}}
This command binds the value {\term} to the name {\ident} in the
environment, providing that {\term} is well-typed.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Clash with previous constant {\ident}}
\end{enumerate}
\Variant
\begin{enumerate}
\item {\tt Definition {\ident} : {\term$_1$} := {\term$_2$}.} It
checks that the type of {\term$_2$} is definitionally equal to
{\term$_1$}, and registers {\ident} as being of type {\term$_1$},
and bound to value {\term$_2$}.
\end{enumerate}
\ErrMsg
\begin{enumerate}
\item {\tt In environment the term: {\term$_2$} does not have type
{\term$_1$}. Ac\-tu\-al\-ly, it has \\ ty\-pe {\term$_3$}}.
\end{enumerate}
\SeeAlso sections \ref{Transparent}, \ref{Unfold}
\subsection{\tt Local {\ident} := {\term}.}\index{Local@{\tt Local}}
This command binds the value {\term} to the name {\ident} in the
environment of the current section. The name {\ident} will be unknown
when the current section will be closed and all occurrences of
{\ident} in persistent objects (such as theorems) defined within the
section will be replaced by \term. One can say that the {\tt Local}
definition is a kind of {\em macro}.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Clash with previous constant {\ident}}
\end{enumerate}
\Variant
\begin{enumerate}
\item {\tt Local {\ident} : {\term$_1$} := {\term$_2$}.}\\ Checks that
the type of {\term$_2$} is definitionally equal to {\term$_1$}, and
registers {\ident} as being of type {\term$_1$}.
\end{enumerate}
\SeeAlso sections \ref{Section}, \ref{Transparent}, \ref{Unfold}
%\subsection{\tt Let {\ident} := {\term}.}
%Not yet documented.
\section{Inductive definitions}\index{Inductive definitions} \label{gal_Inductive_Definitions}
This version of {\Coq} contains a new implementation of inductive
definitions. It is formally presented in section
\ref{Cic-inductive-definitions}.
%We also refer the reader
%to \ref{Addoc-mutual} which contains commented examples
%and some useful comments about the difference between the
%previous version {\Coq} V5.8 and the present one.
\subsection{\tt Inductive {\ident} : {\term} := {\ident$_1$} : {\term$_1$} | .. | {\ident$_n$} : {\term$_n$}.}\index{Inductive@{\tt Inductive}}\label{Inductive}
This command is used to define inductive types and inductive families
such as inductively defined relations. The name {\ident} is the name
of the inductively defined object and {\term} is its type. The names
{\ident$_1$}, .., {\ident$_n$} are the names of its constructors and
{\term$_1$}, .., {\term$_n$} their respective types. The types of the
constructors have to satisfy a {\em positivity condition} (see section
\ref{Positivity}) for {\ident}. This condition ensures the
well-foundedness of the inductive definition. If this is the case,
the constants {\ident}, {\ident$_1$}, .., {\ident$_n$} are added to
the environment with their respective types. According to the arity
of the aimed inductive type ({\it e.g.} the type of {\term}), {\Coq}
provides a number of destructors for {\ident}. Destructors are named
{\ident}{\tt\_ind}, {\ident}{\tt \_rec} or {\ident}{\tt \_rect} which
respectively correspond to elimination principles on {\tt Prop}, {\tt
Set} and {\tt Type}. Note that {\ident}{\tt \_ind} is always
provided whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} are not.
The type of the destructors expresses structural induction/recursion
principles over objects of {\ident}. The inductive definitions are
formally detailed in section \ref{Cic-inductive-definitions}. We give
below two examples of the use of the {\tt Inductive} definitions.
The set of natural numbers is defined as :
\begin{coq_example}
Inductive nat : Set := O : nat | S : nat -> nat.
\end{coq_example}
The type {\tt nat} is defined as the least \verb:Set: containing {\tt
O} and closed by the {\tt S} constructor. The constants {\tt nat},
{\tt O} and {\tt S} are added to the environment.
Now let us have a look at the elimination principles. They are three :
{\tt nat\_ind}, {\tt nat\_rec} and {\tt nat\_rect}. The type of {\tt
nat\_ind} is~:
\begin{coq_example}
Check nat_ind.
\end{coq_example}
This is the well known structural induction principle over natural
numbers, i.e. the second-order form of Peano's induction principle.
It allows to prove some universal property of natural numbers ({\tt
(n:nat)(P n)}) by induction on {\tt n}. Recall that {\tt (n:nat)(P
n)} is {\sf Gallina}'s syntax for the universal quantification
$\forall n:nat\cdot P(n).$\\
The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except
that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)}
respectively . They correspond to primitive induction principles
(allowing dependent types) respectively over sorts \verb:Set: and
\verb:Type:.
As a second example, let us define the $even$ predicate :
\begin{coq_example}
Inductive even : nat->Prop :=
even_0 : (even O)
| even_SS : (n:nat)(even n)->(even (S (S n))).
\end{coq_example}
The type {\tt nat->Prop} means that {\tt even} is a unary predicate
(inductively defined) over natural numbers. The type of its two
constructors are the defining clauses of the predicate {\tt even}. The
type of {\tt even\_ind} is~:
\begin{coq_example}
Check even_ind.
\end{coq_example}
From a mathematical point of vue it asserts that the natural numbers
satisfying the predicate {\tt even} are just the naturals satisfying
the clauses {\tt even\_0} or {\tt even\_SS}. This is why, when we want
to prove any predicate {\tt P} over elements of {\tt even}, it is
enough to prove it for {\tt O} and to prove that if any natural number
{\tt n} satisfies {\tt P} its double successor {\tt (S (S n))}
satisfies also {\tt P}. This is indeed analogous to the structural
induction principle we got for {\tt nat}.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Non positive Occurrence in {\term$_i$}}
\item {\tt Type of Constructor not well-formed}
\end{enumerate}
\Variant
\begin{enumerate}
\item {\tt Inductive {\ident} [ {\params} ] : {\term} :=
{\ident$_1$}:{\term$_1$} | .. | {\ident$_n$}:\term$_n$.}\\ Allows
to define parameterized inductive types (see section~\ref{term} for
the syntax of \params).\\
For instance, one can define
parameterized lists as~:
\begin{coq_example*}
Inductive list [X:Set] : Set :=
Nil : (list X) | Cons : X->(list X)->(list X).
\end{coq_example*}
Note that, in the type of {\tt Nil} and {\tt Cons}, we write {\tt
(list X)} and not just {\tt list}.\\ The constants {\tt Nil} and
{\tt Cons} will have respectively types
\begin{coq_example}
Check Nil.
\end{coq_example}
and
\begin{coq_example}
Check Cons.
\end{coq_example}
Types of destructors will be also quantified with {\tt (X:Set)}.
\item {\tt Inductive {\sort} {\ident} :=
{\ident$_1$}:{\term$_1$} | .. | {\ident$_n$}:\term$_n$.}\\
with {\sort} being one of {\tt Prop, Type, Set, Typeset} is
equivalent to \\ {\tt Inductive {\ident} : {\sort} :=
{\ident$_1$}:{\term$_1$} | .. | {\ident$_n$}:\term$_n$.}
\item {\tt Inductive {\sort} {\ident} [ {\params} ]:=
{\ident$_1$}:{\term$_1$} | .. | {\ident$_n$}:\term$_n$.}\\
Same as before but with parameters.
\end{enumerate}
\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{Elim}
\subsection{\tt Mutual Inductive}\index{Mutual Inductive@{\tt Mutual Inductive}}\label{Mutual-Inductive}
This command is a new feature of {\Coq} V5.10. It allows to define
mutually recursive inductive types. Its syntax is :\\[0.3cm]
{\tt
Mutual Inductive {\ident$_1$} : {\term$_1$} := \\
\mbox{}\hspace{0.4cm} {\ident$_1^1$} : {\term$_1^1$} \\
\mbox{}\hspace{0.1cm}| .. \\
\mbox{}\hspace{0.1cm}| {\ident$_{n_1}^1$} : {\term$_{n_1}^1$} \\
with\\
\mbox{}\hspace{0.1cm} .. \\
with {\ident$_m$} : {\term$_m$} := \\
\mbox{}\hspace{0.4cm}{\ident$_1^m$} : {\term$_1^m$} \\
\mbox{}\hspace{0.1cm}| .. \\
\mbox{}\hspace{0.1cm}| {\ident$_{n_m}^m$} : {\term$_{n_m}^m$}.
}
It has the same semantics as the above {\tt Inductive} definition for
each \ident$_1$, .., \ident$_m$. All names \ident$_1$, .., \ident$_m$
are simultaneously added to the environment. Then well-typing of
constructors can be checked. Each one of the \ident$_1$, ..,
\ident$_m$ can be used on its own.
It is also possible to parameterize these inductive definitions.
However, one should remark that parameters correspond to a local
context in which the whole set of inductive declarations is done. For
this reason, the parameters are shared between all inductive types and
this context syntactically appears between the {\tt Mutual} and the
{\tt Inductive} keywords and not after the identifier as it is the
case for a single inductive declaration. The syntax is thus:\\[0.3cm]
{\tt
Mutual [{\rm\sl params} ] Inductive {{\ident$_1$} : {\term$_1$} := \\
\mbox{}\hspace{0.4cm} {\ident$_1^1$} : {\term$_1^1$} \\
\mbox{}\hspace{0.1cm}| .. \\
\mbox{}\hspace{0.1cm}| {\ident$_{n_1}^1$} : {\term$_{n_1}^1$} \\
with\\
\mbox{}\hspace{0.1cm} .. \\
with {\ident$_m$} : {\term$_m$} := \\
\mbox{}\hspace{0.4cm}{\ident$_1^m$} : {\term$_1^m$} \\
\mbox{}\hspace{0.1cm}| .. \\
\mbox{}\hspace{0.1cm}| {\ident$_{n_m}^m$} : {\term$_{n_m}^m$}.
}}
\\[0.3cm]
\Example
The typical example of a mutual inductive data type is the one for
trees and forests. We assume given two types $A$ and $B$ as variables.
It can be declared the following way.
\begin{coq_example*}
Variables A,B:Set.
Mutual Inductive tree : Set := node : A -> forest -> tree
with forest : Set := leaf : B -> forest
| cons : tree -> forest -> forest.
\end{coq_example*}
This declaration generates automatically six induction principles
called respectively {\tt tree\_rec}, {\tt tree\_ind}, {\tt
tree\_rect}, {\tt forest\_rec}, {\tt forest\_ind}, {\tt
forest\_rect}. These ones are not the most general ones but are
just the induction principles corresponding to each inductive part
seen as a single inductive definition.
To illustrate this point on our example, we give the types of {\tt
tree\_rec} and {\tt forest\_rec}.
\begin{coq_example}
Check tree_rec.
Check forest_rec.
\end{coq_example}
Assume we want to parameterized our mutual inductive definitions with
the two type variables $A$ and $B$, the declaration should be done the
following way:
\begin{coq_eval}
Reset tree.
\end{coq_eval}
\begin{coq_example*}
Mutual [A,B:Set] Inductive
tree : Set := node : A -> (forest A B) -> (tree A B)
with forest : Set := leaf : B -> (forest A B)
| cons : (tree A B) -> (forest A B) -> (forest A B).
\end{coq_example*}
\begin{coq_eval}
Save State toto.
\end{coq_eval}
Assume we define an inductive definition inside a section. When the
section is closed, the variables declared in the section and occuring
free in the declaration are added as parameters to the inductive
definition.
\subsection{The Record Macro}\index{Record@{\tt Record}}
This version of {\Coq} contains a macro called \verb+Record+ allowing
the definition of records as is done in many programming languages.
Its syntax is~: \\[0.3cm]
{\tt Record {\ident} [ {\params} ] : {\sort} := {\ident$_0$} \verb+{+ \\
\mbox{}\hspace{0.4cm} {\ident$_1$} : {\term$_1$}; \\
\mbox{}\hspace{0.4cm} ... \\
\mbox{}\hspace{0.4cm} {\ident$_n$} : {\term$_n$} \verb+}+.}\\[0.3cm]
The identifier {\ident} is the name of the defined record and {\sort}
is its type. The identifier {\ident$_0$} is the name of its
constructor. The identifiers {\ident$_1$}, .., {\ident$_n$} are the
names of its fields and {\term$_1$}, .., {\term$_n$} their respective
types. Note that the records may have parameters.
\\[0.3cm]
\Example
The set of rational numbers is defined by~:
\begin{coq_eval}
Restore State Initial.
\end{coq_eval}
\begin{coq_example}
Record Rat : Set := mkRat {
top : nat;
bottom : nat;
Rat_cond : (gt bottom O) }.
\end{coq_example}
An important difference between our records and those of most
programming languages is that a field may depend on other fields
appearing before it. For instance in the above example, the field
\verb+Rat_cond+ depends on the field \verb+bottom+. Thus the order of
the fields is important.
Let us now see the work done by the {\tt Record} macro.
First the macro generates a one-constructor inductive definition
of the following form~:\\[0.3cm]
\noindent
{\tt Inductive {\ident} [ {\params} ] : {\sort} := \\
\mbox{}\hspace{0.4cm} {\ident$_0$} : ({\ident$_1$}:{\term$_1$}) ..
({\ident$_n$}:{\term$_n$})({\ident} {\rm\sl params}).}\\[0.3cm]
To build an object of type {\ident}, one should provide the
constructor {\ident$_0$} with $n$ terms filling the fields of
the record.
Let us define the rational $1/2$. Following our definition, a rational
number is defined by two natural numbers and a proof that the second
is strictly positive. Thus we must prove that $2$ is strictly
positive. Let us just assume it as axiom. Try to prove it using
tactics (see the chapter \ref{Proof-handling}).
\begin{coq_example*}
Axiom two_is_positive : (gt (S (S O)) O).
\end{coq_example*}
We have now all the ingredients to define $1/2$ (we call it
\verb+half+).
\begin{coq_example}
Definition half := (mkRat (S O) (S (S O)) two_is_positive).
Check half.
\end{coq_example}
The macro generates also, when it is possible, the projection
functions for destructuring an object of type {\ident} into its
constituent fields. We give the field names to these projection
functions.
For our example, these functions are \verb+top+, \verb+bottom+ and
\verb+Rat_cond+. Let us show their behavior on \verb+half+.
\begin{coq_example}
Compute (top half).
Compute (bottom half).
Compute (Rat_cond half).
\end{coq_example}
\begin{coq_eval}
Restore State toto.
\end{coq_eval}
In the case where the definition of a projection function {\ident$_i$}
is impossible, a warning is printed.
\\[0.3cm]
\noindent {\bf Warning :}
\begin{enumerate}
\item {\tt Warning: {\ident$_i$} cannot be defined.}\\
This message is followed by an explanation of this impossibility.\\
There may be three reasons~:
\begin{enumerate}
\item The name {\ident$_i$} already exists in environment (see
section \ref{Axiom}).
\item The body of {\ident$_i$} uses a incorrect elimination for
{\ident} (see sections \ref{Fixpoint} and \ref{Caseexpr}).
\item {\tt The projections [ {\rm\sl idents} ] were not defined.}\\
The body of {\term$_i$} uses the projections {\rm\sl idents}
which are not defined for one of these three reasons listed here.
\end{enumerate}
\end{enumerate}
\ErrMsg
\begin{enumerate}
\item {\tt A record cannot be recursive}\\
The record name {\ident} appears in the type of its fields.
During the definition of the one-constructor inductive definition,
all the errors of inductive definitions, as described in section
\ref{gal_Inductive_Definitions}, may occur.
\end{enumerate}
\Variant
\begin{enumerate}
\item
\noindent
{\tt Record {\ident} [ {\rm\sl params} ] : {\sort} := \verb+{+ \\
\mbox{}\hspace{0.4cm} {\ident$_1$} : {\term$_1$}; \\
\mbox{}\hspace{0.4cm} ... \\
\mbox{}\hspace{0.4cm} {\ident$_n$} : {\term$_n$} \verb+}+.}\\
One can omit the constructor name in which case the system will use
the name {\tt Build\_{\ident}}.
\end{enumerate}
\subsection{\tt Fixpoint {\ident} [ \ident$_1$ : \term$_1$ ] : \term$_2$ := \term$_3$.}\index{Fixpoint@{\tt Fixpoint}}\label{Fixpoint}
This command is a new feature of {\Coq} V5.10. It may be used to
define inductive objects using a fixed point construction instead of
the {\tt Match} recursion operator. The meaning of this declaration is
to define {\it ident} a recursive function with one argument
\ident$_1$ of type \term$_1$ such that ({\it ident}~\ident$_1$) has
type \term$_2$ and is equivalent to the expression \term$_3$. The
type of the {\ident} is consequentely {(\ident$_1$ :
\term$_1$)\term$_2$} and the value is equivalent to [\ident$_1$ :
\term$_1$]\term$_3$. The argument {\ident$_1$} (of type {\term$_1$})
is called the {\em recursive variable} of {\ident}. Its type should
be an inductive definition.
To be accepted, a {\tt Fixpoint} definition has to satisfy some
syntactical constraints on this recursive variable. They are needed to
ensure that the {\tt Fixpoint} definition always terminates. For
instance, one can define the addition function as :
\begin{coq_example}
Fixpoint add [n:nat] : nat->nat
:= [m:nat]<nat>Case n of m [p:nat](S (add p m)) end.
\end{coq_example}
The {\tt Case} operator matches a value (here \verb:n:) with the
various constructors of its (inductive) type. The remaining arguments
give the respective values to be returned, as functions of the
parameters of the corresponding constructor. Thus here when \verb:n:
equals \verb:O: we return \verb:m:, and when \verb:n: equals \verb:(S
p): we return \verb:(S (add p m)):. The {\tt Case} operator is described
in detail in section \ref{Caseexpr}. The system recognizes that in
the inductive call {\tt (add p m)} the first argument actually
decreases because it is a {\em pattern variable} coming from {\tt Case
n of}.
\\[0.3cm]
\Variant
\begin{itemize}
\item {\tt Fixpoint {\ident} [ {\params} ] : \term$_1$ :=
\term$_2$.}\\
See section \ref{term} for a syntactic descrrption of
\params. It declares a list of identifiers with their type
usable in the type \term$_1$ and the definition body \term$_2$
and the last identifier in \ident$_0$ is the recursion variable.
\item {\tt Fixpoint {\ident$_1$} [ {\params$_1$} ] :
{\term$_1$} := {\term$_1'$}\\
with\\
\mbox{}\hspace{0.1cm} .. \\
with {\ident$_m$} [ {\params$_m$} ] : {\term$_m$} :=
{\term$_m'$}}\\
Allows to define simultaneously {\ident$_1$}, ..,
{\ident$_m$}.
\end{itemize}
\Example The following definition is not correct and generates an
error message:
\begin{coq_example}
Fixpoint wrongplus [n:nat] : nat->nat
:= [m:nat]<nat>Case m of n [p:nat](S (wrongplus n p)) end.
\end{coq_example}
because the declared decreasing argument {\tt n} actually does not
decrease in the recursive call. The function computing the addition
over the second argument should rather be written:
\begin{coq_example*}
Fixpoint plus [n,m:nat] : nat
:= <nat>Case m of n [p:nat](S (plus n p)) end.
\end{coq_example*}
The ordinary match operation on natural numbers can be mimicked the
following way.
\begin{coq_example*}
Fixpoint nat_match [C:Set;f0:C;fS:nat->C->C;n:nat] : C
:= <C>Case n of f0 [p:nat](fS p (nat_match C f0 fS p)) end.
\end{coq_example*}
The recursive call may not only be on direct subterms of the recursive
variable {\tt n} but also on a deeper subterm and we can directly
write the function {\tt mod2} which gives the remainder modulo 2 of a
natural number.
\begin{coq_example*}
Fixpoint mod2 [n:nat] : nat
:= <nat>Case n of O [p:nat]<nat>Case p of (S O) [q:nat](mod2 q) end end.
\end{coq_example*}
In order to keep the strong normalisation property, the fixed point
reduction will only be performed when the argument in position of the
recursive variable (whose type should be in an inductive definition)
starts with a constructor.
The {\tt Fixpoint} construction enjoys also the {\tt with} extension
to define functions over mutually defined inductive types or more
generally any mutually recursive definitions.
\\[0.3cm]
\Example
The size of trees and forests can be defined the following
way:
\begin{coq_eval}
Restore State Initial.
Variables A,B:Set.
Mutual Inductive tree : Set := node : A -> forest -> tree
with forest : Set := leaf : B -> forest
| cons : tree -> forest -> forest.
\end{coq_eval}
\begin{coq_example*}
Fixpoint tree_size [t:tree] : nat :=
<nat>Case t of [a:A][f:forest](S (forest_size f)) end
with forest_size [f:forest] : nat :=
<nat>Case f of [b:B](S O)
[t:tree][f':forest](plus (tree_size t) (forest_size f'))
end.
\end{coq_example*}
A generic command {\tt Scheme} is able to build automatically various
mutual induction principles. It is described in section \ref{Scheme}.
\subsection{\tt Recursive Definition ...}\index{Recursive Definition@{\tt Recursive Definition}}\label{Recursive-Definition}
This command is a new feature of {\Coq} V5.10. It is a high level tool
for defining recursive functions. Its syntax follows the schema :
\noindent
{\tt Recursive Definition {\ident} : {\form} :=\\
\mbox{}\hspace{0.2cm}
{\pattern$_1^1$} .. {\pattern$_n^1$} \verb.=>. {\term$_1$}\\
\verb.|. .. \\
\verb.|. {\pattern$_1^m$} .. {\pattern$_n^m$} \verb.=>.
{\term$_m$}.}
\noindent
It can be compared to functions declarations in ML languages (see, for
instance \cite{Caml}).\\ The {\tt Recursive Definition} command uses a
heuristic which tries to derive a term satisfying the specification.
That is to say that {\Coq} tries to find a term {\tt T} such that for
each $i\in [1..m]$,\\
\centerline{{\tt (T {\pattern$_1^i$} \ldots
{\pattern$_n^i$})}$=_{\beta\iota\delta}${\term$_i$}.}\\
If such a term can be inferred then {\ident} is defined as being {\tt
T} and all corresponding equational theorems are provided. We refer
the reader to section \ref{Addoc-recdef} for more details.
% Useless it is loaded automatically.
%\Rem Since the {\tt Recursive Definition} command allows to define
%propositional functions, it requires the module
%{\tt Logic\_Type} to be loaded.
\section{Section mechanism}\index{Sections}\label{Section}
The sectioning mechanism allows to organize a proof in structured
sections. Then local declarations become available (see section
\ref{Simpl-definitions}).
\subsection{\tt Section {\ident}}\index{Section@{\tt Section}}
This command is used to open a section named {\ident}.
\\[0.3cm]
\Variant
\begin{enumerate}\index{Chapter@{\tt Chapter}}
\item{\tt Chapter {\ident}}\\
Same as {\tt Section {\ident}}
\end{enumerate}
\subsection{\tt End {\ident}}
This command closes the section named {\ident}. When a section is
closed, all local declarations are discharged. This means that all
global objects defined in the section are {\it closed} (in the sense
of $\lambda$-calculus) with as many abstractions as there were local
declarations in the section explicitely occuring in the term. A local
object in the section is not exported and its value will be
substituted in the other definitions.
Here is an example :
\begin{coq_example}
Section s1.
Variables x,y : nat.
Local y' := y.
Definition x' := (S x).
Print x'.
End s1.
Print x'.
\end{coq_example}
Note the difference between the value of {\tt x'} inside section {\tt
s1} and outside.
\\[0.3cm]
\ErrMsg
\begin{enumerate}
\item {\tt Section {\ident} does not exist (or is already closed)}
\item {\tt Section {\ident} is not the innermost section}
\end{enumerate}
\Rem Some commands such as {\tt Hint \ident} or {\tt Syntactic
Definition} which appear inside a section are cancelled when the
section is closed.
% Local Variables:
% mode: LaTeX
% TeX-master: "Reference-Manual"
% End:
Raw
RefMan-int.tex
\chapter{Introduction}
This document is the Reference Manual of version V5.10 of the \Coq\
proof assistant. A companion volume, the \Coq\ Tutorial, is provided
for the beginners. It is advised to read the Tutorial first.
Additional documentation is described in chapter \ref{Addoc}.
All services of the \Coq\ proof assistant are accessible by
interpretation of a command language. A command is a string ended
with a period.
\Coq\ has an interactive mode in which commands are interpreted as the
user types them in from the keyboard and a compiled mode where
commands are processed from a file. Other modes of interaction with
\Coq\ are possible, through an emacs shell window, or through a
customized interface with the Centaur environment (CTCoq). These
facilities are not documented here.
\begin{itemize}
\item The interactive mode may be used as a debugging mode in which
the user can develop his theories and proofs step by step,
backtracking if needed and so on. The interactive mode is run with
the {\tt coqtop} command from the operating system (which we shall
assume to be some variety of UNIX in the rest of this document).
\item The compiled mode acts as a proof checker taking a file
containing a whole development in order to ensure its correctness.
Moreover, \Coq's compiler provides an output file containing a
compact representation of its input. The compiled mode is run with
the {\tt coqc} command from the operating system. Its use is
documented in chapter \ref{Addoc-coqc}.
\end{itemize}
\Coq\ offers two kinds of services : logical services and operating
services.
We divide the logical services in two main parts :
\begin{itemize}
\item a specification language in which the user axiomatizes his own
theories. This specification language is known as {\sf Gallina}
which mainly provides declaration and definition mechanisms. It is
documented in chapter \ref{Gallina}.
\item a proof editing mode providing tools for proof development.
Proofs services are again of two kinds :
\begin{itemize}
\item proofs pragmas such as switching on and off the proof editor,
restarting a proof, etc ... They are documented in chapter
\ref{Proof-handling}.
\item tactics which are the implementation of logical reasoning steps.
The whole chapter \ref{Tactics} is devoted to their documentation.
\end{itemize}
\end{itemize}
For a more fundamental understanding of the logical framework, we urge
the user of \Coq\ to read chapter \ref{Cic}.
The so-called operating services are :
\begin{itemize}
\item a file system service including modules facilities
\item displaying features
\item user's syntax handling
\item miscellaneous pragmas
\end{itemize}
They are documented in chapter \ref{Other-commands}.
\paragraph{Notations} In the rest of this document, \Coq's grammar
terminals will be written in {\tt typewriter} font. Non-terminals are
\begin{enumerate}
\item {\Fwterm}\index{Fomega term@$F_\omega$ term} which denotes an
$F_\omega$ term (see section \ref{Extraction}).
\item {\ident} \index{ident@{\rm\sl ident}} which denotes an {\it
identifier} in the usual sense. Characters such as {\tt \_} and
{\tt '} are allowed to appear in identifiers, besides
alpha-numerical characters.
\item {\num}\index{num@{\rm\sl num}} which denotes a positive natural
number ({\it e.g.} a sequence of digits with no blanks).
\item {\pattern}\index{pattern@{\rm\sl pattern}} which denotes any {\sc
Cic}-term belonging to a restricted class (see section
\ref{Recursive-Definition}).
\item {\vref}\index{ref@{\rm\sl ref}} which is either an {\ident} or a
\num.
\item {\str}\index{string@{\rm\sl string}} which denotes any sequence
of characters enclosed between two \verb!"!.
\item {\tac} which denotes any simple tactic's name or composed
tactical (see section \ref{Tacticals}).
\item {\term}\index{term@{\rm\sl term}} which denotes any {\sc
Cic}-term (see section \ref{term}).
\item {\sort}\index{sort@{\rm\sl sort}} which denotes one of the
special {\sc Cic}-constants called a sort (see section \ref{Sorts}).
\end{enumerate}
Raw
RefMan-prg.tex
%\documentstyle[11pt]{article}
%\input{title}
\newcommand{\real}{{\sf Real}}
\newcommand{\Ra}{\Rightarrow}
%\newcommand{\Prop}{{\it Prop}}
%\newcommand{\Type}{{\it Type}}
\newcommand{\Spec}{{\it Spec}}
\newcommand{\Data}{{\it Data}}
\newcommand{\FW}{\mbox{$F_{\omega}$}}
\def\ra{\rightarrow}
\def\la{\leftarrow}
\def\fa{\forall}
\def\ex{\exists}
%\begin{document}
%\coverpage{The Program Tactic}{Catherine PARENT}
\chapter{The Program Tactic}\label{Addoc-program}
The facilities described in this chapter pertain to a special aspect of
the \Coq\ system: how to associate to a functional program, whose
specification is written in Gallina, a proof of its correctness.
This methodology is based on the Curry-Howard isomorphism between
functional programs and constructive proofs. This isomorphism allows
the synthesis of a functional program from the constructive part of its
proof of correctness. That is, it is possible to analyze a \Coq\ proof,
to erase all its non-informative parts (roughly speaking, removing the
parts pertaining to sort \Prop, considered as comments, to keep only the
parts pertaining to sort \Set).
This {\sl realizability interpretation}
was defined by Christine Paulin-Mohring in her PhD dissertation, and
implemented as a {\sl program extraction} facility in previous versions of
\Coq~ by Benjamin Werner. However, the corresponding certified program
development methodology was very awkward: the user had to understand very
precisely the extraction mechanism in order to guide the proof construction
towards the desired algorithm. The facilities described in this chapter
attempt to do the reverse: i.e. to try and generate the proof of correctness
from the program itself, given as argument to a specialized tactic.
This work is based on the PhD dissertation of
Catherine Parent \cite{CPar95}.
\section{Developing certified programs: Motivations}
\label{program_proving}
We want to develop certified programs automatically proved by the
system. That is to say, instead of giving a specification, an
interactive proof and then extracting a program, the user gives the
program he wants to prove and the corresponding specification. Using
this information, an automatic proof is developed which solves the
``informative'' goals without the help of the user. When the proof is
finished, the extracted program is guaranteed to be correct and
corresponds to the one given by the user. The tactic uses the fact
that the extracted program is a skeleton of its corresponding proof.
\section{Syntax for tactics}
The user has to give two things~: the specification (given as usual by
a goal) and the program (see section \ref{syntax}). Then, this program
is associated to the current goal (to know which specification it
corresponds to) and the user can use different tactics to develop an
automatic proof.
\subsection{Realizer}
First, the program is associated to the current goal by using the
\verb=Realizer= \index{Realizer@{\tt Realizer}} command. With this
command, the program has to be given with the syntax indicated in
section \ref{syntax} and it is associated to the current goal.
\subsection{Show Program}
The command \verb=Show Program= shows the program associated to the
current goal. \verb=Show Program n= shows the program associated to
the nth subgoal.
\subsection{Program}
Then, an automatic process may be started. A program is associated to
a goal by the user (for the initial goal) and by the tactic
\verb!Program! itself (for the subgoals). If no program is associated
to the current goal, the \verb=Program= tactic fails. This tactic
generates a sequence of \verb=Intro=, \verb=Apply= or \verb=Elim=
tactics depending on the syntax of the program. For instance, if the
program starts with a $\lambda$-abstraction, the \verb=Intro= tactic
is generated several times depending on the goal.
The \verb=Program= tactic generates a list of subgoals which can be
either logical or informative. Subprograms are associated to the
informative subgoals.
\subsection{Program\_all}
The \verb=Program_all= tactic is equivalent to the following tactic~:
\verb=Repeat (Program OrElse Auto)=. It repeats the \verb=Program=
tactic on every informative subgoal and tries the \verb=Auto= tactic
on the logical subgoals. Note that the work of the \verb=Program=
tactic is considered to be finished when all the informative subgoals
have been solved. This implies that logical lemmas can stay at the end
of the automatic proof which have to be solved by the user.
\subsection{Program\_Expand}
The \verb=Program_Expand= tactic transforms the current program into
the same program with the head constant expanded. This tactic
particularly allows the user to force a program to be reduced before
each application of the \verb=Program= tactic.
\section{Syntax for programs}
\label{syntax}
\subsection{Pure programs}
The language to express programs is called \real\footnote{It
corresponds to \FW\ plus inductive definitions}. Programs are
explicitly typed\footnote{This information is not strictly needed but
was useful for type checking in a first experiment.} like terms
extracted from proofs. Some extra expressions have been added to have
a simpler syntax.
This is the raw form of what we call pure programs. But, in fact, it
appeared that this simple type of programs is not sufficient. Indeed,
all the logical part useful for the proof is not contained in these
programs. That is why annotated programs are introduced.
\subsection{Annotated programs}
The notion of annotation introduces in a program a logical assertion
that will be used for the proof. The aim of the \verb=Program= tactic
is to start from a specification and a program and to generate
subgoals either logical or associated with programs. However, to find
the good specification for subprograms is not at all trivial in
general. For instance, if we have to find an invariant for a loop, or
a well founded order in a recursive call.
So, annotations add in a program the logical part which is needed for
the proof and which cannot be automatically retrieved. This allows the
system to do proofs it could not do otherwise.
For this, a particular syntax is needed which is the following~: since
they are specifications, annotations follow the same internal syntax
as \Coq~terms. We indicate they are annotations by putting them
between \verb={= and \verb=}= and preceding them with \verb=:: ::=.
Since annotations are \Coq~terms, they can involve abstractions over
logical propositions that have to be declared. Annotated-$\lambda$
have to be written between \verb=[{= and \verb=}]=.
Annotated-$\lambda$ can be seen like usual $\lambda$-bindings but
concerning just annotations and not \Coq~programs.
\subsection{Recursive Programs}
Programs can be recursively defined using the syntax~: \verb=<={\it
type-of-the-result}\verb=> rec= \index{rec@{\tt rec}} {\it
name-of-the-induction-hypothesis} \verb=:: :: {= {\it
well-founded-order-of-the-recursion} \verb=}= and then the body of
the program (see section \ref{examples}) which must always begin with
an abstraction [x:A] where A is the type of the arguments of the
function (also on which the ordering relation acts).
\subsection{Abbreviations}
Two abbreviations have been defined~:
\verb!<P>let (p:X;q:Y)=Q in S! is syntactic sugar for \verb=<P>Case Q of [p:X][q:Y]S=
and
\verb=<P>if B then Q else R= abbreviates matching on boolean
expressions, that is to say it abbreviates \verb=<P>Case B of Q R=.
Moreover, a synthesis of implicit arguments has been added in order to
allow the user to write a minimum of types in a program. Then, it is
possible not to write a type inside a program term. This type has then
to be automatically synthesized. For this, it is necessary to indicate
where the implicit type to be synthesized appears. The syntax is the
current one of implicit arguments in \Coq~: the question mark
\verb+?+.
This synthesis of implicit arguments is not possible everywhere in a
program. In fact, the synthesis is only available inside a
\verb+Match+, a \verb+Case+ or a \verb+Fix+ construction (where
\verb+Fix+ is a syntax for defining fixpoints).
Then, two macros have been introduced to suppress some question
marks~:
\verb!<P>let (p,q:?)=Q in S! can be abbreviate into \verb!<P>let
(p,q)=Q in S! and \verb+[x,y:?]T+ can be abbreviate into
\verb+[x,y]T+.
\subsection{Grammar}
The grammar for programs is the following (see the section \ref{term}
for more explanation)~:
\begin{tabbing}
pg::= \= ~~ident $|$ ? \\
\> $|$ [x:pg]pg \\
\> $|$ [x]pg \\
\> $|$ (x:pg)pg \\
\> $|$ pg\verb=->=pg \\
\> $|$ (pg pg \ldots pg) \\
\> $|$ \verb=<=pg\verb=>=Match pg with pg-list end \\
\> $|$ \verb=<=pg\verb=>=Case pg of pg-list end \\
\> $|$ Fix ident \{ident/num : pg := pg with \ldots with
ident/num : pg := pg\} \\
\> $|$ pg :: :: \{ coqterm \} \\
\> $|$ [\{x:coqterm\}]pg \\
\> $|$ \verb=<=pg\verb=>=let (x$_1^1$,\ldots,x$_1^{k_1}$:A$_1$;\ldots ;x$_n^1$,\ldots,x$_n^{k_n}$:A$_n$) = pg in pg \\
\> $|$ \verb=<=pg\verb=>=let (x$_1^1$,\ldots,x$_1^{k_1}$,\ldots,x$_n^1$,\ldots,x$_n^{k_n}$) = pg in pg \\
\> $|$ \verb=<=pg\verb=>=if pg then pg else pg \\
\> $|$ \verb=<=pg\verb=>=rec ident :: :: \{ coqterm \} [x:pg]pg
\end{tabbing}
The reference to an identifier of the \Coq\ context (in particular a
constant) inside a program of the
language \real\ is a reference to its extracted contents.
\section{Examples}
\label{examples}
\subsection{Ackermann Function}
Let us give the specification of Ackermann's function. We want to
prove that for every $n$ and $m$, there exists a $p$ such that
$ack(n,m)=p$ with~:
\begin{eqnarray*}
ack(0,n) & = & n+1 \\
ack(n+1,0) & = & ack(n,1) \\
ack(n+1,m+1) & = & ack(n,ack(n+1,m))
\end{eqnarray*}
An ML program following this specification can be~:
\begin{verbatim}
let rec ack = function
0 -> (function m -> Sm)
| Sn -> (function 0 -> ack n 1
| Sm -> ack n (ack Sn m))
\end{verbatim}
Suppose we give the following definition in \Coq~of a ternary relation
\verb=(Ack n m p)= in a Prolog like form representing $p=ack(n,m)$~:
\begin{coq_example*}
Inductive Ack : nat->nat->nat->Prop :=
AckO : (n:nat)(Ack O n (S n))
| AcknO : (n,p:nat)(Ack n (S O) p)->(Ack (S n) O p)
| AckSS : (n,m,p,q:nat)(Ack (S n) m q)->(Ack n q p)
->(Ack (S n) (S m) p).
\end{coq_example*}
Then the goal is to prove that $\forall n,m .\exists p.(Ack~n~m~p)$, so
the specification is~:
\verb!(n,m:nat){p:nat|(Ack n m p)}!.
The associated {\real} program corresponding to the above ML program can be defined as a fixpoint~:
\begin{coq_example*}
Fixpoint ack_func [n:nat] : nat -> nat :=
<nat->nat>Case n of
(* 0 *) [m:nat](S m)
(* (S n) *) [n':nat]
Fix ack_func2 {ack_func2/1 : nat -> nat :=
[m:nat]<nat>Case m of
(* 0 *) (ack_func n' (S O))
(* S m *) [m':nat](ack_func n' (ack_func2 m'))
end}
end.
\end{coq_example*}
The program is associated by using \verb=Realizer ack_func=. The
program is automatically expanded. Each realizer which is a constant
is automatically expanded. Then, by repeating the \verb=Program=
tactic, three logical lemmas are generated and are easily solved by
using the property Ack0, Ackn0 and AckSS.
\begin{coq_eval}
Goal (n,m:nat){p:nat|(Ack n m p)}.
Realizer ack_func.
\end{coq_eval}
\begin{coq_example}
Repeat Program.
\end{coq_example}
\subsection{Euclidean Division}
This example shows the use of {\bf recursive programs}. Let us
give the specification of the euclidean division algorithm. We want to
prove that for $a$ and $b$ ($b>0$), there exist $q$ and $r$ such that
$a=b*q+r$ and $b>r$.
An ML program following this specification can be~:
\begin{verbatim}
let div b a = divrec a where rec divrec = function
if (b<=a) then let (q,r) = divrec (a-b) in (Sq,r)
else (0,a)
\end{verbatim}
Suppose we give the following definition in \Coq~which describes what
has to be proved, ie, $\exists q \exists r.~(a=b*q+r \wedge ~b>r)$~:
\begin{coq_eval}
Abort.
Require Compare_dec.
Require Minus.
Require Wf_nat.
Require Plus.
Require Le.
Require Gt.
\end{coq_eval}
\begin{coq_example*}
Inductive diveucl [a,b:nat] : Set
:= divex : (q,r:nat)(a=(plus (mult q b) r))->(gt b r)
->(diveucl a b).
\end{coq_example*}
The decidability of the ordering relation has to be proved first, by
giving the associated function of type \verb!nat->nat->bool!~:
\begin{coq_example*}
Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
Realizer [n:nat]<nat->bool> Match n with
(* O *) [m]true
(* S *) [n',H,m]<bool> Case m of
(* O *) false
(* S *) [m'](H m')
end
end.
Program_all.
Save.
\end{coq_example*}
Then the specification is \verb!(b:nat)(gt b O)->(a:nat)(diveucl a b)!.
The associated program corresponding to the ML program will be~:
\begin{coq_eval}
Definition lt := [n,m:nat](gt m n).
Theorem eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
\end{coq_eval}
\begin{coq_example*}
Realizer
[b:nat](<nat*nat>rec div :: :: { lt }
[a:nat]<nat*nat>if (le_gt_dec b a)
then <nat*nat>let (q,r) = (div (minus a b))
in ((S q),r)
else (O,a)).
\end{coq_example*}
Where \verb=lt= is the well-founded ordering relation defined by~:
\begin{verbatim}
Coq < Definition lt := [n,m:nat](gt m n).
\end{verbatim}
Note the syntax for recursive programs as explained before. The
\verb=rec= construction needs 4 arguments~: the type result of the
function (\verb=nat*nat= because it returns two natural numbers)
between \verb=<= and \verb=>=, the name of the induction hypothesis
(which can be used for recursive calls), the ordering relation
\verb=lt= (as an annotation because it is a specification), and the
program itself which must begin with a $\lambda$-abstraction. The
specification of \verb=le_gt_dec= is known because it is a previous
lemma.
The term \verb!(le_gt_dec b a)! is seen by the \verb!Program! tactic
as a term of type \verb!bool! which satisfies the specification
\verb!{(le a b)}+{(gt a b)}!.
The tactics \verb=Program_all= or \verb=Program= can be used, and the
following logical lemmas are obtained~:
\begin{coq_example}
Repeat Program.
\end{coq_example}
The subgoals 4, 5 and 6 are resolved by \verb=Auto= (if you use
\verb=Program_all= they don't appear, because \verb=Program_all= tries
to apply \verb=Auto=). The other ones have to be solved by the user.
\subsection{Insertion sort}
This example shows the use of {\bf annotations}. Let us give the
specification of a sorting algorithm. We want to prove that for a
sorted list of natural numbers $l$ and a natural number $a$, we can
build another sorted list $l'$, containing all the elements of $l$
plus $a$.
An ML program implementing the insertion sort and following this
specification can be~:
\begin{verbatim}
let sort a l = sortrec l where rec sortrec = function
[] -> [a]
| b::l' -> if a<b then a::b::l' else b::(sortrec l')
\end{verbatim}
Suppose we give the following definitions in \Coq~:
First, the decidability of the ordering relation~:
\begin{coq_eval}
Restore State Initial.
Require Le.
Require Gt.
\end{coq_eval}
\begin{coq_example*}
Fixpoint inf_dec [n:nat] : nat -> bool :=
[m:nat]<bool>Case n of
true
[n':nat]<bool>Case m of
false
[m':nat](inf_dec n' m')
end
end.
\end{coq_example*}
The definition of the type \verb=list=~:
\begin{coq_example*}
Inductive list : Set := nil : list | cons : nat -> list -> list.
\end{coq_example*}
We define the property for an element \verb=x= to be {\bf in} a list
\verb=l= as the smallest relation such that~: $\forall a \forall
l~(In~x~l) \Ra (In~x~(a::l))$ and $\forall l~(In~x~(x::l))$.
\begin{coq_example*}
Inductive In [x:nat] : list->Prop
:= Inl : (a:nat)(l:list)(In x l) -> (In x (cons a l))
| Ineq : (l:list)(In x (cons x l)).
\end{coq_example*}
A list \verb=t'= is equivalent to a list \verb=t= with one added
element \verb=y= iff~: $(\forall x~(In~x~t) \Ra (In~x~t'))$ and
$(In~y~t')$ and $\forall x~(In~x~t') \Ra ((In~x~t) \vee y=x)$. The
following definition implements this ternary conjunction.
\begin{coq_example*}
Inductive equiv [y:nat;t,t':list]: Prop :=
equiv_cons :
((x:nat)(In x t)->(In x t'))
-> (In y t')
->((x:nat)(In x t')->((In x t)\/y=x))
-> (equiv y t t').
\end{coq_example*}
Definition of the property of list to be sorted, still defined
inductively~:
\begin{coq_example*}
Inductive sorted : list->Prop
:= sorted_nil : (sorted nil)
| sorted_trans : (a:nat)(sorted (cons a nil))
| sorted_cons : (a,b:nat)(l:list)(sorted (cons b l)) -> (le a b)
-> (sorted (cons a (cons b l))).
\end{coq_example*}
Then the specification is:\\
\verb!(a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}!.
The associated \real\ program corresponding to the ML program will be~:
\begin{coq_eval}
Lemma toto : (a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}.
\end{coq_eval}
\begin{coq_example*}
Realizer
[a:nat][l:list]
<list>Match l with
(cons a nil)
[b,m,H]<list>if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} }
then (cons b H)
else (cons a (cons b m))
end.
\end{coq_example*}
Note that we have defined \verb=inf_dec= as the program realizing the
decidability of the ordering relation on natural numbers. But, it has
no specification, so an annotation is needed to give this
specification. This specification is used and then the decidability of
the ordering relation on natural numbers has to be proved using the
index program.
Suppose \verb=Program_all= is used, a few logical
lemmas are obtained (which have to be solved by the user)~:
\begin{coq_example}
Program_all.
\end{coq_example}
\subsection{Quicksort}
This example shows the use of {\bf programs using previous
programs}. Let us give the specification of Quicksort. We want to
prove that for a list of natural numbers $l$, we can build a sorted
list $l'$, which is a permutation of the previous one.
An ML program following this specification can be~:
\begin{verbatim}
let rec quicksort l = function
[] -> []
| a::m -> let (l1,l2) = splitting a m in
let m1 = quicksort l1 and
let m2 = quicksort l2 in m1@[a]@m2
\end{verbatim}
Where \verb=splitting= is defined by~:
\begin{verbatim}
let rec splitting a l = function
[] -> ([],[])
| b::m -> let (l1,l2) = splitting a m in
if a<b then (l1,b::l2)
else (b::l1,l2)
\end{verbatim}
Suppose we give the following definitions in \Coq~:
Declaration of the ordering relation~:
\begin{coq_eval}
Restore State Initial.
Require List.
Require Gt.
\end{coq_eval}
\begin{coq_example*}
Variable inf : A -> A -> Prop.
Definition sup := [x,y:A]~(inf x y).
Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}.
\end{coq_example*}
Definition of the concatenation of two lists~:
\begin{coq_eval}
Save State toto.
\end{coq_eval}
\begin{coq_example*}
Fixpoint app [l:list] : list -> list
:= [m:list]<list>Case l of
(* nil *) m
(* cons a l1 *) [a:A][l1:list](cons a (app l1 m)) end.
\end{coq_example*}
\begin{coq_eval}
Restore State toto.
\end{coq_eval}
Definition of the permutation of two lists~:
\begin{coq_eval}
Definition mil := [a:A][l,m:list](app l (cons a m)) : A->list->list->list.
Lemma mil_app : (a:A)(l,m,n:list)(mil a l (app m n))=(app (mil a l m) n).
Intros.
Unfold mil.
Elim (ass_app l (cons a m) n).
Auto.
Save.
\end{coq_eval}
\begin{coq_example*}
Inductive permut : list->list->Prop :=
permut_nil : (permut nil nil)
|permut_tran : (l,m,n:list)(permut l m)->(permut m n)->(permut l n)
|permut_cmil : (a:A)(l,m,n:list)
(permut l (app m n))->(permut (cons a l) (mil a m n))
|permut_milc : (a:A)(l,m,n:list)
(permut (app m n) l)->(permut (mil a m n) (cons a l)).
\end{coq_example*}
\begin{coq_eval}
Hint permut_nil permut_cmil permut_milc.
Lemma permut_cons : (a:A)(l,m:list)(permut l m)->(permut (cons a l) (cons a m)).
Intros.
Change (permut (cons a l) (mil a nil m)).
Auto.
Save.
Hint permut_cons.
Lemma permut_refl : (l:list)(permut l l).
Induction l ; Auto.
Save.
Hint permut_refl.
Lemma permut_sym : (l,m:list)(permut l m)->(permut m l).
Intros l m h1 ; Elim h1 ; Auto.
Intros l0 m0 n h2 h3 h4 h5.
Apply permut_tran with m0 ; Auto.
Save.
Immediate permut_sym.
Lemma permut_app1 : (m1,n1,l:list)(permut m1 n1)->(permut (app l m1) (app l n1)).
Intros ; Elim l ; Simpl ; Auto.
Save.
Hint permut_app1.
Lemma permut_app_mil : (a:A)(l1,m1,l2,m2,n2:list)
(permut (app l1 m1) (app (app l2 m2) n2))
-> (permut (app (cons a l1) m1) (app (mil a l2 m2) n2)).
Intros ; Simpl.
Elim (mil_app a l2 m2 n2).
Apply permut_cmil.
Elim (app_ass l2 m2 n2) ; Auto.
Save.
Hint permut_app_mil.
Lemma permut_app_app : (m1,m2,n1,n2 :list)
(permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)).
Intros m1 m2 n1 n2 h1 h2.
Elim h1 ; Intros.
Exact h2.
Apply permut_tran with (app m n2) ; Auto.
Apply permut_tran with (app m m2) ; Auto.
Auto.
Apply permut_sym ; Auto.
Save.
Hint permut_app_app.
Lemma permut_app : (m,m1,m2,n1,n2 :list)(permut m1 n1)->(permut m2 n2)->
(permut m (app m1 m2))->(permut m (app n1 n2)).
Intros.
Apply permut_tran with (app m1 m2) ; Auto.
Save.
\end{coq_eval}
The definitions \verb=inf_list= and \verb=sup_list= allow to know if
an element is lower or greater than all the elements of a list~:
\begin{coq_example*}
Section Rlist_.
Variable R : A->Prop.
Inductive Rlist : list -> Prop :=
Rnil : (Rlist nil)
| Rcons : (x:A)(l:list)(R x)->(Rlist l)->(Rlist (cons x l)).
\end{coq_example*}
\begin{coq_eval}
Hint Rnil Rcons.
Lemma Rlist_app : (m,n:list)(Rlist m)->(Rlist n)->(Rlist (app m n)).
Intros m n h1 h2 ; Elim h1 ; Simpl ; Auto.
Save.
Hint Rlist_app.
Section Rlist_cons_.
Variable a : A.
Variable l : list.
Hypothesis Rc : (Rlist (cons a l)).
Lemma Rlist_cons : (R a)/\(Rlist l).
Inversion_clear Rc; Auto.
Save.
End Rlist_cons_.
Section Rlist_append.
Variable n,m : list.
Lemma Rlist_appd : (Rlist (app n m))->((Rlist n)/\(Rlist m)).
Elim n ; Simpl; Auto.
Intros a y h1 h2.
Elim (Rlist_cons a (app y m)) ; Auto.
Intros h3 h4; Elim h1 ; Auto.
Save.
End Rlist_append.
Hint Rlist_appd.
Lemma Rpermut : (m,n:list)(permut m n)->(Rlist m)->(Rlist n).
Intros m n h1 ; Elim h1 ; Unfold mil ; Auto.
Intros a l m0 n0 h2 h3 h4.
Elim (Rlist_cons a l); Auto.
Intros h5 h6; Elim (Rlist_appd m0 n0); Auto.
Intros a l m0 n0 h2 h3 h4.
Elim (Rlist_appd m0 (cons a n0)) ; Auto.
Intros h5 h6; Elim (Rlist_cons a n0) ; Auto.
Save.
\end{coq_eval}
\begin{coq_example*}
End Rlist_.
Hint Rnil Rcons.
\end{coq_example*}
\begin{coq_eval}
Hint Rlist_app.
\end{coq_eval}
\begin{coq_example*}
Section Inf_Sup.
Hypothesis x : A.
Hypothesis l : list.
Definition inf_list := (Rlist (inf x) l).
Definition sup_list := (Rlist (sup x) l).
End Inf_Sup.
\end{coq_example*}
\begin{coq_eval}
Hint Unfold inf_list sup_list.
\end{coq_eval}
Definition of the property of a list to be sorted~:
\begin{coq_example*}
Inductive sort : list->Prop :=
sort_nil : (sort nil)
| sort_mil : (a:A)(l,m:list)(sup_list a l)->(inf_list a m)
->(sort l)->(sort m)->(sort (mil a l m)).
\end{coq_example*}
\begin{coq_eval}
Hint sort_nil sort_mil.
Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))).
Intros.
Exact (permut_cmil a0 y l1 l2 H).
Save.
Hint permutapp.
Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)).
Intros.
Apply sort_mil ; Auto.
Unfold sup_list ; Apply Rpermut with l1 ; Auto.
Unfold inf_list ; Apply Rpermut with l2 ; Auto.
Save.
\end{coq_eval}
Then the goal to prove is $\forall l~\exists m~(sort~m) \wedge
(permut~l~m)$ and the specification is
\verb!(l:list){m:list|(sort m)&(permut l m)!.
Let us first prove a preliminary lemma. Let us define \verb=ltl= a
well-founded ordering relation.
\begin{coq_example*}
Definition ltl := [l,m:list](gt (length m) (length l)).
\end{coq_example*}
\begin{coq_eval}
Hint Unfold ltl.
Lemma ltl_cons : (a,a0:A)(l1,y:list)(ltl l1 (cons a y))->(ltl l1 (cons a (cons a0 y))).
Unfold ltl; Simpl; Auto.
Save.
Hint ltl_cons.
Lemma ltl_cons_cons : (a,a0:A)(l2,y:list)(ltl l2 (cons a y))->(ltl (cons a0 l2) (cons a (cons a0 y))).
Unfold ltl; Simpl; Auto.
Save.
Hint ltl_cons_cons.
Require Wf_nat.
\end{coq_eval}
Let us then give a definition of \verb=Splitting_spec= corresponding
to\\
$\exists l_1 \exists l_2.~(sup\_list~a~l_1) \wedge (inf\_list~a~l_2)
\wedge (l \equiv l_1@l_2) \wedge (ltl~l_1~(a::l)) \wedge
(ltl~l2~(a::l))$ and a theorem on this definition.
\begin{coq_example*}
Inductive Splitting_spec [a:A; l:list] : Set :=
Split_intro : (l1,l2:list)(sup_list a l1)->(inf_list a l2)
->(permut l (app l1 l2))
->(ltl l1 (cons a l))->(ltl l2 (cons a l))
->(Splitting_spec a l).
\end{coq_example*}
\begin{coq_example*}
Theorem Splitting : (a:A)(l:list)(Splitting_spec a l).
Realizer [a:A][l:list]
<list*list>Match l with
(* nil *) (nil,nil)
(* cons *) [b,m,ll]<list*list>let (l1,l2) = ll in
<list*list>if (inf_sup a b)
then (* inf a b *) (l1,(cons b l2))
else (* sup a b *) ((cons b l1),l2)
end.
Program_all.
Simpl; Auto.
Save.
\end{coq_example*}
The associated {\real} program to the specification we wanted to first
prove and corresponding to the ML program will be~:
\begin{coq_example*}
Lemma Quicksort: (l:list){m:list|(sort m)&(permut l m)}.
Realizer <list>rec quick :: :: { ltl }
[l:list]<list>Case l of
(* nil *) nil
(* cons *) [a,m]<list>let (l1,l2) = (Splitting a m) in
(mil a (quick l1) (quick l2))
end.
\end{coq_example*}
Then \verb=Program_all= gives the following logical lemmas (they have
to be resolved by the user)~:
\begin{coq_example}
Program_all.
\end{coq_example}
%\end{document}
Raw
RefMan-uti.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% chapter ``Utilities'' (JCF, 21.6.95) %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\def\Coq{{\sf Coq}}
\def\camllight{{\rm Caml Light}}
\def\emacs{{\rm GNU Emacs}}
\chapter{Utilities}\label{Utilities}
The distribution provides utilities to simplify some tedious works
beside proof development, tactics writing or documentation.
\section{Modules dependencies}\label{Dependencies}\index{Dependencies}
\index{Coqdep@{\tt coqdep}}
In order to compute modules dependencies (so to use {\tt make}),
\Coq\ comes with an appropriate tool, {\tt coqdep}.
{\tt coqdep} computes inter-module dependencies for \Coq\ and
\camllight\ programs, and prints the dependencies on the standard
output in a format readable by make. When a directory is given as
argument, it is recursively looked at.
Dependencies of \Coq\ modules are computed by looking at {\tt Require}
commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import},
{\tt Require Implementation}), and {\tt Declare ML Module} commands.
Dependencies of \camllight\ modules are computed by looking at
\verb!#open! directives and the double underscore notation {\em
module\_\_value}.
See the man page of {\tt coqdep} for more details and options.
\section{{\tt Makefile}}\label{Makefile}\index{Makefile@{\tt Makefile}}
When a proof development becomes large and is split into several files,
it becomes crucial to use a tool like {\tt make} to compile \Coq\
modules.
The writing of a generic and complete {\tt Makefile} may seem tedious
and that's why \Coq\ provides a tool to automate its creation,
{\tt do\_Makefile}. Given the path to \verb!$COQTOP! (the main directory %$
of \Coq) and the files to compile, {\tt do\_Makefile} prints a
{\tt Makefile} on the standard output. So one has just to run the
command~:
$$\mbox{\verb!do\_Makefile! {\em Coq-path file$_1$ \dots\
file$_n$} \verb!> Makefile!}$$ %$$
The resulted {\tt Makefile} has a target {\tt depend} which computes the
dependencies and adds them to the end of the {\tt Makefile}. So each time
you want to update the modules dependencies, type in~:
$$\mbox{\verb!make depend!}$$
There is also a target {\tt all} to compile all the files {\em file$_1$
\dots\ file$_n$}, and a generic target to produce a {\tt .vo} file from
the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo}
to compile the file {\em file}{\tt.v}).
%See the man page of {\tt do\_Makefile} for more details.
\section{\Coq\ and \LaTeX}\label{Latex}\index{Coqtex@{\tt coq-tex}}
\index{Latex@{\LaTeX}}
When writing a documentation about a proof development, we provide a
mechanical way to process \Coq\ phrases embedded in \LaTeX\ files~: the
{\tt coq-tex} filter. This filter extracts Coq phrases embedded in
LaTeX files, evaluates them, and insert the outcome of the evaluation
after each phrase.
Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases,
the {\tt coq-tex} filter produces a file {\em file}{\tt.v.tex} with
the \Coq\ outcome. This \LaTeX\ file must be compiled using the {\tt coq}
or {\tt coq-sl} document style option (provided together with {\tt coq-tex}).
See the man page of {\tt coq-tex} for more details and options. \\[0.3cm]
\noindent{\bf Remark.} This Reference Manual and the Tutorial have been
completely produced with {\tt coq-tex}.
\section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}
\Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides
syntax highlighting (assuming your \emacs\ library provides
{\tt hilit19.el}) and also a rudimentary indentation facility.
See the file {\tt tools/emacs/README} for more details.
\section{Module specification}\label{gallina}\index{Gallina@{\tt gallina}}
Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
specification (inductive types declarations, definitions, type of
lemmas and theorems), removing the proofs parts of the file. The \Coq\
file {\em file}{\tt.v} gives birth to the specification file
{\em file}{\tt.g} (where the suffix {\tt.g} stands for {\sf Gallina}).
See the man page of {\tt gallina} for more details and options.
\section{Man pages}\label{ManPages}\index{Man pages}
There are man pages for {\tt coqtop}, {\tt coq}, {\tt coqc},
{\tt coqdep}, {\tt gallina} and {\tt coq-tex}.
Man pages are optionally installed (see installation instructions in
file {\tt INSTALL}, step 6).
Raw
Tutorial.tex
\input{title}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Prop}{{\it Prop}}
\newcommand{\Type}{{\it Type}}
\newcommand{\Spec}{{\it Spec}}
\newcommand{\Data}{{\it Data}}
\def\ra{\rightarrow}
\def\la{\leftarrow}
\def\fa{\forall}
\def\ex{\exists}
\newcommand{\Coq}{{\sf Coq}}
%\makeindex
\begin{document}
\coverpage{A Tutorial}{G\'erard 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/V5.10:.
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. It assumes that the user
has prepared in his home directory an initialisation file
\verb".coqrc.5.10" containing the following lines:
\begin{coq_example*}
AddPath ".".
AddPath "$COQTH/LISTS".
AddPath "$COQTH/SETS".
AddPath "$COQTH/BOOL".
\end{coq_example*}
so that the standard invocation of \Coq~ delivers a message such as:
\begin{verbatim}
unix: coqtop
> Caml Light version 0.61
Welcome to Coq V5.10 - Thu Nov 10 18:27:12 MET 1994
Coq <
\end{verbatim}
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 executing the command `\verb:Require Basis.:' in the initialisation file
\verb:.coqrc:.
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 \verb:Basis: 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:Hint: 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 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:D](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:D](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:D](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:D](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:D] ~(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:D]~(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:.
{\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.
%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 P):. 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:, which $\beta$-reduces an expression
to its {\sl normal form}:
\begin{coq_example}
Eval ([_: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}
Compute (addition (S (S O)) (S (S (S O)))).
\end{coq_example}
Actually, we do not have to do all this explicitly. \Coq~ provides a special
syntax \verb:Fixpoint/Case: for generic primitive recursion, and we could thus
have defined directly addition as:
\begin{coq_example}
Fixpoint plus [n:nat] : nat -> nat :=
[m:nat]<nat>Case n of
(* O *) m
(* S p *) [p:nat](S (plus p m)) end.
\end{coq_example}
Here the strings \verb:(* ... *): are just comments to help understand the
cases.
Indeed in \Coq~ version V5.10 an easier syntax is available to describe
directly simple recursions, as follows:
\begin{coq_example}
Recursive Definition pluss : nat->nat->nat :=
O m => m
| (S p) m => (S (pluss p m)).
\end{coq_example}
{\bf Warning} This facility was NOT available in earlier versions of \Coq.
The names \verb:pluss_eq1: and \verb:pluss_eq2: are the defining equations of
\verb:pluss:, entered as equalities. For instance:
\begin{coq_example}
Check pluss_eq1.
\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}
Hint 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.
Hint 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]<Prop>Case n of (* O *) False
(* S p *) [p:nat]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:Simple 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; Simple 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.
Hint 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}
{\bf Warning} This important
facility was NOT available in earlier versions of \Coq. More information
on inversion tactics is provided in the document
``Tactics-Inversion''.
\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.vi:
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}
\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}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment