[Sphinx] Move chapter 24 to new infrastructure

1 files changed, 329 insertions, 0 deletions

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
new file mode 100644
index 000000000..1e204dc83
--- /dev/null
+++ b/doc/sphinx/addendum/program.rst
@@ -0,0 +1,329 @@
+\achapter{\Program{}}
+%HEVEA\cutname{program.html}
+\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 thought 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{verbatim}
+  match x with
+  | 0 => t
+  | S n => u
+  end.
+\end{verbatim}
+will be first rewritten to:
+\begin{verbatim}
+  (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{verbatim}
+
+  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}
+
+There are options to control the generation of equalities
+and coercions.
+
+\begin{itemize}
+\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates
+  the special treatment of pattern-matching generating equalities and
+  inequalities when using \Program\ (it is on by default). All
+  pattern-matchings and let-patterns are handled using the standard
+  algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is
+  deactivated.
+\item {\tt Unset Program Generalized Coercion}\optindex{Program
+    Generalized Coercion} This deactivates the coercion of general
+  inductive types when using \Program\ (the option is on by default).
+  Coercion of subset types and pairs is still active in this case.
+\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 generates 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
+functional 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 elaborated 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}\optindex{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. 
+\item {\tt Set Hide Obligations}\optindex{Hide Obligations}
+  Control whether obligations appearing in the term should be hidden
+  as implicit arguments of the special constant
+  \texttt{Program.Tactics.obligation}.
+\item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
+\emph{Deprecated since 8.7}
+  This option (on by default) controls whether obligations should have their
+  context minimized to the set of variables used in the proof of the
+  obligation, to avoid unnecessary dependencies.
+\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: