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 --- Makefile.doc | 2 +- doc/refman/Program.tex | 329 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/program.rst | 329 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 330 insertions(+), 331 deletions(-) delete mode 100644 doc/refman/Program.tex create mode 100644 doc/sphinx/addendum/program.rst diff --git a/Makefile.doc b/Makefile.doc index e63728649..8a3d3a307 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Program.v.tex Polynom.v.tex Nsatz.v.tex \ + Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex deleted file mode 100644 index 1e204dc83..000000000 --- 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: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 3feb9014f..a652a121c 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Program.v}% \include{Polynom.v}% = Ring \include{Nsatz.v}% \include{Setoid.v}% Tactique pour les setoides 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: -- cgit v1.2.3