diff options
Diffstat (limited to 'doc/refman/RefMan-cas.tex')
-rwxr-xr-x | doc/refman/RefMan-cas.tex | 692 |
1 files changed, 692 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cas.tex b/doc/refman/RefMan-cas.tex new file mode 100755 index 000000000..c79c14e9b --- /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} + |