passage V8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8343 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 158 insertions, 137 deletions

diff --git a/doc/RefMan-cas.tex b/doc/RefMan-cas.tex
index f48242fae..c79c14e9b 100755
--- a/doc/RefMan-cas.tex
+++ b/doc/RefMan-cas.tex
@@ -109,7 +109,10 @@ using the command \texttt{Check}  that displays
 the term with its type :
 
 \begin{coq_example}
-Check [n:nat] Cases n of O => true | _ => false end.
+Check (fun n:nat => match n with
+                    | O => true
+                    | _ => false
+                    end).
 \end{coq_example}
 
 
@@ -128,28 +131,33 @@ 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] : nat :=
-        Case n of
-         (*  O   *) m
-         (* S n' *) [n':nat]Case m of
-                             (* O    *) (S n')
-                             (* S m' *) [m':nat](S (max n' m'))
-                            end
-        end.
+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] : nat :=
-          Cases n of 
-             O     => m
-          | (S n') => Cases m of
-                         O      => (S n')
-                       | (S m') => (S (max n' m'))
-                      end
-         end.
+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
@@ -157,12 +165,12 @@ Another way to write this definition is to use a multiple pattern to
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n,m:nat] : nat :=
-          Cases n m of
-             O         _  => m   
-          | (S n') O      => (S n')
-          | (S n') (S m') => (S (max n' m')) 
-         end.
+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}
 
 
@@ -170,7 +178,9 @@ 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 [x:nat]<nat>Cases x of y => y end.
+Check (fun x:nat => match x return nat with
+                    | y => y
+                    end).
 \end{coq_example}
 
 
@@ -180,12 +190,12 @@ sub-pattern:
 
 \begin{coq_example}
 Reset max.
-Fixpoint max [n:nat] : nat -> nat :=
-  [m:nat] Cases n m of
-             O     _         => m   
-          | ((S n') as N) O  => N
-          | (S n') (S m')    => (S (max n' m')) 
-         end.
+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}
 
 
@@ -197,12 +207,12 @@ 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] : bool :=
-         Cases n m of
-             O     x     => true 
-          |  x     O     => false 
-          | (S n) (S m)  => (lef n m)
-         end.
+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
@@ -219,12 +229,12 @@ Another way to write  this function is:
 
 \begin{coq_example}
 Reset lef.
-Fixpoint lef [n,m:nat] : bool :=
-         Cases n m of
-             O     x    => true  
-          | (S n) (S m) => (lef n m)
-          |  _     _    => false
-         end.
+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}
 
 
@@ -236,7 +246,12 @@ the second one.
 Terms with useless patterns are accepted by the
 system. For example,
 \begin{coq_example}
-Check [x:nat]Cases x of O => true | (S _) => false | x => true end.
+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.
@@ -255,27 +270,31 @@ 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).
+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 [l:(List nat)]Cases l of 
-                             nil        => (nil nat)
-                          | (cons _ l') => l'
-                           end.
+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 [l:(List nat)]Cases l of 
-                             (nil nat)      => (nil nat)
-                          | (cons nat _ l') => l'
-                           end.
+Check
+  (fun l:List nat =>
+     match l with
+     | nil nat => nil nat
+     | cons nat _ l' => l'
+     end).
 \end{coq_example}
 
 
@@ -287,27 +306,27 @@ 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 O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+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.
+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)]
-                      Cases l of  
-                         niln         => O 
-                      | (consn n _ _) => (S n) 
-                      end.
+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
@@ -317,23 +336,23 @@ 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)]
-   Cases l of 
-        niln                   => O
-   | (consn n _ niln)          => (S n)
-   | (consn n _ (consn _ _ _)) => (S n)
+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)]
- Cases l of 
-     niln                    => O
- | (consn n _ niln)          => (S O)
- | (consn n _ (consn m _ _)) => (S (S m))
- end.
+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
@@ -354,12 +373,12 @@ 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)]
-                         Cases l of 
-                            niln              => O
-                         |  (consn O _ _)     => (S O)
-                         |  (consn (S n) _ _) => (S (S n))
-                         end.
+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
@@ -392,12 +411,12 @@ 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) (listn m) -> (listn (plus n m))
- := [m:nat][l':(listn m)] 
-       <[n:nat](listn (plus n m))>Cases l  of 
-           niln          => l'
-        | (consn n' a y) => (consn (plus n' m) a (concat n' y m l'))
-        end.
+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
@@ -410,12 +429,12 @@ been:
 
 \begin{coq_example}
 Reset concat.
-Fixpoint concat [n:nat; l:(listn n)] : (m:nat) (listn m) -> (listn (plus n m)) 
-:= [m:nat][l':(listn m)] 
-    <[n,_:nat](listn (plus n m))>Cases l l' of 
-                     niln          x => x
-                  | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-                  end.
+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
@@ -429,12 +448,12 @@ 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) (listn m) -> (listn (plus n m)) := 
-[m:nat][l':(listn m)] 
-     <[n:nat](listn (plus n m))>Cases l l' of 
-                     niln          x => x
-                  | (consn n' a y) x => (consn (plus n' m) a (concat n' y m x))
-                  end.
+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}
 
 
@@ -448,11 +467,11 @@ 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) :=
-    <[n:nat](listn n)>Cases n of 
-           O    => niln 
-       |  (S n) => (consn n O (buildlist n))
-       end.
+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
@@ -462,25 +481,25 @@ Consider the following definition of the predicate less-equal
 \verb+Le+:
 
 \begin{coq_example}
-Inductive Le : nat->nat->Prop :=
-  LeO: (n:nat)(Le O n)
-| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+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:nat] : (m:nat)(Le n m) \/ (Le m n) :=
- [m:nat] <[n,m:nat](Le n m) \/ (Le m n)>Cases n m of
-           O   x =>  (or_introl ? (Le x O) (LeO x))
-         | x   O =>  (or_intror (Le x O) ? (LeO x))
-         | ((S n) as N) ((S m) as M) =>
-              Cases (dec n m) of
-                  (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.
+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
@@ -519,7 +538,9 @@ 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] Cases H of (x,y) => x end.
+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. 
@@ -615,12 +636,12 @@ 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)] : nat :=
-Cases l of
-    (consn _ a niln) => a
- |  (consn m _ x)    => (last m x)
- |   niln            => O
- end.
+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
@@ -628,12 +649,12 @@ definition is equivalent to the following more explicit one (which
 fails too):
 
 \begin{coq_example*}
-Fixpoint last [n:nat; l:(listn n)] : nat :=
-Cases l of
-    (consn _ a niln)          => a
- |  (consn n _ (consn m b x)) => (last n (consn m b x))
- |   niln                     => O
- end.
+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
@@ -654,14 +675,14 @@ 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>Cases l of
-    (consn m a x) => Cases x of
-                         niln => a
-                     |   _    => (last m x)
-                     end
- |   niln         => O
- end.
+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}