\achapter{\Program{}}
\label{Program}
\aauthor{Matthieu Sozeau}
\index{Program}

We present here the \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) (eq_refl 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}

\subsection{Syntactic control over equalities}
\label{ProgramSyntax}
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}

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}.
Also, {\tt {\term}:>} explicitly asks the system to coerce {\tt \term} to its
support type. It can be useful in notations, for example:
\begin{coq_example}
Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
\end{coq_example}

This notation denotes equality on subset types using equality on their
support types, avoiding uses of proof-irrelevance that would come up
when reasoning with equality on the subset types themselves. 

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] [with
    \tacexpr]}\comindex{Solve Obligations}
  Tries to solve
  each obligation of \ident using the given tactic or the default one.
\item {\tt Solve All Obligations [with \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: