From 98fc90ba52d0c2e2837001538117562ce9caefd6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 22 Mar 2018 14:49:42 +0100
Subject: [Sphinx] Move chapter 24 to new infrastructure

---
 doc/refman/Program.tex | 329 -------------------------------------------------
 1 file changed, 329 deletions(-)
 delete mode 100644 doc/refman/Program.tex

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
deleted file mode 100644
index 1e204dc83d..0000000000
--- a/doc/refman/Program.tex
+++ /dev/null
@@ -1,329 +0,0 @@
-\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: 
-- 
cgit v1.2.3

