diff options
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 686 |
1 files changed, 369 insertions, 317 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 1e204dc83..eb50e52dc 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,329 +1,381 @@ -\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} +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. this should be just "_program", but refs to it don't work + +.. _programs: + +Program +======== + +:Author: Matthieu Sozeau + +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 :ref:`Extraction <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, 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. + + +.. _elaborating-programs: + +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 match +operation (see :ref:`extendedpatternmatching`). + + ++ Generation of equalities. A match expression is always generalized + by the corresponding equality. As an example, the expression: + + :: + + match x with + | 0 => t + | S n => u + end. + + will be first rewritten to: + + :: + + (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). 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} ++ 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 div2 below, where the second branch is + typed in a context where ∀ p, _ <> S (S p). ++ 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. + + +There are options to control the generation of equalities and +coercions. + +.. opt:: Program Cases + + This controls 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 :ref:`extendedpatternmatching`) when this option is + deactivated. + +.. opt:: Program Generalized Coercion + + This controls 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. + +.. _syntactic_control: + +Syntactic control over equalities +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +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 return or in clause is specified. Likewise, the +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 dec combinator to get the correct hypotheses as in: + +.. coqtop:: none + + Require Import Program Arith. + +.. coqtop:: all + + Program Definition id (n : nat) : { x : nat | x = n } := + if dec (leb n 0) then 0 + else S (pred n). + +The let tupling construct :g:`let (x1, ..., xn) := t in b` does not +produce an equality, contrary to the let pattern construct :g:`let ’(x1, +..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +coerce term to its support type. It can be useful in notations, for +example: + +.. coqtop:: all + + Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). 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. +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} +Definition (see Section `TODO-1.3.2-Definition`_) and Fixpoint (see Section `TODO-1.3.4-Fixpoint`_) +in that they define constants. However, they may require the user to +prove some goals to construct the final definitions. + + +.. _program_definition: + +Program Definition +~~~~~~~~~~~~~~~~~~ + +.. cmd:: Program Definition @ident := @term. + + 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. + + .. exn:: ident already exists + + .. cmdv:: Program Definition @ident : @type := @term + + It interprets the type ``type``, potentially generating proof + obligations to be resolved. Once done with them, we have a |Coq| + type |type_0|. It then elaborates the preterm ``term`` into a |Coq| + term |term_0|, checking that the type of |term_0| is coercible to + |type_0|, and registers ``ident`` as being of type |type_0| once the + set of obligations generated during the interpretation of |term_0| + and the aforementioned coercion derivation are solved. + + .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... + + + .. cmdv:: Program Definition @ident @binders : @type := @term. + + This is equivalent to: + + :g:`Program Definition ident : forall binders, type := fun binders => term`. + + .. TODO refer to production in alias + +See also: Sections `TODO-6.10.1-Opaque`_, `TODO-6.10.2-Transparent`_, `TODO-8.7.5-unfold`_ + +.. _program_fixpoint: + +Program Fixpoint +~~~~~~~~~~~~~~~~ + +.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term. + +The optional order annotation follows the grammar: + +.. productionlist:: orderannot + order : measure `term` (`term`)? | wf `term` `term` + ++ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional (parenthesised) term + ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` + to ``lt``. + ++ :g:`wf R x` which is equivalent to :g:`measure x (R)`. + +The structural fixpoint operator behaves just like the one of |Coq| (see +Section `TODO-1.3.4-Fixpoint`_), except it may also generate obligations. It works +with mutually recursive definitions too. + +.. coqtop:: reset none + + Require Import Program Arith. + +.. coqtop:: all + + 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. + +Here we have one obligation for each branch (branches for :g:`0` and +``(S 0)`` are automatically generated by the pattern-matching +compilation algorithm). + +.. coqtop:: all + + Obligation 1. + +.. coqtop:: reset none + + Require Import Program Arith. + +One can use a well-founded order or a measure as termination orders +using the syntax: + +.. coqtop:: in + + 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. + + + +.. 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 :g:`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 :g:`Qed`). However, as soon as it appears in the context, the + proof of the obligation is *required* to be declared transparent. + + No such problems arise when using measures or well-founded recursion. + +.. _program_lemma: + +Program Lemma +~~~~~~~~~~~~~ + +.. cmd:: Program Lemma @ident : @type. + + 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 :g:`Program + Definition` and use it as the goal afterwards. Otherwise the proof + will be started with the elaborated version as a goal. The + :g:`Program` prefix can similarly be used as a prefix for + :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc... + +.. _solving_obligations: + +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 +obligations (e.g. when defining mutually recursive blocks). The +optional tactic is replaced by the default one if not specified. + +.. cmd:: {? Local|Global} Obligation Tactic := @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 :g:`Next`. :g:`Local` makes the setting last only for the current + module. Inside sections, local is the default. + +.. cmd:: Show Obligation Tactic + + Displays the current default tactic. + +.. cmd:: Obligations {? of @ident} + + Displays all remaining obligations. + +.. cmd:: Obligation num {? of @ident} + + Start the proof of obligation num. + +.. cmd:: Next Obligation {? of @ident} + + Start the proof of the next unsolved obligation. + +.. cmd:: Solve Obligations {? of @ident} {? with @tactic} + + Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one. + +.. cmd:: Solve All Obligations {? with @tactic} + + Tries to solve each obligation of every program using the given + tactic or the default one (useful for mutually recursive definitions). + +.. cmd:: Admit Obligations {? of @ident} + + Admits all obligations (of ``ident``). + + .. note:: Does not work with structurally recursive programs. + +.. cmd:: Preterm {? of @ident} + + Shows the term that will be fed to the kernel once the obligations + are solved. Useful for debugging. + +.. opt:: 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. + +.. opt:: Hide Obligations + + Control whether obligations appearing in the + term should be hidden as implicit arguments of the special + constantProgram.Tactics.obligation. + +.. opt:: Shrink Obligations + + *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. + +The module :g:`Coq.Program.Tactics` defines the default tactic for solving +obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also +adds some useful notations, as documented in the file itself. + +.. _program-faq: + +Frequently Asked Questions +--------------------------- + + +.. exn:: Ill-formed recursive definition + + 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: + + :: + + 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 ``exist`` constructor to + build an object of type ``{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: + + :: + + Program Fixpoint f (x : A | P) { measure (size x) } := + match x with A b => f b end. + + One will then just have to prove that the measure decreases at each + recursive call. There are three drawbacks though: + + #. A measure function has to be defined; + #. The reduction is a little more involved, although it works well + using lazy evaluation; + #. Mutual recursion on the underlying inductive type isn’t possible + anymore, but nested mutual recursion is always possible. + +.. bibliography:: ../biblio.bib + :keyprefix: p- |