diff options
Diffstat (limited to 'doc/refman/Cases.tex')
| -rw-r--r-- | doc/refman/Cases.tex | 698 |
1 files changed, 698 insertions, 0 deletions
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex new file mode 100644 index 00000000..95411afa --- /dev/null +++ b/doc/refman/Cases.tex @@ -0,0 +1,698 @@ +\achapter{Extended pattern-matching}\defaultheaders +\aauthor{Cristina Cornes} + +\label{Mult-match-full} +\ttindex{Cases} +\index{ML-like patterns} + +This section describes the full form of pattern-matching in {\Coq} terms. + +\asection{Patterns}\label{implementation} The full syntax of {\tt +match} is presented in figures~\ref{term-syntax} +and~\ref{term-syntax-aux}. Identifiers in patterns are either +constructor names or variables. Any identifier that is not the +constructor of an inductive or coinductive type is considered to be a +variable. A variable name cannot occur more than once in a given +pattern. It is recommended to start variable names by a lowercase +letter. + +If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor +symbol and $\vec{x}$ is a linear vector of variables, it is called +{\em simple}: it is the kind of pattern recognized by the basic +version of {\tt match}. 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 ``\texttt{\_}'' (called ``don't care'' or +``wildcard'' symbol) also matches any value, but does not bind anything. It +may occur an arbitrary number of times in a pattern. Alias patterns +written \texttt{(}{\sl pattern} \texttt{as} {\sl identifier}\texttt{)} 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 separated with commas +is also considered as a pattern and is called {\em multiple +pattern}. + +Since extended {\tt match} expressions are compiled into the primitive +ones, the expressiveness of the theory remains the same. Once the +stage of parsing has finished only simple patterns remain. 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}. + +The extended \texttt{match} still accepts an optional {\em elimination +predicate} given after the keyword \texttt{return}. Given a pattern +matching expression, if all the right hand sides of \texttt{=>} ({\em +rhs} in short) have the same type, then this type can be sometimes +synthesized, and so we can omit the \texttt{return} part. Otherwise +the predicate after \texttt{return} has to be provided, like for the basic +\texttt{match}. + +Let us illustrate through examples the different aspects of extended +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 => m + | S n' => match m with + | O => S n' + | S m' => S (max n' m') + end + end. +\end{coq_example} + +Using multiple patterns in the definition allows to write: + +\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} + +which will be compiled into the previous form. + +The pattern-matching compilation strategy examines patterns from left +to right. A \texttt{match} expression is generated {\bf only} when +there is at least one constructor in the column of patterns. E.g. the +following example does not build a \texttt{match} expression. + +\begin{coq_example} +Check (fun x:nat => match x return nat with + | y => y + end). +\end{coq_example} + +We can also use ``\texttt{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 p, O => p + | S n', S m' => S (max n' m') + end. +\end{coq_example} + +Here is now an example of nested patterns: + +\begin{coq_example} +Fixpoint even (n:nat) : bool := + match n with + | O => true + | S O => false + | S (S n') => even n' + end. +\end{coq_example} + +This is compiled into: + +\begin{coq_example} +Print even. +\end{coq_example} + +In the previous examples patterns do not conflict with, but +sometimes it is comfortable to write patterns that admit a non +trivial superposition. Consider +the boolean function \texttt{lef} that given two natural numbers +yields \texttt{true} if the first one is less or equal than the second +one and \texttt{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 \texttt{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 it is not matched by some pattern of a previous row. Thus in the +example, +\texttt{O O} is matched by the first pattern, and so \texttt{(lef O O)} +yields \texttt{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 not accepted by the +system. Here is an example: +% Test failure +\begin{coq_eval} +Set Printing Depth 50. + (********** The following is not correct and should produce **********) + (**************** Error: This clause is redundant ********************) +\end{coq_eval} +\begin{coq_example} +Check (fun x:nat => + match x with + | O => true + | S _ => false + | x => true + end). +\end{coq_example} + +\asection{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: +% Test failure +\begin{coq_eval} +Set Printing Depth 50. +(********** The following is not correct and should produce **********) +(******** Error: The constructor cons expects 2 arguments ************) +\end{coq_eval} +\begin{coq_example} +Check + (fun l:List nat => + match l with + | nil A => nil nat + | cons A _ l' => l' + end). +\end{coq_example} + + + +\asection{Matching objects of dependent types} +The previous examples illustrate pattern matching on objects of +non-dependent types, but we can also +use the expansion strategy to destructure objects of dependent type. +Consider the type \texttt{listn} of lists of a certain length: + +\begin{coq_example} +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n:nat, nat -> listn n -> listn (S n). +\end{coq_example} + +\asubsection{Understanding dependencies in patterns} +We can define the function \texttt{length} over \texttt{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 + | consn n _ _ => S n + end. +\end{coq_example} + +We can understand the meaning of this definition using the +same notions of usual pattern matching. + +% +% Constraining of dependencies is not longer valid in V7 +% +\iffalse +Now suppose we split the second pattern of \texttt{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 + | consn n _ niln => S n + | consn n _ (consn _ _ _) => S n + end. +\end{coq_example} + +It is obvious that \texttt{length1} is another version of +\texttt{length}. We can also give the following definition: +\begin{coq_example} +Definition length2 (n:nat) (l:listn n) := + match l with + | niln => 0 + | consn n _ niln => 1 + | consn n _ (consn m _ _) => S (S m) + end. +\end{coq_example} + +If we forget that \texttt{listn} is a dependent type and we read these +definitions using the usual semantics of pattern matching, we can conclude +that \texttt{length1} +and \texttt{length2} are different functions. +In fact, they are equivalent +because the pattern \texttt{niln} implies that \texttt{n} can only match +the value $0$ and analogously the pattern \texttt{consn} determines that \texttt{n} can +only match values of the form $(S~v)$ where $v$ is the value matched by +\texttt{m}. + +The converse is also true. If +we destructure the length value with the pattern \texttt{O} then the list +value should be $niln$. +Thus, the following term \texttt{length3} corresponds to the function +\texttt{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 + | consn O _ _ => 1 + | 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 +\texttt{length1} and \texttt{length2} yields exactly the same term + but the +expansion of \texttt{length3} is completely different. \texttt{length1} and +\texttt{length2} are expanded into two nested case analysis on +\texttt{listn} while \texttt{length3} is expanded into a case analysis on +\texttt{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. \\ +\fi +% +% +% + +\asubsection{When the elimination predicate must be provided} +The examples given so far do not need an explicit elimination predicate + 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 \texttt{concat} for \texttt{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} +The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}. +In general if $m$ has type $(I~q_1\ldots q_r~t_1\ldots t_s)$ where +$q_1\ldots q_r$ are parameters, the elimination predicate should be of +the form~: +{\tt fun $y_1$\ldots $y_s$ $x$:($I$~$q_1$\ldots $q_r$~$y_1$\ldots + $y_s$) => P}. + +In the concrete syntax, it should be written~: +\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_\ldots \_~y_1\ldots y_s)~\kw{return}~Q~\kw{with}~\ldots~\kw{end}\] + +The variables which appear in the \kw{in} and \kw{as} clause are new +and bounded in the property $Q$ in the \kw{return} clause. The +parameters of the inductive definitions should not be mentioned and +are replaced by \kw{\_}. + +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. +It is done using the same scheme, each term may be associated to an +\kw{as} and \kw{in} clause in order to introduce a dependent product. + +For example, an equivalent definition for \texttt{concat} (even though the matching on the second term is trivial) 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} + +% Notice that this time, the predicate \texttt{[n,\_:nat](listn (plus n +% m))} is binary because we +% destructure both \texttt{l} and \texttt{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 raises an error message. For example: + +% Test failure +\begin{coq_eval} +Reset concat. +Set Printing Depth 50. +(********** The following is not correct and should produce ***********) +(** Error: the term l' has type listn m while it is expected to have **) +(** type listn (?31 + ?32) **) +\end{coq_eval} +\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} + +\asection{Using pattern matching to write proofs} +In all the previous examples the elimination predicate does not depend +on the object(s) matched. But it may depend and the typical case +is when we write a proof by induction or a function that yields an +object of dependent type. An example of proof using \texttt{match} in +given in section \ref{refine-example} + +For example, we can write +the function \texttt{buildlist} that given a natural number +$n$ builds a list of 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. +Consider the following definition of the predicate less-equal +\texttt{Le}: + +\begin{coq_example} +Inductive LE : nat -> nat -> Prop := + | LEO : forall n:nat, LE 0 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 + \texttt{(n,m:nat) (LE n m)}\verb=\/=\texttt{(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 \texttt{dec}, +the first \texttt{match} 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 +% $\lb (\vec{d_i}:\vec{D_i}) \mto T_i$ ($1\leq i +% \leq n$). Then, in expression \texttt{match} $e_1,\ldots, +% e_n$ \texttt{of} \ldots \texttt{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.$ + +The user can also use \texttt{match} in combination with the tactic +\texttt{refine} (see section \ref{refine}) to build incomplete proofs +beginning with a \texttt{match} construction. + +\asection{Pattern-matching on inductive objects involving local +definitions} + +If local definitions occur in the type of a constructor, then there +are two ways to match on this constructor. Either the local +definitions are skipped and matching is done only on the true arguments +of the constructors, or the bindings for local definitions can also +be caught in the matching. + +Example. + +\begin{coq_eval} +Reset Initial. +Require Import Arith. +\end{coq_eval} + +\begin{coq_example*} +Inductive list : nat -> Set := + | nil : list 0 + | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). +\end{coq_example*} + +In the next example, the local definition is not caught. + +\begin{coq_example} +Fixpoint length n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | cons n l0 => S (length (2 * n) l0) + end. +\end{coq_example} + +But in this example, it is. + +\begin{coq_example} +Fixpoint length' n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | cons _ m l0 => S (length' m l0) + end. +\end{coq_example} + +\Rem for a given matching clause, either none of the local +definitions or all of them can be caught. + +\asection{Pattern-matching and coercions} + +If a mismatch occurs between the expected type of a pattern and its +actual type, a coercion made from constructors is sought. If such a +coercion can be found, it is automatically inserted around the +pattern. + +Example: + +\begin{coq_example} +Inductive I : Set := + | C1 : nat -> I + | C2 : I -> I. +Coercion C1 : nat >-> I. +Check (fun x => match x with + | C2 O => 0 + | _ => 0 + end). +\end{coq_example} + + +\asection{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 when 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\texttt{(cons n O x) => e1}} +and {\small\texttt{(cons n \_ x) => e2}} instead of +{\small\texttt{(cons n O x) => e1}} and +{\small\texttt{(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{ErrMsgs} +\item \sverb{The constructor } {\sl + ident} \sverb{expects } {\sl num} \sverb{arguments} + + \sverb{The variable } {\sl ident} \sverb{is bound several times + in pattern } {\sl term} + + \sverb{Found a constructor of inductive type} {\term} + \sverb{while a constructor of} {\term} \sverb{is expected} + + 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) + +\item \errindex{Non exhaustive pattern-matching} + +the pattern matching is not exhaustive + +\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)} + +The elimination predicate provided to \texttt{match} has not the + expected arity + + +%\item the whole expression is wrongly typed + +% CADUC ? +% , 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 \texttt{match} with {\em simple patterns}. + +\item {\tt Unable to infer a match predicate\\ + Either there is a type incompatiblity or the problem involves\\ + dependencies} + + There is a type mismatch between the different branches + + Then the user should provide an elimination predicate. + +% Obsolete ? +% \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} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % LA PROPAGATION DES CONTRAINTES ARRIERE N'EST PAS FAITE DANS LA V7 +% TODO +% \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. +% 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 \texttt{match} of simple patterns}. Let us +% explain this with an example. Consider the following definition of a +% function that yields the last element of a list and \texttt{O} if it is +% empty: + +% \begin{coq_example} +% Fixpoint last [n:nat; l:(listn n)] : nat := +% match l of +% (consn _ a niln) => a +% | (consn m _ x) => (last m x) | niln => O +% 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)] : nat := +% match l of +% (consn _ a niln) => a +% | (consn n _ (consn m b x)) => (last n (consn m b x)) +% | niln => O +% end. +% \end{coq_example*} + +% Note that the recursive call {\tt (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 +% one\footnote{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)] : nat := +% <[_:nat]nat>match l of +% (consn m a x) => Cases x of niln => a | _ => (last m x) end +% | niln => O +% end. +% \end{coq_example} + +\end{ErrMsgs} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |