summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-cas.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-cas.tex')
-rw-r--r--doc/refman/RefMan-cas.tex692
1 files changed, 692 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cas.tex b/doc/refman/RefMan-cas.tex
new file mode 100644
index 00000000..c79c14e9
--- /dev/null
+++ b/doc/refman/RefMan-cas.tex
@@ -0,0 +1,692 @@
+%\documentstyle[11pt,../tools/coq-tex/coq,fullpage]{article}
+
+%\pagestyle{plain}
+
+%\begin{document}
+%\nocite{Augustsson85,wadler87,HuetLevy79,MaSi94,maranget94,Laville91,saidi94,dowek93,Leroy90,puel-suarez90}
+
+%\input{title}
+%\input{macros}
+%\coverpage{The Macro \verb+Cases+}{Cristina Cornes}
+%\pagestyle{plain}
+\chapter{The Macro {\tt Cases}}\label{Cases}\index{Cases@{\tt Cases}}
+
+\marginparwidth 0pt \oddsidemargin 0pt \evensidemargin 0pt \marginparsep 0pt
+\topmargin 0pt \textwidth 6.5in \textheight 8.5in
+
+
+\verb+Cases+ is an extension to the concrete syntax of Coq that allows
+to write case expressions using patterns in a syntax close to that of ML languages.
+This construction is just a macro that is
+expanded during parsing into a sequence of the primitive construction
+ \verb+Case+.
+The current implementation contains two strategies, one for compiling
+non-dependent case and another one for dependent case.
+\section{Patterns}\label{implementation}
+A pattern is a term that indicates the {\em shape} of a value, i.e. a
+term where the variables can be seen as holes. When a value is
+matched against a pattern (this is called {\em pattern matching})
+the pattern behaves as a filter, and associates a sub-term of the value
+to each hole (i.e. to each variable pattern).
+
+
+The syntax of patterns is presented in figure \ref{grammar}\footnote{
+Notation: \{$P$\}$^*$ denotes zero or more repetitions of $P$ and
+ \{$P$\}$^+$ denotes one or more repetitions of $P$. {\sl command} is the
+non-terminal corresponding to terms in Coq.}.
+Patterns are built up from constructors and variables. Any identifier
+that is not a constructor of an inductive or coinductive type is
+considered to be
+a variable. Identifiers in patterns should be linear except for
+the ``don't care'' pattern denoted by ``\verb+_+''.
+We can use patterns to build more complex patterns.
+We call {\em simple pattern} a variable or a pattern of the form
+$(c~\vec{x})$ where $c$ is a constructor symbol and $\vec{x}$ is a
+linear vector of variables. If a pattern is
+not simple we call it {\em nested}.
+
+
+A variable pattern matches any value, and the
+identifier is bound to that value. The pattern ``\verb+_+'' also matches
+any value, but it is not binding. Alias patterns written \verb+(+{\sl pattern} \verb+as+ {\sl
+identifier}\verb+)+ are also accepted. This pattern matches the same values as
+{\sl pattern} does and
+{\sl identifier} is bound to the matched value.
+A list of patterns is also considered as a pattern and is called {\em
+multiple pattern}.
+
+\begin{figure}[t]
+\begin{center}
+\begin{sl}
+\begin{tabular}{|l|}\hline \\
+\begin{tabular}{rcl}%\hline && \\
+simple\_pattern & := & pattern \verb+as+ identifier \\
+ &$|$ & pattern \verb+,+ pattern \\
+ &$|$ & pattern pattern\_list \\ && \\
+
+pattern & := & identifier $|$ \verb+(+ simple\_pattern \verb+)+ \\ &&\\
+
+
+equation & := & \{pattern\}$^+$ ~\verb+=>+ ~term \\ && \\
+
+ne\_eqn\_list & := & \verb+|+$^{opt}$ equation~ \{\verb+|+ equation\}$^*$ \\ &&\\
+
+eqn\_list & := & \{~equation~ \{\verb+|+ equation\}$^*$~\}$^*$\\ &&\\
+
+
+term & := &
+\verb+Cases+ \{term \}$^+$ \verb+of+ ne\_eqn\_list \verb+end+ \\
+&$|$ & \verb+<+term\verb+>+ \verb+Cases+ \{ term \}$^+$
+\verb+of+ eqn\_list \verb+end+ \\&& %\\ \hline
+\end{tabular} \\ \hline
+\end{tabular}
+\end{sl} \end{center}
+\caption{Macro Cases syntax.}
+\label{grammar}
+\end{figure}
+
+
+Pattern matching improves readability. Compare for example the term
+of the function {\em is\_zero} of natural
+numbers written with patterns and the one written in primitive
+concrete syntax (note that the first bar \verb+|+ is optional)~:
+
+\begin{center}
+\begin{small}
+\begin{tabular}{l}
+\verb+[n:nat] Cases n of | O => true | _ => false end+,\\
+\verb+[n:nat] Case n of true [_:nat]false end+.
+\end{tabular}
+\end{small}
+\end{center}
+
+In Coq pattern matching is compiled into the primitive constructions,
+thus the expressiveness of the theory remains the same. Once the stage
+of parsing has finished patterns disappear. An easy way to see the
+result of the expansion is by printing the term with \texttt{Print} if
+the term is a constant, or
+using the command \texttt{Check} that displays
+the term with its type :
+
+\begin{coq_example}
+Check (fun n:nat => match n with
+ | O => true
+ | _ => false
+ end).
+\end{coq_example}
+
+
+\verb+Cases+ accepts optionally an infix term enclosed between
+brackets \verb+<>+ that we
+call the {\em elimination predicate}.
+This term is the same argument as the one expected by the primitive
+\verb+Case+. Given a pattern matching
+expression, if all the right hand sides of \verb+=>+ ({\em rhs} in
+short) have the same type, then this term
+can be sometimes synthesized, and so we can omit the \verb+<>+.
+Otherwise we have to
+provide the predicate between \verb+<>+ as for the primitive \verb+Case+.
+
+Let us illustrate through examples the different aspects of pattern matching.
+Consider for example the function that computes the maximum of two
+natural numbers. We can write it in primitive syntax by:
+\begin{coq_example}
+Fixpoint max (n m:nat) {struct m} : nat :=
+ match n with
+ | O =>
+ (* O *) m
+ (* S n' *)
+ | S n' =>
+ match m with
+ | O =>
+ (* O *) S n'
+ (* S m' *)
+ | S m' => S (max n' m')
+ end
+ end.
+\end{coq_example}
+
+Using patterns in the definitions gives:
+
+\begin{coq_example}
+Reset max.
+Fixpoint max (n m:nat) {struct m} : nat :=
+ match n with
+ | O => m
+ | S n' => match m with
+ | O => S n'
+ | S m' => S (max n' m')
+ end
+ end.
+\end{coq_example}
+
+Another way to write this definition is to use a multiple pattern to
+ match \verb+n+ and \verb+m+:
+
+\begin{coq_example}
+Reset max.
+Fixpoint max (n m:nat) {struct m} : nat :=
+ match n, m with
+ | O, _ => m
+ | S n', O => S n'
+ | S n', S m' => S (max n' m')
+ end.
+\end{coq_example}
+
+
+The strategy examines patterns
+from left to right. A case expression is generated {\bf only} when there is at least one constructor in the column of patterns.
+For example,
+\begin{coq_example}
+Check (fun x:nat => match x return nat with
+ | y => y
+ end).
+\end{coq_example}
+
+
+
+We can also use ``\verb+as+ patterns'' to associate a name to a
+sub-pattern:
+
+\begin{coq_example}
+Reset max.
+Fixpoint max (n m:nat) {struct n} : nat :=
+ match n, m with
+ | O, _ => m
+ | S n' as N, O => N
+ | S n', S m' => S (max n' m')
+ end.
+\end{coq_example}
+
+
+In the previous examples patterns do not conflict with, but
+sometimes it is comfortable to write patterns that admits a non
+trivial superposition. Consider
+the boolean function $lef$ that given two natural numbers
+yields \verb+true+ if the first one is less or equal than the second
+one and \verb+false+ otherwise. We can write it as follows:
+
+\begin{coq_example}
+Fixpoint lef (n m:nat) {struct m} : bool :=
+ match n, m with
+ | O, x => true
+ | x, O => false
+ | S n, S m => lef n m
+ end.
+\end{coq_example}
+
+Note that the first and the second multiple pattern superpose because the couple of
+values \verb+O O+ matches both. Thus, what is the result of the
+function on those values?
+To eliminate ambiguity we use the {\em textual priority rule}: we
+consider patterns ordered from top to bottom, then a value is matched
+by the pattern at the $ith$ row if and only if is not matched by some
+pattern of a previous row. Thus in the example,
+\verb+O O+ is matched by the first pattern, and so \verb+(lef O O)+
+yields \verb+true+.
+
+Another way to write this function is:
+
+\begin{coq_example}
+Reset lef.
+Fixpoint lef (n m:nat) {struct m} : bool :=
+ match n, m with
+ | O, x => true
+ | S n, S m => lef n m
+ | _, _ => false
+ end.
+\end{coq_example}
+
+
+Here the last pattern superposes with the first two. Because
+of the priority rule, the last pattern
+will be used only for values that do not match neither the first nor
+the second one.
+
+Terms with useless patterns are accepted by the
+system. For example,
+\begin{coq_example}
+Check
+ (fun x:nat => match x with
+ | O => true
+ | S _ => false
+ | x => true
+ end).
+\end{coq_example}
+
+is accepted even though the last pattern is never used.
+Beware, the
+current implementation rises no warning message when there are unused
+patterns in a term.
+
+
+
+
+\subsection{About patterns of parametric types}
+When matching objects of a parametric type, constructors in patterns
+{\em do not expect} the parameter arguments. Their value is deduced
+during expansion.
+
+Consider for example the polymorphic lists:
+
+\begin{coq_example}
+Inductive List (A:Set) : Set :=
+ | nil : List A
+ | cons : A -> List A -> List A.
+\end{coq_example}
+
+We can check the function {\em tail}:
+
+\begin{coq_example}
+Check
+ (fun l:List nat =>
+ match l with
+ | nil => nil nat
+ | cons _ l' => l'
+ end).
+\end{coq_example}
+
+
+When we use parameters in patterns there is an error message:
+\begin{coq_example}
+Check
+ (fun l:List nat =>
+ match l with
+ | nil nat => nil nat
+ | cons nat _ l' => l'
+ end).
+\end{coq_example}
+
+
+
+\subsection{Matching objects of dependent types}
+The previous examples illustrate pattern matching on objects of
+non-dependent types, but we can also
+use the macro to destructure objects of dependent type.
+Consider the type \verb+listn+ of lists of a certain length:
+
+\begin{coq_example}
+Inductive listn : nat -> Set :=
+ | niln : listn 0%N
+ | consn : forall n:nat, nat -> listn n -> listn (S n).
+\end{coq_example}
+
+\subsubsection{Understanding dependencies in patterns}
+We can define the function \verb+length+ over \verb+listn+ by :
+
+\begin{coq_example}
+Definition length (n:nat) (l:listn n) := n.
+\end{coq_example}
+
+Just for illustrating pattern matching,
+we can define it by case analysis:
+\begin{coq_example}
+Reset length.
+Definition length (n:nat) (l:listn n) :=
+ match l with
+ | niln => 0%N
+ | consn n _ _ => S n
+ end.
+\end{coq_example}
+
+We can understand the meaning of this definition using the
+same notions of usual pattern matching.
+
+Now suppose we split the second pattern of \verb+length+ into two
+cases so to give an
+alternative definition using nested patterns:
+\begin{coq_example}
+Definition length1 (n:nat) (l:listn n) :=
+ match l with
+ | niln => 0%N
+ | consn n _ niln => S n
+ | consn n _ (consn _ _ _) => S n
+ end.
+\end{coq_example}
+
+It is obvious that \verb+length1+ is another version of
+\verb+length+. We can also give the following definition:
+\begin{coq_example}
+Definition length2 (n:nat) (l:listn n) :=
+ match l with
+ | niln => 0%N
+ | consn n _ niln => 1%N
+ | consn n _ (consn m _ _) => S (S m)
+ end.
+\end{coq_example}
+
+If we forget that \verb+listn+ is a dependent type and we read these
+definitions using the usual semantics of pattern matching, we can conclude
+that \verb+length1+
+and \verb+length2+ are different functions.
+In fact, they are equivalent
+because the pattern \verb+niln+ implies that \verb+n+ can only match
+the value $0$ and analogously the pattern \verb+consn+ determines that \verb+n+ can
+only match values of the form $(S~v)$ where $v$ is the value matched by
+\verb+m+.
+
+
+The converse is also true. If
+we destructure the length value with the pattern \verb+O+ then the list
+value should be $niln$.
+Thus, the following term \verb+length3+ corresponds to the function
+\verb+length+ but this time defined by case analysis on the dependencies instead of on the list:
+
+\begin{coq_example}
+Definition length3 (n:nat) (l:listn n) :=
+ match l with
+ | niln => 0%N
+ | consn O _ _ => 1%N
+ | consn (S n) _ _ => S (S n)
+ end.
+\end{coq_example}
+
+When we have nested patterns of dependent types, the semantics of
+pattern matching becomes a little more difficult because
+the set of values that are matched by a sub-pattern may be conditioned by the
+values matched by another sub-pattern. Dependent nested patterns are
+somehow constrained patterns.
+In the examples, the expansion of
+\verb+length1+ and \verb+length2+ yields exactly the same term
+ but the
+expansion of \verb+length3+ is completely different. \verb+length1+ and
+\verb+length2+ are expanded into two nested case analysis on
+\verb+listn+ while \verb+length3+ is expanded into a case analysis on
+\verb+listn+ containing a case analysis on natural numbers inside.
+
+
+In practice the user can think about the patterns as independent and
+it is the expansion algorithm that cares to relate them. \\
+
+
+\subsubsection{When the elimination predicate must be provided}
+The examples given so far do not need an explicit elimination predicate
+between \verb+<>+ because all the rhs have the same type and the
+strategy succeeds to synthesize it.
+Unfortunately when dealing with dependent patterns it often happens
+that we need to write cases where the type of the rhs are
+different instances of the elimination predicate.
+The function \verb+concat+ for \verb+listn+
+is an example where the branches have different type
+and we need to provide the elimination predicate:
+
+\begin{coq_example}
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+ match l in listn n return listn (n + m) with
+ | niln => l'
+ | consn n' a y => consn (n' + m) a (concat n' y m l')
+ end.
+\end{coq_example}
+
+Recall that a list of patterns is also a pattern. So, when
+we destructure several terms at the same time and the branches have
+different type we need to provide
+the elimination predicate for this multiple pattern.
+
+For example, an equivalent definition for \verb+concat+ (even though with a useless extra pattern) would have
+been:
+
+\begin{coq_example}
+Reset concat.
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+ match l in listn n, l' return listn (n + m) with
+ | niln, x => x
+ | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+ end.
+\end{coq_example}
+
+Note that this time, the predicate \verb+[n,_:nat](listn (plus n m))+ is binary because we
+destructure both \verb+l+ and \verb+l'+ whose types have arity one.
+In general, if we destructure the terms $e_1\ldots e_n$
+the predicate will be of arity $m$ where $m$ is the sum of the
+number of dependencies of the type of $e_1, e_2,\ldots e_n$ (the $\lambda$-abstractions
+should correspond from left to right to each dependent argument of the
+type of $e_1\ldots e_n$).
+When the arity of the predicate (i.e. number of abstractions) is not
+correct Coq rises an error message. For example:
+
+\begin{coq_example}
+Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
+ listn (n + m) :=
+ match l, l' with
+ | niln, x => x
+ | consn n' a y, x => consn (n' + m) a (concat n' y m x)
+ end.
+\end{coq_example}
+
+
+\subsection{Using pattern matching to write proofs}
+In all the previous examples the elimination predicate does not depend on the object(s) matched.
+The typical case where this is not possible is when we write a proof by
+induction or a function that yields an object of dependent type.
+
+For example, we can write
+the function \verb+buildlist+ that given a natural number
+$n$ builds a list length $n$ containing zeros as follows:
+
+\begin{coq_example}
+Fixpoint buildlist (n:nat) : listn n :=
+ match n return listn n with
+ | O => niln
+ | S n => consn n 0 (buildlist n)
+ end.
+\end{coq_example}
+
+We can also use multiple patterns whenever the elimination predicate has
+the correct arity.
+
+Consider the following definition of the predicate less-equal
+\verb+Le+:
+
+\begin{coq_example}
+Inductive Le : nat -> nat -> Prop :=
+ | LeO : forall n:nat, Le 0%N n
+ | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+\end{coq_example}
+
+We can use multiple patterns to write the proof of the lemma
+ \verb+(n,m:nat) (Le n m)\/(Le m n)+:
+
+\begin{coq_example}
+Fixpoint dec (n m:nat) {struct n} : Le n m \/ Le m n :=
+ match n, m return Le n m \/ Le m n with
+ | O, x => or_introl (Le x 0) (LeO x)
+ | x, O => or_intror (Le x 0) (LeO x)
+ | S n as N, S m as M =>
+ match dec n m with
+ | or_introl h => or_introl (Le M N) (LeS n m h)
+ | or_intror h => or_intror (Le N M) (LeS m n h)
+ end
+ end.
+\end{coq_example}
+In the example of \verb+dec+ the elimination predicate is binary
+because we destructure two arguments of \verb+nat+ that is a
+non-dependent type. Note the first \verb+Cases+ is dependent while the
+second is not.
+
+In general, consider the terms $e_1\ldots e_n$,
+where the type of $e_i$ is an instance of a family type
+$[\vec{d_i}:\vec{D_i}]T_i$ ($1\leq i
+\leq n$). Then to write \verb+<+${\cal P}$\verb+>Cases+ $e_1\ldots
+e_n$ \verb+of+ \ldots \verb+end+, the
+elimination predicate ${\cal P}$ should be of the form:
+$[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
+
+
+
+
+\section{Extending the syntax of pattern}
+The primitive syntax for patterns considers only those patterns containing
+symbols of constructors and variables. Nevertheless, we
+may define our own syntax for constructors and may be interested in
+using this syntax to write patterns.
+Because not any term is a pattern, the fact of extending the terms
+syntax does not imply the extension of pattern syntax. Thus,
+the grammar of patterns should be explicitly extended whenever we
+want to use a particular syntax for a constructor.
+The grammar rules for the macro \verb+Cases+ (and thus for patterns)
+are defined in the file \verb+Multcase.v+ in the directory
+\verb+src/syntax+. To extend the grammar of patterns
+we need to extend the non-terminals corresponding to patterns
+(we refer the reader to chapter of grammar extensions).
+
+
+We have already extended the pattern syntax so as to note
+the constructor \verb+pair+ of cartesian product with "( , )" in patterns.
+This allows for example, to write the first projection
+of pairs as follows:
+\begin{coq_example}
+Definition fst (A B:Set) (H:A * B) := match H with
+ | pair x y => x
+ end.
+\end{coq_example}
+The grammar presented in figure \ref{grammar} actually
+contains this extension.
+
+\section{When does the expansion strategy fail?}\label{limitations}
+The strategy works very like in ML languages when treating
+patterns of non-dependent type.
+But there are new cases of failure that are due to the presence of
+dependencies.
+
+The error messages of the current implementation may be
+sometimes confusing.
+When the tactic fails because patterns are somehow incorrect then
+error messages refer to the initial expression. But the strategy
+may succeed to build an expression whose sub-expressions are well typed but
+the whole expression is not. In this situation the message makes
+reference to the expanded expression.
+We encourage users, when they have patterns with the same outer constructor in different equations, to name the variable patterns in the same positions with the same name.
+E.g. to write {\small\verb+(cons n O x) => e1+} and {\small\verb+(cons n \_ x) => e2+} instead of
+{\small\verb+(cons n O x) => e1+} and {\small\verb+(cons n' \_ x') => e2+}. This helps to maintain certain name correspondence between the generated expression and the original.
+
+
+Here is a summary of the error messages corresponding to each situation:
+\begin{itemize}
+\item patterns are incorrect (because constructors are not
+applied to the correct number of the arguments, because they are not linear or they are
+wrongly typed)
+\begin{itemize}
+\item \sverb{In pattern } {\sl term} \sverb{the constructor } {\sl ident}
+\sverb{expects } {\sl num} \sverb{arguments}
+
+\item \sverb{The variable } {\sl ident} \sverb{is bound several times in pattern } {\sl term}
+
+\item \sverb{Constructor pattern: } {\sl term} \sverb{cannot match values of type } {\sl term}
+\end{itemize}
+
+\item the pattern matching is not exhaustive
+\begin{itemize}
+\item \sverb{This pattern-matching is not exhaustive}
+\end{itemize}
+\item the elimination predicate provided to \verb+Cases+ has not the expected arity
+
+\begin{itemize}
+\item \sverb{The elimination predicate } {\sl term} \sverb{should be
+of arity } {\sl num} \sverb{(for non dependent case) or } {\sl num} \sverb{(for dependent case)}
+\end{itemize}
+
+ \item the whole expression is wrongly typed, or the synthesis of implicit arguments fails (for example to find
+the elimination predicate or to resolve implicit arguments in the rhs).
+
+
+There are {\em nested patterns of dependent type}, the
+elimination predicate corresponds to non-dependent case and has the form $[x_1:T_1]...[x_n:T_n]T$
+and {\bf some} $x_i$ occurs {\bf free} in
+$T$. Then, the strategy may fail to find out a correct elimination
+predicate during some step of compilation.
+In this situation we recommend the user to rewrite the nested
+dependent patterns into several \verb+Cases+ with {\em simple patterns}.
+
+In all these cases we have the following error message:
+
+ \begin{itemize}
+ \item
+ {\tt Expansion strategy failed to build a well typed case expression.
+ There is a branch that mismatches the expected type.
+ The risen type error on the result of expansion was:}
+ \end{itemize}
+
+\item because of nested patterns, it may happen that even though all
+the rhs have the same type, the strategy needs
+dependent elimination and so an elimination predicate must be
+provided. The system
+warns about this situation, trying to compile anyway with the
+non-dependent strategy. The risen message is:
+\begin{itemize}
+\item {\tt Warning: This pattern matching may need dependent elimination to be compiled.
+I will try, but if fails try again giving dependent elimination predicate.}
+\end{itemize}
+
+\item there are {\em nested patterns of dependent type} and the strategy
+builds a term that is well typed but recursive
+calls in fix point are reported as illegal:
+\begin{itemize}
+\item {\tt Error: Recursive call applied to an illegal term ...}
+\end{itemize}
+
+This is because the strategy generates a term that is correct
+w.r.t. to the initial term but which does not pass the guard condition.
+In this situation we recommend the user to transform the nested dependent
+patterns into {\em several \verb+Cases+ of simple patterns}.
+Let us explain this with an example.
+Consider the following defintion of a function that yields the last
+element of a list and \verb+O+ if it is empty:
+
+\begin{coq_example}
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+ match l with
+ | consn _ a niln => a
+ | consn m _ x => last m x
+ | niln => 0%N
+ end.
+\end{coq_example}
+
+It fails because of the priority between patterns, we know that this
+definition is equivalent to the following more explicit one (which
+fails too):
+
+\begin{coq_example*}
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+ match l with
+ | consn _ a niln => a
+ | consn n _ (consn m b x) => last n (consn m b x)
+ | niln => 0%N
+ end.
+\end{coq_example*}
+
+Note that the recursive call \sverb{(last n (consn m b x)) } is not
+guarded. When treating with patterns of dependent types the strategy
+interprets the first definition of \texttt{last} as the second
+onefootnote{In languages of the ML family
+the first definition would be translated into a term where the
+variable \texttt{x} is shared in the expression. When
+patterns are of non-dependent types, Coq compiles as in ML languages
+using sharing. When patterns are of dependent types the compilation
+reconstructs the term as in the second definition of \texttt{last} so to
+ensure the result of expansion is well typed.}.
+Thus it generates a
+term where the recursive call is rejected by the
+guard condition.
+
+You can get rid of this problem by writing the definition with \emph{simple
+patterns}:
+
+\begin{coq_example}
+Fixpoint last (n:nat) (l:listn n) {struct l} : nat :=
+ match l return nat with
+ | consn m a x => match x with
+ | niln => a
+ | _ => last m x
+ end
+ | niln => 0%N
+ end.
+\end{coq_example}
+
+
+\end{itemize}
+
+%\end{document}
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 13:20:28 +0000