diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 295 |
1 files changed, 295 insertions, 0 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex new file mode 100644 index 00000000..b41014ab --- /dev/null +++ b/doc/refman/Program.tex @@ -0,0 +1,295 @@ +\achapter{\Program{}} +\label{Program} +\aauthor{Matthieu Sozeau} +\index{Program} + +\begin{flushleft} + \em The status of \Program\ is experimental. +\end{flushleft} + +We present here the new \Program\ tactic commands, used to build certified +\Coq\ programs, elaborating them from their algorithmic skeleton and a +rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction +(see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular +functional programming language whilst using as rich a specification as +desired and proving that the code meets the specification using the whole \Coq{} proof +apparatus. This is done using a technique originating from the +``Predicate subtyping'' mechanism of \PVS \cite{Rushby98}, which generates type-checking +conditions while typing a term constrained to a particular type. +Here we insert existential variables in the term, which must be filled +with proofs to get a complete \Coq\ term. \Program\ replaces the +\Program\ tactic by Catherine Parent \cite{Parent95b} which had a similar goal but is no longer +maintained. + +The languages available as input are currently restricted to \Coq's term +language, but may be extended to \ocaml{}, \textsc{Haskell} and others +in the future. We use the same syntax as \Coq\ and permit to use implicit +arguments and the existing coercion mechanism. +Input terms and types are typed in an extended system (\Russell) and +interpreted into \Coq\ terms. The interpretation process may produce +some proof obligations which need to be resolved to create the final term. + +\asection{Elaborating programs} +The main difference from \Coq\ is that an object in a type $T : \Set$ +can be considered as an object of type $\{ x : T~|~P\}$ for any +wellformed $P : \Prop$. +If we go from $T$ to the subset of $T$ verifying property $P$, we must +prove that the object under consideration verifies it. \Russell\ will +generate an obligation for every such coercion. In the other direction, +\Russell\ will automatically insert a projection. + +Another distinction is the treatment of pattern-matching. Apart from the +following differences, it is equivalent to the standard {\tt match} +operation (see Section~\ref{Caseexpr}). +\begin{itemize} +\item Generation of equalities. A {\tt match} expression is always + generalized by the corresponding equality. As an example, + the expression: + +\begin{coq_example*} + match x with + | 0 => t + | S n => u + end. +\end{coq_example*} +will be first rewrote to: +\begin{coq_example*} + (match x as y return (x = y -> _) with + | 0 => fun H : x = 0 -> t + | S n => fun H : x = S n -> u + end) (refl_equal n). +\end{coq_example*} + + This permits to get the proper equalities in the context of proof + obligations inside clauses, without which reasoning is very limited. + +\item Generation of inequalities. If a pattern intersects with a + previous one, an inequality is added in the context of the second + branch. See for example the definition of {\tt div2} below, where the second + branch is typed in a context where $\forall p, \_ <> S (S p)$. + +\item Coercion. If the object being matched is coercible to an inductive + type, the corresponding coercion will be automatically inserted. This also + works with the previous mechanism. +\end{itemize} + +To give more control over the generation of equalities, the typechecker will +fall back directly to \Coq's usual typing of dependent pattern-matching +if a {\tt return} or {\tt in} clause is specified. Likewise, +the {\tt if} construct is not treated specially by \Program{} so boolean +tests in the code are not automatically reflected in the obligations. +One can use the {\tt dec} combinator to get the correct hypotheses as in: + +\begin{coq_eval} +Require Import Program Arith. +\end{coq_eval} +\begin{coq_example} +Program Definition id (n : nat) : { x : nat | x = n } := + if dec (leb n 0) then 0 + else S (pred n). +\end{coq_example} + +Finally, the let tupling construct {\tt let (x1, ..., xn) := t in b} +does not produce an equality, contrary to the let pattern construct +{\tt let '(x1, ..., xn) := t in b}. + +The next two commands are similar to their standard counterparts +Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that +they define constants. However, they may require the user to prove some +goals to construct the final definitions. + +\subsection{\tt Program Definition {\ident} := {\term}. + \comindex{Program Definition}\label{ProgramDefinition}} + +This command types the value {\term} in \Russell\ and generate proof +obligations. Once solved using the commands shown below, it binds the final +\Coq\ term to the name {\ident} in the environment. + +\begin{ErrMsgs} +\item \errindex{{\ident} already exists} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt Program Definition {\ident} {\tt :}{\term$_1$} := + {\term$_2$}.}\\ + It interprets the type {\term$_1$}, potentially generating proof + obligations to be resolved. Once done with them, we have a \Coq\ type + {\term$_1'$}. It then checks that the type of the interpretation of + {\term$_2$} is coercible to {\term$_1'$}, and registers {\ident} as + being of type {\term$_1'$} once the set of obligations generated + during the interpretation of {\term$_2$} and the aforementioned + coercion derivation are solved. +\item {\tt Program Definition {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\ + This is equivalent to \\ + {\tt Program Definition\,{\ident}\,{\tt :\,forall} % + {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}} \\ + \qquad {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,% + {\tt .} +\end{Variants} + +\begin{ErrMsgs} +\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type + {\term$_1$}}.\\ + \texttt{Actually, it has type {\term$_3$}}. +\end{ErrMsgs} + +\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold} + +\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type := \term + \comindex{Program Fixpoint} + \label{ProgramFixpoint}} + +The structural fixpoint operator behaves just like the one of Coq +(see Section~\ref{Fixpoint}), except it may also generate obligations. +It works with mutually recursive definitions too. + +\begin{coq_eval} +Admit Obligations. +\end{coq_eval} +\begin{coq_example} +Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. +\end{coq_example} + +Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are +automatically generated by the pattern-matching compilation algorithm). +\begin{coq_example} + Obligation 1. +\end{coq_example} + +One can use a well-founded order or a measure as termination orders using the syntax: +\begin{coq_eval} +Reset Initial. +Require Import Arith. +Require Import Program. +\end{coq_eval} +\begin{coq_example*} +Program Fixpoint div2 (n : nat) {measure n} : + { x : nat | n = 2 * x \/ n = 2 * x + 1 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. +\end{coq_example*} + +The order annotation can be either: +\begin{itemize} +\item {\tt measure f (R)?} where {\tt f} is a value of type {\tt X} + computed on any subset of the arguments and the optional + (parenthesised) term {\tt (R)} is a relation + on {\tt X}. By default {\tt X} defaults to {\tt nat} and {\tt R} to + {\tt lt}. +\item {\tt wf R x} which is equivalent to {\tt measure x (R)}. +\end{itemize} + +\paragraph{Caution} +When defining structurally recursive functions, the +generated obligations should have the prototype of the currently defined functional +in their context. In this case, the obligations should be transparent +(e.g. defined using {\tt Defined}) so that the guardedness condition on +recursive calls can be checked by the +kernel's type-checker. There is an optimization in the generation of +obligations which gets rid of the hypothesis corresponding to the +functionnal when it is not necessary, so that the obligation can be +declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the +context, the proof of the obligation is \emph{required} to be declared transparent. + +No such problems arise when using measures or well-founded recursion. + +\subsection{\tt Program Lemma {\ident} : type. + \comindex{Program Lemma} + \label{ProgramLemma}} + +The \Russell\ language can also be used to type statements of logical +properties. It will generate obligations, try to solve them +automatically and fail if some unsolved obligations remain. +In this case, one can first define the lemma's +statement using {\tt Program Definition} and use it as the goal afterwards. +Otherwise the proof will be started with the elobarted version as a goal. +The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt + Hypothesis}, {\tt Axiom} etc... + +\section{Solving obligations} +The following commands are available to manipulate obligations. The +optional identifier is used when multiple functions have unsolved +obligations (e.g. when defining mutually recursive blocks). The optional +tactic is replaced by the default one if not specified. + +\begin{itemize} +\item {\tt [Local|Global] Obligation Tactic := \tacexpr}\comindex{Obligation Tactic} + Sets the default obligation + solving tactic applied to all obligations automatically, whether to + solve them or when starting to prove one, e.g. using {\tt Next}. + Local makes the setting last only for the current module. Inside + sections, local is the default. +\item {\tt Show Obligation Tactic}\comindex{Show Obligation Tactic} + Displays the current default tactic. +\item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining + obligations. +\item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of + obligation {\tt num}. +\item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next + unsolved obligation. +\item {\tt Solve Obligations [of \ident] [using + \tacexpr]}\comindex{Solve Obligations} + Tries to solve + each obligation of \ident using the given tactic or the default one. +\item {\tt Solve All Obligations [using \tacexpr]} Tries to solve + each obligation of every program using the given tactic or the default + one (useful for mutually recursive definitions). +\item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations} + Admits all obligations (does not work with structurally recursive programs). +\item {\tt Preterm [of \ident]}\comindex{Preterm} + Shows the term that will be fed to + the kernel once the obligations are solved. Useful for debugging. +\item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations} + Control whether all obligations should be declared as transparent (the + default), or if the system should infer which obligations can be declared opaque. +\end{itemize} + +The module {\tt Coq.Program.Tactics} defines the default tactic for solving +obligations called {\tt program\_simpl}. Importing +{\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself. + +\section{Frequently Asked Questions + \label{ProgramFAQ}} + +\begin{itemize} +\item {Ill-formed recursive definitions} + This error can happen when one tries to define a + function by structural recursion on a subset object, which means the Coq + function looks like: + + \verb$Program Fixpoint f (x : A | P) := match x with A b => f b end.$ + + Supposing $b : A$, the argument at the recursive call to f is not a + direct subterm of x as b is wrapped inside an {\tt exist} constructor to build + an object of type \verb${x : A | P}$. Hence the definition is rejected + by the guardedness condition checker. However one can use + wellfounded recursion on subset objects like this: + +\begin{verbatim} +Program Fixpoint f (x : A | P) { measure (size x) } := + match x with A b => f b end. +\end{verbatim} + + One will then just have to prove that the measure decreases at each recursive + call. There are three drawbacks though: + \begin{enumerate} + \item A measure function has to be defined; + \item The reduction is a little more involved, although it works well + using lazy evaluation; + \item Mutual recursion on the underlying inductive type isn't possible + anymore, but nested mutual recursion is always possible. + \end{enumerate} +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% compile-command: "BIBINPUTS=\".\" make QUICK=1 -C ../.. doc/refman/Reference-Manual.pdf" +%%% End: |