From db6262fd028086c6201fe4894243fcf691c65099 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 10:01:01 +0100
Subject: [Sphinx] Move chapter 17 to new infrastructure

---
 Makefile.doc                                      |   2 +-
 doc/refman/Cases.tex                              | 843 ----------------------
 doc/refman/Reference-Manual.tex                   |   1 -
 doc/sphinx/addendum/extended-pattern-matching.rst | 843 ++++++++++++++++++++++
 4 files changed, 844 insertions(+), 845 deletions(-)
 delete mode 100644 doc/refman/Cases.tex
 create mode 100644 doc/sphinx/addendum/extended-pattern-matching.rst

diff --git a/Makefile.doc b/Makefile.doc
index df1e2d3c4..6f4bcfb67 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
-  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
+  Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
   Setoid.v.tex Classes.v.tex Universes.v.tex \
   Misc.v.tex)
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
deleted file mode 100644
index 376ef031d..000000000
--- a/doc/refman/Cases.tex
+++ /dev/null
@@ -1,843 +0,0 @@
-\achapter{Extended pattern-matching}
-%HEVEA\cutname{cases.html}
-%BEGIN LATEX
-\defaultheaders
-%END LATEX
-\aauthor{Cristina Cornes and Hugo Herbelin}
-
-\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 co-inductive 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 (distinct) variables, it is
-called {\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt match}. On the opposite, if it is a variable $x$ or
-has the form $(c~\vec{p})$ with $p$ not only made of variables, the
-pattern is called {\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 pattern of the form {\pattern}{\tt |}{\pattern} is called
-disjunctive. A list of patterns separated with commas is also
-considered as a pattern and is called {\em multiple pattern}. However
-multiple patterns can only occur at the root of pattern-matching
-equations. Disjunctions of {\em multiple pattern} are allowed though.
-
-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.  Re-nesting
-of pattern is performed at printing time. An easy way to see the
-result of the expansion is to toggle off the nesting performed at
-printing (use here {\tt Set Printing Matching}), then 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}
-
-\paragraph{Multiple patterns}
-
-Using multiple patterns in the definition of {\tt max} lets us write:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-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}
-
-\paragraph{Aliasing subpatterns}
-
-We can also use ``\texttt{as} {\ident}'' to associate a name to a
-sub-pattern:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-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}
-
-\paragraph{Nested patterns}
-
-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}
-Unset Printing Matching.
-Print even.
-\end{coq_example}
-\begin{coq_eval}
-Set Printing Matching.
-\end{coq_eval}
-
-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_eval}
-Reset lef.
-\end{coq_eval}
-\begin{coq_example}
-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: "This clause is redundant."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check (fun x:nat =>
-         match x with
-         | O => true
-         | S _ => false
-         | x => true
-         end).
-\end{coq_example}
-
-\paragraph{Disjunctive patterns}
-
-Multiple patterns that share the same right-hand-side can be
-factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
-{\tt max} can be rewritten as follows:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct m} : nat :=
-  match n, m with
-  | S n', S m' => S (max n' m')
-  | 0, p | p, 0 => p
-  end.
-\end{coq_example}
-
-Similarly, factorization of (non necessary multiple) patterns
-that share the same variables is possible by using the notation
-\nelist{\pattern}{\tt |}. Here is an example:
-
-\begin{coq_example}
-Definition filter_2_4 (n:nat) : nat :=
-  match n with
-  | 2 as m | 4 as m => m
-  | _ => 0
-  end.
-\end{coq_example}
-
-Here is another example using disjunctive subpatterns.
-
-\begin{coq_example}
-Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
-  match p with
-  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
-  | _ => (0,0)
-  end.
-\end{coq_example}
-
-\asection{About patterns of parametric types}
-\paragraph{Parameters in patterns}
-When matching objects of a parametric type, parameters do not bind in patterns.
-They must be substituted by ``\_''.
-Consider for example the type of 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: "The parameters do not bind in patterns."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check
-  (fun l:List nat =>
-     match l with
-     | nil A => nil nat
-     | cons A _ l' => l'
-     end).
-\end{coq_example}
-
-The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
-(off by default) removes parameters from constructors in patterns:
-\begin{coq_example}
-  Set Asymmetric Patterns.
-  Check (fun l:List nat =>
-    match l with
-    | nil => nil
-    | cons _ l' => l'
-    end)
-  Unset Asymmetric Patterns.
-\end{coq_example}
-
-\paragraph{Implicit arguments in patterns}
-By default, implicit arguments are omitted in patterns. So we write:
-
-\begin{coq_example}
-Arguments nil [A].
-Arguments cons [A] _ _.
-Check
-  (fun l:List nat =>
-     match l with
-     | nil => nil
-     | cons _ l' => l'
-     end).
-\end{coq_example}
-
-But the possibility to use all the arguments is given by ``{\tt @}'' implicit
-explicitations (as for terms~\ref{Implicits-explicitation}).
-
-\begin{coq_example}
-Check
-  (fun l:List nat =>
-     match l with
-     | @nil _ => @nil nat
-     | @cons _ _ 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:
-\label{listn}
-
-\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_eval}
-Reset length.
-\end{coq_eval}
-\begin{coq_example}
-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}
-\paragraph{Dependent pattern matching}
-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 {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where
-$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of
-the form~:
-{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots}
-  $y_s${\tt ) =>} $Q$.
-
-In the concrete syntax, it should be written~:
-\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\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{\_}.
-
-\paragraph{Multiple dependent pattern matching}
-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 types 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_eval}
-Reset concat.
-\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 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}
-
-Even without real matching over the second term, this construction can be used to
-keep types linked.  If {\tt a} and {\tt b} are two {\tt listn} of the same length,
-by writing
-\begin{coq_eval}
-  Unset Printing Matching.
-\end{coq_eval}
-\begin{coq_example}
-Check (fun n (a b: listn n) => match a,b with
- |niln,b0 => tt
- |consn n' a y, bS => tt
-end).
-\end{coq_example}
-\begin{coq_eval}
-  Set Printing Matching.
-\end{coq_eval}
-
-I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
-
-% 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}
-
-\paragraph{Patterns in {\tt in}}
-\label{match-in-patterns}
-
-If the type of the matched term is more precise than an inductive applied to
-variables, arguments of the inductive in the {\tt in} branch can be more
-complicated patterns than a variable.
-
-Moreover, constructors whose type do not follow the same pattern will
-become impossible branches. In an impossible branch, you can answer
-anything but {\tt False\_rect unit} has the advantage to be subterm of
-anything. % ???
-
-To be concrete: the {\tt tail} function can be written:
-\begin{coq_example}
-Definition tail n (v: listn (S n)) :=
-  match v in listn (S m) return listn m with
-  | niln => False_rect unit
-  | consn n' a y => y
-  end.
-\end{coq_example}
-and {\tt tail n v} will be subterm of {\tt v}.
-
-\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{forall (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.
-
-\Rem you can only catch {\tt let} bindings in mode where you bind all variables and so you
-have to use @ syntax.
-
-\Rem this feature is incoherent with the fact that parameters cannot be caught and
-consequently is somehow hidden. For example, there is no mention of it in error messages.
-
-\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 incompatibility or the problem involves\\
-    dependencies}
-
-  There is a type mismatch between the different branches.
-  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:
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 231742e56..7ef676ba9 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.}
 %END LATEX
 \part{Addendum to the Reference Manual}
 \include{AddRefMan-pre}%
-\include{Cases.v}%
 \include{Coercion.v}%
 \include{CanonicalStructures.v}%
 \include{Classes.v}%
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
new file mode 100644
index 000000000..376ef031d
--- /dev/null
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -0,0 +1,843 @@
+\achapter{Extended pattern-matching}
+%HEVEA\cutname{cases.html}
+%BEGIN LATEX
+\defaultheaders
+%END LATEX
+\aauthor{Cristina Cornes and Hugo Herbelin}
+
+\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 co-inductive 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 (distinct) variables, it is
+called {\em simple}: it is the kind of pattern recognized by the basic
+version of {\tt match}. On the opposite, if it is a variable $x$ or
+has the form $(c~\vec{p})$ with $p$ not only made of variables, the
+pattern is called {\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 pattern of the form {\pattern}{\tt |}{\pattern} is called
+disjunctive. A list of patterns separated with commas is also
+considered as a pattern and is called {\em multiple pattern}. However
+multiple patterns can only occur at the root of pattern-matching
+equations. Disjunctions of {\em multiple pattern} are allowed though.
+
+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.  Re-nesting
+of pattern is performed at printing time. An easy way to see the
+result of the expansion is to toggle off the nesting performed at
+printing (use here {\tt Set Printing Matching}), then 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}
+
+\paragraph{Multiple patterns}
+
+Using multiple patterns in the definition of {\tt max} lets us write:
+
+\begin{coq_eval}
+Reset max.
+\end{coq_eval}
+\begin{coq_example}
+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}
+
+\paragraph{Aliasing subpatterns}
+
+We can also use ``\texttt{as} {\ident}'' to associate a name to a
+sub-pattern:
+
+\begin{coq_eval}
+Reset max.
+\end{coq_eval}
+\begin{coq_example}
+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}
+
+\paragraph{Nested patterns}
+
+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}
+Unset Printing Matching.
+Print even.
+\end{coq_example}
+\begin{coq_eval}
+Set Printing Matching.
+\end{coq_eval}
+
+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_eval}
+Reset lef.
+\end{coq_eval}
+\begin{coq_example}
+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: "This clause is redundant."
+\begin{coq_eval}
+Set Printing Depth 50.
+\end{coq_eval}
+\begin{coq_example}
+Fail Check (fun x:nat =>
+         match x with
+         | O => true
+         | S _ => false
+         | x => true
+         end).
+\end{coq_example}
+
+\paragraph{Disjunctive patterns}
+
+Multiple patterns that share the same right-hand-side can be
+factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
+{\tt max} can be rewritten as follows:
+
+\begin{coq_eval}
+Reset max.
+\end{coq_eval}
+\begin{coq_example}
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n, m with
+  | S n', S m' => S (max n' m')
+  | 0, p | p, 0 => p
+  end.
+\end{coq_example}
+
+Similarly, factorization of (non necessary multiple) patterns
+that share the same variables is possible by using the notation
+\nelist{\pattern}{\tt |}. Here is an example:
+
+\begin{coq_example}
+Definition filter_2_4 (n:nat) : nat :=
+  match n with
+  | 2 as m | 4 as m => m
+  | _ => 0
+  end.
+\end{coq_example}
+
+Here is another example using disjunctive subpatterns.
+
+\begin{coq_example}
+Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
+  match p with
+  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
+  | _ => (0,0)
+  end.
+\end{coq_example}
+
+\asection{About patterns of parametric types}
+\paragraph{Parameters in patterns}
+When matching objects of a parametric type, parameters do not bind in patterns.
+They must be substituted by ``\_''.
+Consider for example the type of 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: "The parameters do not bind in patterns."
+\begin{coq_eval}
+Set Printing Depth 50.
+\end{coq_eval}
+\begin{coq_example}
+Fail Check
+  (fun l:List nat =>
+     match l with
+     | nil A => nil nat
+     | cons A _ l' => l'
+     end).
+\end{coq_example}
+
+The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
+(off by default) removes parameters from constructors in patterns:
+\begin{coq_example}
+  Set Asymmetric Patterns.
+  Check (fun l:List nat =>
+    match l with
+    | nil => nil
+    | cons _ l' => l'
+    end)
+  Unset Asymmetric Patterns.
+\end{coq_example}
+
+\paragraph{Implicit arguments in patterns}
+By default, implicit arguments are omitted in patterns. So we write:
+
+\begin{coq_example}
+Arguments nil [A].
+Arguments cons [A] _ _.
+Check
+  (fun l:List nat =>
+     match l with
+     | nil => nil
+     | cons _ l' => l'
+     end).
+\end{coq_example}
+
+But the possibility to use all the arguments is given by ``{\tt @}'' implicit
+explicitations (as for terms~\ref{Implicits-explicitation}).
+
+\begin{coq_example}
+Check
+  (fun l:List nat =>
+     match l with
+     | @nil _ => @nil nat
+     | @cons _ _ 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:
+\label{listn}
+
+\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_eval}
+Reset length.
+\end{coq_eval}
+\begin{coq_example}
+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}
+\paragraph{Dependent pattern matching}
+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 {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where
+$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of
+the form~:
+{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots}
+  $y_s${\tt ) =>} $Q$.
+
+In the concrete syntax, it should be written~:
+\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\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{\_}.
+
+\paragraph{Multiple dependent pattern matching}
+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 types 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_eval}
+Reset concat.
+\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 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}
+
+Even without real matching over the second term, this construction can be used to
+keep types linked.  If {\tt a} and {\tt b} are two {\tt listn} of the same length,
+by writing
+\begin{coq_eval}
+  Unset Printing Matching.
+\end{coq_eval}
+\begin{coq_example}
+Check (fun n (a b: listn n) => match a,b with
+ |niln,b0 => tt
+ |consn n' a y, bS => tt
+end).
+\end{coq_example}
+\begin{coq_eval}
+  Set Printing Matching.
+\end{coq_eval}
+
+I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
+
+% 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}
+
+\paragraph{Patterns in {\tt in}}
+\label{match-in-patterns}
+
+If the type of the matched term is more precise than an inductive applied to
+variables, arguments of the inductive in the {\tt in} branch can be more
+complicated patterns than a variable.
+
+Moreover, constructors whose type do not follow the same pattern will
+become impossible branches. In an impossible branch, you can answer
+anything but {\tt False\_rect unit} has the advantage to be subterm of
+anything. % ???
+
+To be concrete: the {\tt tail} function can be written:
+\begin{coq_example}
+Definition tail n (v: listn (S n)) :=
+  match v in listn (S m) return listn m with
+  | niln => False_rect unit
+  | consn n' a y => y
+  end.
+\end{coq_example}
+and {\tt tail n v} will be subterm of {\tt v}.
+
+\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{forall (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.
+
+\Rem you can only catch {\tt let} bindings in mode where you bind all variables and so you
+have to use @ syntax.
+
+\Rem this feature is incoherent with the fact that parameters cannot be caught and
+consequently is somehow hidden. For example, there is no mention of it in error messages.
+
+\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 incompatibility or the problem involves\\
+    dependencies}
+
+  There is a type mismatch between the different branches.
+  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:
-- 
cgit v1.2.3


From d0706a9aee2d43134e71bb02a5c7baabea7bb264 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 10:12:32 +0100
Subject: [Sphinx] Add chapter 17
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Thanks to Clément Pit-Claudel for porting this chapter.
---
 doc/sphinx/addendum/extended-pattern-matching.rst | 1336 +++++++++------------
 doc/sphinx/index.rst                              |    2 +
 2 files changed, 554 insertions(+), 784 deletions(-)

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 376ef031d..64d4eddf0 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -1,843 +1,611 @@
-\achapter{Extended pattern-matching}
-%HEVEA\cutname{cases.html}
-%BEGIN LATEX
-\defaultheaders
-%END LATEX
-\aauthor{Cristina Cornes and Hugo Herbelin}
-
-\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 co-inductive 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 (distinct) variables, it is
-called {\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt match}. On the opposite, if it is a variable $x$ or
-has the form $(c~\vec{p})$ with $p$ not only made of variables, the
-pattern is called {\em nested}.
+.. include:: ../replaces.rst
+
+.. _extendedpatternmatching:
+
+Extended pattern-matching
+=========================
+
+:Authors: Cristina Cornes and Hugo Herbelin
+
+.. TODO links to figures
+
+This section describes the full form of pattern-matching in |Coq| terms.
+
+.. |rhs| replace:: right hand side
+
+Patterns
+--------
+
+The full syntax of match is presented in Figures 1.1 and 1.2.
+Identifiers in patterns are either constructor names or variables. Any
+identifier that is not the constructor of an inductive or co-inductive
+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 x)`` where ``c`` is a constructor symbol and x
+is a linear vector of (distinct) variables, it is called *simple*: it
+is the kind of pattern recognized by the basic version of match. On
+the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not
+only made of variables, the pattern is called *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 pattern of the form {\pattern}{\tt |}{\pattern} is called
-disjunctive. A list of patterns separated with commas is also
-considered as a pattern and is called {\em multiple pattern}. However
-multiple patterns can only occur at the root of pattern-matching
-equations. Disjunctions of {\em multiple pattern} are allowed though.
-
-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.  Re-nesting
-of pattern is performed at printing time. An easy way to see the
-result of the expansion is to toggle off the nesting performed at
-printing (use here {\tt Set Printing Matching}), then 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}.
+that value. The pattern “``_``” (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
+:n:`(@pattern as @identifier)` are also accepted. This pattern matches the
+same values as ``pattern`` does and ``identifier`` is bound to the matched
+value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
+list of patterns separated with commas is also considered as a pattern
+and is called *multiple pattern*. However multiple patterns can only
+occur at the root of pattern-matching equations. Disjunctions of
+*multiple pattern* are allowed though.
+
+Since extended ``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. Re-nesting of
+pattern is performed at printing time. An easy way to see the result
+of the expansion is to toggle off the nesting performed at printing
+(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print`
+if the term is a constant, or using the command :cmd:`Check`.
+
+The extended ``match`` still accepts an optional *elimination predicate*
+given after the keyword ``return``. Given a pattern matching expression,
+if all the right-hand-sides of ``=>`` have the same
+type, then this type can be sometimes synthesized, and so we can omit
+the return part. Otherwise the predicate after return has to be
+provided, like for the basicmatch.
 
 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}
-
-\paragraph{Multiple patterns}
-
-Using multiple patterns in the definition of {\tt max} lets us write:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-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}
+.. coqtop:: in undo
+
+   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.
+
+Multiple patterns
+-----------------
+
+Using multiple patterns in the definition of max lets us write:
+
+.. coqtop:: in undo
+
+   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.
 
 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}
-
-\paragraph{Aliasing subpatterns}
-
-We can also use ``\texttt{as} {\ident}'' to associate a name to a
-sub-pattern:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-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}
-
-\paragraph{Nested patterns}
+to right. A match expression is generated **only** when there is at least
+one constructor in the column of patterns. E.g. the following example
+does not build a match expression.
+
+.. coqtop:: all
+
+   Check (fun x:nat => match x return nat with
+                       | y => y
+                       end).
+
+
+Aliasing subpatterns
+--------------------
+
+We can also use :n:`as @ident` to associate a name to a sub-pattern:
+
+.. coqtop:: in undo
+
+   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.
+
+Nested patterns
+---------------
 
 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}
+.. coqtop:: in
+
+   Fixpoint even (n:nat) : bool :=
+     match n with
+     | O => true
+     | S O => false
+     | S (S n') => even n'
+     end.
 
 This is compiled into:
 
-\begin{coq_example}
-Unset Printing Matching.
-Print even.
-\end{coq_example}
-\begin{coq_eval}
-Set Printing Matching.
-\end{coq_eval}
-
-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}
+.. coqtop:: all undo
+
+   Unset Printing Matching.
+   Print even.
+
+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 :g:`lef` that given two
+natural numbers yields :g:`true` if the first one is less or equal than the
+second one and :g:`false` otherwise. We can write it as follows:
+
+.. coqtop:: in undo
+
+   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.
 
 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_eval}
-Reset lef.
-\end{coq_eval}
-\begin{coq_example}
-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: "This clause is redundant."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check (fun x:nat =>
-         match x with
-         | O => true
-         | S _ => false
-         | x => true
-         end).
-\end{coq_example}
-
-\paragraph{Disjunctive patterns}
+the couple of values ``O O`` matches both. Thus, what is the result of the
+function on those values? To eliminate ambiguity we use the *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,O O
+is matched by the first pattern, and so :g:`(lef O O)` yields true.
+
+Another way to write this function is:
+
+.. coqtop:: in
+
+   Fixpoint lef (n m:nat) {struct m} : bool :=
+     match n, m with
+     | O, x => true
+     | S n, S m => lef n m
+     | _, _ => false
+     end.
+
+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:
+
+.. coqtop:: all
+
+   Fail Check (fun x:nat =>
+                 match x with
+                 | O => true
+                 | S _ => false
+                 | x => true
+                 end).
+
+
+Disjunctive patterns
+--------------------
 
 Multiple patterns that share the same right-hand-side can be
-factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
-{\tt max} can be rewritten as follows:
-
-\begin{coq_eval}
-Reset max.
-\end{coq_eval}
-\begin{coq_example}
-Fixpoint max (n m:nat) {struct m} : nat :=
-  match n, m with
-  | S n', S m' => S (max n' m')
-  | 0, p | p, 0 => p
-  end.
-\end{coq_example}
-
-Similarly, factorization of (non necessary multiple) patterns
-that share the same variables is possible by using the notation
-\nelist{\pattern}{\tt |}. Here is an example:
-
-\begin{coq_example}
-Definition filter_2_4 (n:nat) : nat :=
-  match n with
-  | 2 as m | 4 as m => m
-  | _ => 0
-  end.
-\end{coq_example}
+factorized using the notation :n:`{+| @mult_pattern}`. For
+instance, :g:`max` can be rewritten as follows:
+
+.. coqtop:: in undo
+
+   Fixpoint max (n m:nat) {struct m} : nat :=
+     match n, m with
+     | S n', S m' => S (max n' m')
+     | 0, p | p, 0 => p
+     end.
+
+Similarly, factorization of (non necessary multiple) patterns that
+share the same variables is possible by using the notation :n:`{+| @pattern}`.
+Here is an example:
+
+.. coqtop:: in
+
+   Definition filter_2_4 (n:nat) : nat :=
+     match n with
+     | 2 as m | 4 as m => m
+     | _ => 0
+     end.
+
 
 Here is another example using disjunctive subpatterns.
 
-\begin{coq_example}
-Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
-  match p with
-  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
-  | _ => (0,0)
-  end.
-\end{coq_example}
-
-\asection{About patterns of parametric types}
-\paragraph{Parameters in patterns}
-When matching objects of a parametric type, parameters do not bind in patterns.
-They must be substituted by ``\_''.
-Consider for example the type of 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}
+.. coqtop:: in
+
+   Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
+     match p with
+     | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
+     | _ => (0,0)
+     end.
+
+About patterns of parametric types
+----------------------------------
+
+Parameters in patterns
+~~~~~~~~~~~~~~~~~~~~~~
+
+When matching objects of a parametric type, parameters do not bind in
+patterns. They must be substituted by “``_``”. Consider for example the
+type of polymorphic lists:
+
+.. coqtop:: in
+
+   Inductive List (A:Set) : Set :=
+   | nil : List A
+   | cons : A -> List A -> List A.
+
+We can check the function *tail*:
 
+.. coqtop:: all
+
+   Check
+     (fun l:List nat =>
+        match l with
+        | nil _ => nil nat
+        | cons _ _ l' => l'
+        end).
 
 When we use parameters in patterns there is an error message:
-% Test failure: "The parameters do not bind in patterns."
-\begin{coq_eval}
-Set Printing Depth 50.
-\end{coq_eval}
-\begin{coq_example}
-Fail Check
-  (fun l:List nat =>
-     match l with
-     | nil A => nil nat
-     | cons A _ l' => l'
-     end).
-\end{coq_example}
-
-The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
-(off by default) removes parameters from constructors in patterns:
-\begin{coq_example}
-  Set Asymmetric Patterns.
-  Check (fun l:List nat =>
-    match l with
-    | nil => nil
-    | cons _ l' => l'
-    end)
-  Unset Asymmetric Patterns.
-\end{coq_example}
-
-\paragraph{Implicit arguments in patterns}
-By default, implicit arguments are omitted in patterns. So we write:
 
-\begin{coq_example}
-Arguments nil [A].
-Arguments cons [A] _ _.
-Check
-  (fun l:List nat =>
+.. coqtop:: all
+
+   Fail Check
+     (fun l:List nat =>
+        match l with
+        | nil A => nil nat
+        | cons A _ l' => l'
+        end).
+
+.. opt:: Asymmetric Patterns
+
+This option (off by default) removes parameters from constructors in patterns:
+
+.. coqtop:: all
+
+   Set Asymmetric Patterns.
+   Check (fun l:List nat =>
      match l with
      | nil => nil
      | cons _ l' => l'
-     end).
-\end{coq_example}
+     end)
+   Unset Asymmetric Patterns.
+
+Implicit arguments in patterns
+------------------------------
+
+By default, implicit arguments are omitted in patterns. So we write:
+
+.. coqtop:: all
+
+   Arguments nil [A].
+   Arguments cons [A] _ _.
+   Check
+     (fun l:List nat =>
+        match l with
+        | nil => nil
+        | cons _ l' => l'
+        end).
+
+But the possibility to use all the arguments is given by “``@``” implicit
+explicitations (as for terms 2.7.11).
+
+.. coqtop:: all
+
+   Check
+     (fun l:List nat =>
+        match l with
+        | @nil _ => @nil nat
+        | @cons _ _ l' => l'
+        end).
 
-But the possibility to use all the arguments is given by ``{\tt @}'' implicit
-explicitations (as for terms~\ref{Implicits-explicitation}).
 
-\begin{coq_example}
-Check
-  (fun l:List nat =>
+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 :g:`listn` of
+lists of a certain length:
+
+.. coqtop:: in reset
+
+   Inductive listn : nat -> Set :=
+   | niln : listn 0
+   | consn : forall n:nat, nat -> listn n -> listn (S n).
+
+
+Understanding dependencies in patterns
+--------------------------------------
+
+We can define the function length over :g:`listn` by:
+
+.. coqtop:: in
+
+   Definition length (n:nat) (l:listn n) := n.
+
+Just for illustrating pattern matching, we can define it by case
+analysis:
+
+.. coqtop:: in
+
+   Definition length (n:nat) (l:listn n) :=
      match l with
-     | @nil _ => @nil nat
-     | @cons _ _ 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:
-\label{listn}
-
-\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_eval}
-Reset length.
-\end{coq_eval}
-\begin{coq_example}
-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}
-\paragraph{Dependent pattern matching}
-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 {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where
-$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of
-the form~:
-{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots}
-  $y_s${\tt ) =>} $Q$.
-
-In the concrete syntax, it should be written~:
-\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\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{\_}.
-
-\paragraph{Multiple dependent pattern matching}
-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 types 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
+     | niln => 0
+     | consn n _ _ => S n
+     end.
+
+We can understand the meaning of this definition using the same
+notions of usual pattern matching.
+
+
+When the elimination predicate must be provided
+-----------------------------------------------
+
+Dependent pattern matching
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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 concat for listn is an example where the branches have
+different type and we need to provide the elimination predicate:
+
+.. coqtop:: in
+
+   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.
+
+The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`.
+In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr`
+are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`.
+
+In the concrete syntax, it should be written :
+``match m as x in (I _ … _ y1 … ys) return Q with … end``
+The variables which appear in the ``in`` and ``as`` clause are new and bounded
+in the property :g:`Q` in the return clause. The parameters of the
+inductive definitions should not be mentioned and are replaced by ``_``.
+
+Multiple dependent pattern matching
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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 types 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 as and in clause in order to introduce a dependent
+product.
+
+For example, an equivalent definition for :g:`concat` (even though the
 matching on the second term is trivial) would have been:
 
-\begin{coq_eval}
-Reset concat.
-\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 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}
-
-Even without real matching over the second term, this construction can be used to
-keep types linked.  If {\tt a} and {\tt b} are two {\tt listn} of the same length,
-by writing
-\begin{coq_eval}
-  Unset Printing Matching.
-\end{coq_eval}
-\begin{coq_example}
-Check (fun n (a b: listn n) => match a,b with
- |niln,b0 => tt
- |consn n' a y, bS => tt
-end).
-\end{coq_example}
-\begin{coq_eval}
-  Set Printing Matching.
-\end{coq_eval}
-
-I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}.
-
-% 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}
-
-\paragraph{Patterns in {\tt in}}
-\label{match-in-patterns}
-
-If the type of the matched term is more precise than an inductive applied to
-variables, arguments of the inductive in the {\tt in} branch can be more
-complicated patterns than a variable.
+.. coqtop:: in
+
+   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.
+
+Even without real matching over the second term, this construction can
+be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same
+length, by writing
+
+.. coqtop:: in
+
+   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.
+
+I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`.
+
+
+Patterns in ``in``
+~~~~~~~~~~~~~~~~~~
+
+If the type of the matched term is more precise than an inductive
+applied to variables, arguments of the inductive in the ``in`` branch can
+be more complicated patterns than a variable.
 
 Moreover, constructors whose type do not follow the same pattern will
 become impossible branches. In an impossible branch, you can answer
-anything but {\tt False\_rect unit} has the advantage to be subterm of
-anything. % ???
-
-To be concrete: the {\tt tail} function can be written:
-\begin{coq_example}
-Definition tail n (v: listn (S n)) :=
-  match v in listn (S m) return listn m with
-  | niln => False_rect unit
-  | consn n' a y => y
-  end.
-\end{coq_example}
-and {\tt tail n v} will be subterm of {\tt v}.
-
-\asection{Using pattern matching to write proofs}
+anything but False_rect unit has the advantage to be subterm of
+anything.
+
+To be concrete: the tail function can be written:
+
+.. coqtop:: in
+
+   Definition tail n (v: listn (S n)) :=
+     match v in listn (S m) return listn m with
+     | niln => False_rect unit
+     | consn n' a y => y
+     end.
+
+and :g:`tail n v` will be subterm of :g:`v`.
+
+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{forall (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.
-
-\Rem you can only catch {\tt let} bindings in mode where you bind all variables and so you
-have to use @ syntax.
-
-\Rem this feature is incoherent with the fact that parameters cannot be caught and
-consequently is somehow hidden. For example, there is no mention of it in error messages.
-
-\asection{Pattern-matching and coercions}
+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 match in given in Section
+8.2.3.
+
+For example, we can write the function :g:`buildlist` that given a natural
+number :g:`n` builds a list of length :g:`n` containing zeros as follows:
+
+.. coqtop:: in
+
+   Fixpoint buildlist (n:nat) : listn n :=
+     match n return listn n with
+     | O => niln
+     | S n => consn n 0 (buildlist n)
+     end.
+
+We can also use multiple patterns. Consider the following definition
+of the predicate less-equal :g:`Le`:
+
+.. coqtop:: in
+
+   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).
+
+We can use multiple patterns to write the proof of the lemma
+:g:`forall (n m:nat), (LE n m) \/ (LE m n)`:
+
+.. coqtop:: in
+
+   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.
+
+In the example of :g:`dec`, the first match is dependent while the second
+is not.
+
+The user can also use match in combination with the tactic :tacn:`refine` (see
+Section 8.2.3) to build incomplete proofs beginning with a match
+construction.
+
+
+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::
+
+   .. coqtop:: in
+
+      Inductive list : nat -> Set :=
+      | nil : list 0
+      | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)).
+
+   In the next example, the local definition is not caught.
+
+   .. coqtop:: in
+
+      Fixpoint length n (l:list n) {struct l} : nat :=
+        match l with
+        | nil => 0
+        | cons n l0 => S (length (2 * n) l0)
+        end.
+
+   But in this example, it is.
+
+   .. coqtop:: in
+
+      Fixpoint length' n (l:list n) {struct l} : nat :=
+        match l with
+        | nil => 0
+        | @cons _ m l0 => S (length' m l0)
+        end.
+
+.. note:: For a given matching clause, either none of the local
+          definitions or all of them can be caught.
+
+.. note:: You can only catch let bindings in mode where you bind all
+          variables and so you have to use ``@`` syntax.
+
+.. note:: this feature is incoherent with the fact that parameters
+          cannot be caught and consequently is somehow hidden. For example,
+          there is no mention of it in error messages.
+
+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:
+.. example::
+
+   .. coqtop:: in
+
+      Inductive I : Set :=
+        | C1 : nat -> I
+        | C2 : I -> I.
+
+      Coercion C1 : nat >-> I.
+
+   .. coqtop:: all
+
+      Check (fun x => match x with
+                      | C2 O => 0
+                      | _ => 0
+                      end).
 
-\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}
 
+When does the expansion strategy fail?
+--------------------------------------
 
-\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 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
+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
+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
+positions with the same name. E.g. to write ``(cons n O x) => e1`` and
+``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and
+``(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 incompatibility or the problem involves\\
-    dependencies}
-
-  There is a type mismatch between the different branches.
-  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:
+Here is a summary of the error messages corresponding to each
+situation:
+
+.. exn:: The constructor @ident expects @num arguments
+
+   The variable ident is bound several times in pattern termFound a constructor
+   of inductive type term while a constructor of term is expectedPatterns are
+   incorrect (because constructors are not applied to the correct number of the
+   arguments, because they are not linear or they are wrongly typed).
+
+.. exn:: Non exhaustive pattern-matching
+
+   The pattern matching is not exhaustive.
+
+.. exn:: The elimination predicate term should be of arity @num (for non \
+         dependent case) or @num (for dependent case)
+
+   The elimination predicate provided to match has not the expected arity.
+
+.. exn:: Unable to infer a match predicate
+         Either there is a type incompatibility or the problem involves dependencies
+
+   There is a type mismatch between the different branches. The user should
+   provide an elimination predicate.
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 4566db494..3cb58587c 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -43,6 +43,8 @@ Table of contents
 .. toctree::
    :caption: Addendum
 
+   addendum/extended-pattern-matching
+
 .. toctree::
    :caption: Reference
 
-- 
cgit v1.2.3


From d2f43c7519f85d84ff8548aadfb8da46450b3acd Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 10:36:03 +0100
Subject: [Sphinx] Move chapter 19 to new infrastructure

---
 Makefile.doc                                 |   2 +-
 doc/refman/CanonicalStructures.tex           | 383 ---------------------------
 doc/refman/Reference-Manual.tex              |   1 -
 doc/sphinx/addendum/canonical-structures.rst | 383 +++++++++++++++++++++++++++
 4 files changed, 384 insertions(+), 385 deletions(-)
 delete mode 100644 doc/refman/CanonicalStructures.tex
 create mode 100644 doc/sphinx/addendum/canonical-structures.rst

diff --git a/Makefile.doc b/Makefile.doc
index df1e2d3c4..8830c69ea 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
-  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
+  Cases.v.tex Coercion.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
   Setoid.v.tex Classes.v.tex Universes.v.tex \
   Misc.v.tex)
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
deleted file mode 100644
index 8961b0096..000000000
--- a/doc/refman/CanonicalStructures.tex
+++ /dev/null
@@ -1,383 +0,0 @@
-\achapter{Canonical Structures}
-%HEVEA\cutname{canonical-structures.html}
-\aauthor{Assia Mahboubi and Enrico Tassi}
-
-\label{CS-full}
-\index{Canonical Structures!presentation}
-
-\noindent This chapter explains the basics of Canonical Structure and how they can be used
-to overload notations and build a hierarchy of algebraic structures.
-The examples are taken from~\cite{CSwcu}.  We invite the interested reader
-to refer to this paper for all the details that are omitted here for brevity.
-The interested reader shall also find in~\cite{CSlessadhoc} a detailed
-description of another, complementary, use of Canonical Structures:
-advanced proof search.  This latter papers also presents many techniques one
-can employ to tune the inference of Canonical Structures.
-
-\section{Notation overloading}
-
-We build an infix notation $==$ for a comparison predicate.  Such notation
-will be overloaded, and its meaning will depend on the types of the terms
-that are compared.
-
-\begin{coq_eval}
-Require Import Arith.
-\end{coq_eval}
-
-\begin{coq_example}
-Module EQ.
-  Record class (T : Type) := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ the_cmp) := e in the_cmp.
-  Check op.
-  Arguments op {e} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-    Notation "x == y" := (op x y) (at level 70).
-  End theory.
-End EQ.
-\end{coq_example}
-
-We use Coq modules as name spaces.  This allows us to follow the same pattern
-and naming convention for the rest of the chapter.  The base name space
-contains the definitions of the algebraic structure.  To keep the example
-small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
-and characterizes terms on which a binary relation is defined, without
-requiring such relation to validate any property.
-The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
-will eventually contain lemmas holding on all the instances of the
-algebraic structure (in this case there are no lemmas).
-
-Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
-but we will not do that here.
-
-The following line tests that, when we assume a type \texttt{e} that is in the
-\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
-
-\begin{coq_example}
-Import EQ.theory.
-Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
-\end{coq_example}
-
-Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
-with a comparison relation.
-
-\begin{coq_example}
-Fail Check 3 == 3.
-Definition nat_eq (x y : nat) := nat_compare x y = Eq.
-Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
-Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
-Check 3 == 3.
-Eval compute in 3 == 4.
-\end{coq_example}
-
-This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
-also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
-relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
-can be read in the line declaring the canonical structure \texttt{nat\_EQty},
-where the first argument to \texttt{Pack} is the key and its second argument
-a group of canonical values associated to the key.  In this case we associate
-to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
-member).  The use of the projection \texttt{op} requires its argument to be in
-the class \texttt{EQ}, and uses such a member (function) to actually compare
-its arguments.
-
-Similarly, we could equip any other type with a comparison relation, and
-use the \texttt{==} notation on terms of this type.
-
-\subsection{Derived Canonical Structures}
-
-We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
-Here we show how to deal with type constructors, i.e. how to make the
-following example work:
-
-\begin{coq_example}
-Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). 
-\end{coq_example}
-
-The error message is telling that Coq has no idea on how to compare
-pairs of objects.  The following construction is telling Coq exactly how to do
-that.
-
-\begin{coq_example}
-Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
-  fst x == fst y /\ snd x == snd y.
-Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
-Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
-  EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
-Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
-Check forall n m : nat, (3,4) == (n,m).
-\end{coq_example}
-
-Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
-relation for pairs whenever it is able to build a comparison relation
-for each component of the pair.  The declaration associates to the key
-\texttt{*} (the type constructor of pairs) the canonical comparison relation
-\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
-being themselves in the \texttt{EQ} class.
-
-\section{Hierarchy of structures}
-
-To get to an interesting example we need another base class to be available.
-We choose the class of types that are equipped with an order relation,
-to which we associate the infix \texttt{<=} notation.
-
-\begin{coq_example}
-Module LE.
-  Record class T := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ f) := e in f.
-  Arguments op {_} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-  Notation "x <= y" := (op x y) (at level 70).
-  End theory.
-End LE.
-\end{coq_example}
-
-As before we register a canonical \texttt{LE} class for \texttt{nat}.
-
-\begin{coq_example}
-Import LE.theory.
-Definition nat_le x y := nat_compare x y <> Gt.
-Definition nat_LEcl : LE.class nat := LE.Class nat_le.
-Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
-\end{coq_example}
-
-And we enable Coq to relate pair of terms with \texttt{<=}.
-
-\begin{coq_example}
-Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
-  fst x <= fst y /\ snd x <= snd y.
-Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
-Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
-  LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
-Check (3,4,5) <= (3,4,5).
-\end{coq_example}
-
-At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
-like tuples of natural numbers, but we can't develop an algebraic
-theory over the types that are equipped with both relations.
-
-\begin{coq_example}
-Check 2 <= 3 /\ 2 == 2.
-Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
-Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
-\end{coq_example}
-
-We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
-
-\begin{coq_example}
-Module LEQ.
-  Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
-    Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
-  Record class T := Class {
-    EQ_class    : EQ.class T;
-    LE_class    : LE.class T;
-    extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
-  Structure type := _Pack { obj : Type; class_of : class obj }.
-  Arguments Mixin {e le} _.
-  Arguments Class {T} _ _ _.
-\end{coq_example}
-
-The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
-we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
-that the two relations we are combining are compatible.
-
-Unfortunately there is still an obstacle to developing the algebraic theory
-of this new class.
-
-\begin{coq_example}
-  Module theory.
-  Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
-\end{coq_example}
-
-The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
-a subclass relation.  In other words Coq does not see that an object
-of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
-
-The following two constructions tell Coq how to canonically build
-the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
-on the same type.
-
-\begin{coq_example}
-  Definition to_EQ (e : type) : EQ.type :=
-    EQ.Pack (obj e) (EQ_class _ (class_of e)).
-  Canonical Structure to_EQ.
-  Definition to_LE (e : type) : LE.type :=
-    LE.Pack (obj e) (LE_class _ (class_of e)).
-  Canonical Structure to_LE.
-\end{coq_example}
-We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
-\begin{coq_example}
-  Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
-   now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
-  Arguments lele_eq {e} x y _ _.
-  End theory.
-End LEQ.
-Import LEQ.theory.
-Check lele_eq.
-\end{coq_example}
-
-Of course one would like to apply results proved in the algebraic
-setting to any concrete instate of the algebraic structure.
-
-\begin{coq_example}
-Example test_algebraic (n m : nat) :  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-\end{coq_example}
-
-Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
-the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
-proofs are omitted for brevity.
-
-\begin{coq_example}
-Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-split.
-  unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-  case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ].
-  now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K.
-unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ].
-intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ].
-case (nat_compare_eq_iff m m); intros _ H1.
-now rewrite H1; auto; intro H2; discriminate H2.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
-Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-case n; case m; unfold EQ.op; unfold LE.op; simpl.
-intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ].
-  now split; apply lele_eq.
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1).
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2).
-intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4.
-now case H1; case H2; split; split.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
-\end{coq_example}
-
-The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
-type constructor \texttt{*}.  It also tests that they work as expected.
-
-Unfortunately, these declarations are very verbose.  In the following
-subsection we show how to make these declaration more compact.
-
-\begin{coq_example}
-Module Add_instance_attempt.
-  Canonical Structure nat_LEQty : LEQ.type :=
-    LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
-  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
-    LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
-      (LEQ.Class
-        (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
-        (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
-        (pair_LEQmx l1 l2)).
-  Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-  Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-End Add_instance_attempt.
-\end{coq_example}
-
-Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
-user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
-this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
-constructor preserves this property.  The combination of these two facts is a
-simple form of proof search that Coq performs automatically while inferring
-canonical structures.
-
-\subsection{Compact declaration of Canonical Structures}
-
-We need some infrastructure for that.
-
-\begin{coq_example*}
-Require Import Strings.String.
-\end{coq_example*}
-\begin{coq_example}
-Module infrastructure.
-  Inductive phantom {T : Type} (t : T) : Type := Phantom.
-  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
-    phantom t1 -> phantom t2.
-  Definition id {T} {t : T} (x : phantom t) := x.
-  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-    (at level 50, v ident, only parsing).
-  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-    (at level 50, v ident, only parsing).
-  Notation "'Error : t : s" := (unify _ t (Some s))
-    (at level 50, format "''Error'  :  t  :  s").
-  Open Scope string_scope.
-End infrastructure.
-\end{coq_example}
-
-To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one
-of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}.
-It should be read as: ``find a class e such that its objects have type T
-or fail with message "T is not an EQ.type"''.
-
-The other utilities are used to ask Coq to solve a specific unification
-problem, that will in turn require the inference of some canonical
-structures.  They are explained in mode details in~\cite{CSwcu}.
-
-We now have all we need to create a compact ``packager'' to declare
-instances of the \texttt{LEQ} class.
-
-\begin{coq_example}
-Import infrastructure.
-Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
-    [find e  | EQ.obj e ~ T       | "is not an EQ.type" ]
-    [find o  | LE.obj o ~ T       | "is not an LE.type" ]
-    [find ce | EQ.class_of e ~ ce ]
-    [find co | LE.class_of o ~ co ]
-    [find m  | m ~ m0             | "is not the right mixin" ]
-  LEQ._Pack T (LEQ.Class ce co m).
-Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
-\end{coq_example}
-
-The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
-the other pieces of the class \texttt{LEQ} and declares them as canonical values
-associated to the \texttt{T} key.  All in all, the only new piece of information
-we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
-for \texttt{T} and hence can be inferred by Coq.
-
-\texttt{Pack} is a notation, hence it is not type checked at the time of its
-declaration.  It will be type checked when it is used, an in that case
-\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
-pass to the 
-packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
-reader can refer to~\cite{CSwcu}. 
-
-The declaration of canonical instances can now be way more compact:
-
-\begin{coq_example}
-Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
-Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
-  Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
-\end{coq_example}
-
-Error messages are also quite intelligible (if one skips to the end of
-the message).
-
-\begin{coq_example}
-Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
-\end{coq_example}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 231742e56..dedead7f5 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -119,7 +119,6 @@ Options A and B of the licence are {\em not} elected.}
 \include{AddRefMan-pre}%
 \include{Cases.v}%
 \include{Coercion.v}%
-\include{CanonicalStructures.v}%
 \include{Classes.v}%
 \include{Omega.v}%
 \include{Micromega.v}
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
new file mode 100644
index 000000000..8961b0096
--- /dev/null
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -0,0 +1,383 @@
+\achapter{Canonical Structures}
+%HEVEA\cutname{canonical-structures.html}
+\aauthor{Assia Mahboubi and Enrico Tassi}
+
+\label{CS-full}
+\index{Canonical Structures!presentation}
+
+\noindent This chapter explains the basics of Canonical Structure and how they can be used
+to overload notations and build a hierarchy of algebraic structures.
+The examples are taken from~\cite{CSwcu}.  We invite the interested reader
+to refer to this paper for all the details that are omitted here for brevity.
+The interested reader shall also find in~\cite{CSlessadhoc} a detailed
+description of another, complementary, use of Canonical Structures:
+advanced proof search.  This latter papers also presents many techniques one
+can employ to tune the inference of Canonical Structures.
+
+\section{Notation overloading}
+
+We build an infix notation $==$ for a comparison predicate.  Such notation
+will be overloaded, and its meaning will depend on the types of the terms
+that are compared.
+
+\begin{coq_eval}
+Require Import Arith.
+\end{coq_eval}
+
+\begin{coq_example}
+Module EQ.
+  Record class (T : Type) := Class { cmp : T -> T -> Prop }.
+  Structure type := Pack { obj : Type; class_of : class obj }.
+  Definition op (e : type) : obj e -> obj e -> Prop :=
+    let 'Pack _ (Class _ the_cmp) := e in the_cmp.
+  Check op.
+  Arguments op {e} x y : simpl never.
+  Arguments Class {T} cmp.
+  Module theory.
+    Notation "x == y" := (op x y) (at level 70).
+  End theory.
+End EQ.
+\end{coq_example}
+
+We use Coq modules as name spaces.  This allows us to follow the same pattern
+and naming convention for the rest of the chapter.  The base name space
+contains the definitions of the algebraic structure.  To keep the example
+small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
+and characterizes terms on which a binary relation is defined, without
+requiring such relation to validate any property.
+The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
+will eventually contain lemmas holding on all the instances of the
+algebraic structure (in this case there are no lemmas).
+
+Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
+but we will not do that here.
+
+The following line tests that, when we assume a type \texttt{e} that is in the
+\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
+
+\begin{coq_example}
+Import EQ.theory.
+Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
+\end{coq_example}
+
+Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
+with a comparison relation.
+
+\begin{coq_example}
+Fail Check 3 == 3.
+Definition nat_eq (x y : nat) := nat_compare x y = Eq.
+Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
+Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
+Check 3 == 3.
+Eval compute in 3 == 4.
+\end{coq_example}
+
+This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
+also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
+relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
+can be read in the line declaring the canonical structure \texttt{nat\_EQty},
+where the first argument to \texttt{Pack} is the key and its second argument
+a group of canonical values associated to the key.  In this case we associate
+to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
+member).  The use of the projection \texttt{op} requires its argument to be in
+the class \texttt{EQ}, and uses such a member (function) to actually compare
+its arguments.
+
+Similarly, we could equip any other type with a comparison relation, and
+use the \texttt{==} notation on terms of this type.
+
+\subsection{Derived Canonical Structures}
+
+We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
+Here we show how to deal with type constructors, i.e. how to make the
+following example work:
+
+\begin{coq_example}
+Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). 
+\end{coq_example}
+
+The error message is telling that Coq has no idea on how to compare
+pairs of objects.  The following construction is telling Coq exactly how to do
+that.
+
+\begin{coq_example}
+Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
+  fst x == fst y /\ snd x == snd y.
+Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
+Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
+  EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
+Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
+Check forall n m : nat, (3,4) == (n,m).
+\end{coq_example}
+
+Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
+relation for pairs whenever it is able to build a comparison relation
+for each component of the pair.  The declaration associates to the key
+\texttt{*} (the type constructor of pairs) the canonical comparison relation
+\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
+being themselves in the \texttt{EQ} class.
+
+\section{Hierarchy of structures}
+
+To get to an interesting example we need another base class to be available.
+We choose the class of types that are equipped with an order relation,
+to which we associate the infix \texttt{<=} notation.
+
+\begin{coq_example}
+Module LE.
+  Record class T := Class { cmp : T -> T -> Prop }.
+  Structure type := Pack { obj : Type; class_of : class obj }.
+  Definition op (e : type) : obj e -> obj e -> Prop :=
+    let 'Pack _ (Class _ f) := e in f.
+  Arguments op {_} x y : simpl never.
+  Arguments Class {T} cmp.
+  Module theory.
+  Notation "x <= y" := (op x y) (at level 70).
+  End theory.
+End LE.
+\end{coq_example}
+
+As before we register a canonical \texttt{LE} class for \texttt{nat}.
+
+\begin{coq_example}
+Import LE.theory.
+Definition nat_le x y := nat_compare x y <> Gt.
+Definition nat_LEcl : LE.class nat := LE.Class nat_le.
+Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
+\end{coq_example}
+
+And we enable Coq to relate pair of terms with \texttt{<=}.
+
+\begin{coq_example}
+Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
+  fst x <= fst y /\ snd x <= snd y.
+Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
+Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
+  LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
+Check (3,4,5) <= (3,4,5).
+\end{coq_example}
+
+At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
+like tuples of natural numbers, but we can't develop an algebraic
+theory over the types that are equipped with both relations.
+
+\begin{coq_example}
+Check 2 <= 3 /\ 2 == 2.
+Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
+Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
+\end{coq_example}
+
+We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
+
+\begin{coq_example}
+Module LEQ.
+  Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
+    Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
+  Record class T := Class {
+    EQ_class    : EQ.class T;
+    LE_class    : LE.class T;
+    extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
+  Structure type := _Pack { obj : Type; class_of : class obj }.
+  Arguments Mixin {e le} _.
+  Arguments Class {T} _ _ _.
+\end{coq_example}
+
+The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
+we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
+that the two relations we are combining are compatible.
+
+Unfortunately there is still an obstacle to developing the algebraic theory
+of this new class.
+
+\begin{coq_example}
+  Module theory.
+  Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
+\end{coq_example}
+
+The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
+a subclass relation.  In other words Coq does not see that an object
+of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
+
+The following two constructions tell Coq how to canonically build
+the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
+on the same type.
+
+\begin{coq_example}
+  Definition to_EQ (e : type) : EQ.type :=
+    EQ.Pack (obj e) (EQ_class _ (class_of e)).
+  Canonical Structure to_EQ.
+  Definition to_LE (e : type) : LE.type :=
+    LE.Pack (obj e) (LE_class _ (class_of e)).
+  Canonical Structure to_LE.
+\end{coq_example}
+We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
+\begin{coq_example}
+  Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
+   now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
+  Arguments lele_eq {e} x y _ _.
+  End theory.
+End LEQ.
+Import LEQ.theory.
+Check lele_eq.
+\end{coq_example}
+
+Of course one would like to apply results proved in the algebraic
+setting to any concrete instate of the algebraic structure.
+
+\begin{coq_example}
+Example test_algebraic (n m : nat) :  n <= m -> m <= n -> n == m.
+ Fail apply (lele_eq n m). Abort.
+Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+  n <= m -> m <= n -> n == m.
+ Fail apply (lele_eq n m). Abort.
+\end{coq_example}
+
+Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
+the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
+proofs are omitted for brevity.
+
+\begin{coq_example}
+Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
+\end{coq_example}
+\begin{coq_eval}
+
+split.
+  unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
+  case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ].
+  now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K.
+unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
+case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ].
+intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ].
+case (nat_compare_eq_iff m m); intros _ H1.
+now rewrite H1; auto; intro H2; discriminate H2.
+Qed.
+\end{coq_eval}
+\begin{coq_example}
+Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
+Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+n <= m /\ m <= n <-> n == m.
+\end{coq_example}
+\begin{coq_eval}
+
+case n; case m; unfold EQ.op; unfold LE.op; simpl.
+intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ].
+  now split; apply lele_eq.
+case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1).
+case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2).
+intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4.
+now case H1; case H2; split; split.
+Qed.
+\end{coq_eval}
+\begin{coq_example}
+Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
+\end{coq_example}
+
+The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
+type constructor \texttt{*}.  It also tests that they work as expected.
+
+Unfortunately, these declarations are very verbose.  In the following
+subsection we show how to make these declaration more compact.
+
+\begin{coq_example}
+Module Add_instance_attempt.
+  Canonical Structure nat_LEQty : LEQ.type :=
+    LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
+  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
+    LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
+      (LEQ.Class
+        (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
+        (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
+        (pair_LEQmx l1 l2)).
+  Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+   now apply (lele_eq n m). Qed.
+  Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
+   now apply (lele_eq n m). Qed.
+End Add_instance_attempt.
+\end{coq_example}
+
+Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
+user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
+this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
+constructor preserves this property.  The combination of these two facts is a
+simple form of proof search that Coq performs automatically while inferring
+canonical structures.
+
+\subsection{Compact declaration of Canonical Structures}
+
+We need some infrastructure for that.
+
+\begin{coq_example*}
+Require Import Strings.String.
+\end{coq_example*}
+\begin{coq_example}
+Module infrastructure.
+  Inductive phantom {T : Type} (t : T) : Type := Phantom.
+  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
+    phantom t1 -> phantom t2.
+  Definition id {T} {t : T} (x : phantom t) := x.
+  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
+    (at level 50, v ident, only parsing).
+  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
+    (at level 50, v ident, only parsing).
+  Notation "'Error : t : s" := (unify _ t (Some s))
+    (at level 50, format "''Error'  :  t  :  s").
+  Open Scope string_scope.
+End infrastructure.
+\end{coq_example}
+
+To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one
+of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}.
+It should be read as: ``find a class e such that its objects have type T
+or fail with message "T is not an EQ.type"''.
+
+The other utilities are used to ask Coq to solve a specific unification
+problem, that will in turn require the inference of some canonical
+structures.  They are explained in mode details in~\cite{CSwcu}.
+
+We now have all we need to create a compact ``packager'' to declare
+instances of the \texttt{LEQ} class.
+
+\begin{coq_example}
+Import infrastructure.
+Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
+    [find e  | EQ.obj e ~ T       | "is not an EQ.type" ]
+    [find o  | LE.obj o ~ T       | "is not an LE.type" ]
+    [find ce | EQ.class_of e ~ ce ]
+    [find co | LE.class_of o ~ co ]
+    [find m  | m ~ m0             | "is not the right mixin" ]
+  LEQ._Pack T (LEQ.Class ce co m).
+Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
+\end{coq_example}
+
+The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
+the other pieces of the class \texttt{LEQ} and declares them as canonical values
+associated to the \texttt{T} key.  All in all, the only new piece of information
+we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
+for \texttt{T} and hence can be inferred by Coq.
+
+\texttt{Pack} is a notation, hence it is not type checked at the time of its
+declaration.  It will be type checked when it is used, an in that case
+\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
+pass to the 
+packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
+reader can refer to~\cite{CSwcu}. 
+
+The declaration of canonical instances can now be way more compact:
+
+\begin{coq_example}
+Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
+Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
+  Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
+\end{coq_example}
+
+Error messages are also quite intelligible (if one skips to the end of
+the message).
+
+\begin{coq_example}
+Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
+\end{coq_example}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3


From 8ab8818cdb90f5de436099153c56c552a36a04d7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 11:12:52 +0100
Subject: [Sphinx] Add chapter 19
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Thanks to Laurent Théry for porting this chapter.
---
 doc/sphinx/addendum/canonical-structures.rst | 766 ++++++++++++++-------------
 doc/sphinx/index.rst                         |   2 +
 2 files changed, 411 insertions(+), 357 deletions(-)

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 8961b0096..6843e9eaa 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -1,383 +1,435 @@
-\achapter{Canonical Structures}
-%HEVEA\cutname{canonical-structures.html}
-\aauthor{Assia Mahboubi and Enrico Tassi}
-
-\label{CS-full}
-\index{Canonical Structures!presentation}
-
-\noindent This chapter explains the basics of Canonical Structure and how they can be used
-to overload notations and build a hierarchy of algebraic structures.
-The examples are taken from~\cite{CSwcu}.  We invite the interested reader
-to refer to this paper for all the details that are omitted here for brevity.
-The interested reader shall also find in~\cite{CSlessadhoc} a detailed
-description of another, complementary, use of Canonical Structures:
-advanced proof search.  This latter papers also presents many techniques one
-can employ to tune the inference of Canonical Structures.
-
-\section{Notation overloading}
-
-We build an infix notation $==$ for a comparison predicate.  Such notation
-will be overloaded, and its meaning will depend on the types of the terms
-that are compared.
-
-\begin{coq_eval}
-Require Import Arith.
-\end{coq_eval}
-
-\begin{coq_example}
-Module EQ.
-  Record class (T : Type) := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ the_cmp) := e in the_cmp.
-  Check op.
-  Arguments op {e} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-    Notation "x == y" := (op x y) (at level 70).
-  End theory.
-End EQ.
-\end{coq_example}
-
-We use Coq modules as name spaces.  This allows us to follow the same pattern
-and naming convention for the rest of the chapter.  The base name space
-contains the definitions of the algebraic structure.  To keep the example
-small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
-and characterizes terms on which a binary relation is defined, without
-requiring such relation to validate any property.
-The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
-will eventually contain lemmas holding on all the instances of the
+.. include:: ../replaces.rst
+.. _canonicalstructures:
+
+Canonical Structures
+======================
+
+:Authors: Assia Mahboubi and Enrico Tassi
+
+This chapter explains the basics of Canonical Structure and how they can be used
+to overload notations and build a hierarchy of algebraic structures. The
+examples are taken from :cite:`CSwcu`. We invite the interested reader to refer
+to this paper for all the details that are omitted here for brevity. The
+interested reader shall also find in :cite:`CSlessadhoc` a detailed description
+of another, complementary, use of Canonical Structures: advanced proof search.
+This latter papers also presents many techniques one can employ to tune the
+inference of Canonical Structures.
+
+
+Notation overloading
+-------------------------
+
+We build an infix notation == for a comparison predicate. Such
+notation will be overloaded, and its meaning will depend on the types
+of the terms that are compared.
+
+.. coqtop:: all
+  
+  Module EQ.
+    Record class (T : Type) := Class { cmp : T -> T -> Prop }.
+    Structure type := Pack { obj : Type; class_of : class obj }.
+    Definition op (e : type) : obj e -> obj e -> Prop :=
+      let 'Pack _ (Class _ the_cmp) := e in the_cmp.
+    Check op.
+    Arguments op {e} x y : simpl never.
+    Arguments Class {T} cmp.
+    Module theory.
+      Notation "x == y" := (op x y) (at level 70).
+    End theory.
+  End EQ.
+
+We use Coq modules as name spaces. This allows us to follow the same
+pattern and naming convention for the rest of the chapter. The base
+name space contains the definitions of the algebraic structure. To
+keep the example small, the algebraic structure ``EQ.type`` we are
+defining is very simplistic, and characterizes terms on which a binary
+relation is defined, without requiring such relation to validate any
+property. The inner theory module contains the overloaded notation ``==``
+and will eventually contain lemmas holding on all the instances of the
 algebraic structure (in this case there are no lemmas).
 
-Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
-but we will not do that here.
-
-The following line tests that, when we assume a type \texttt{e} that is in the
-\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
-
-\begin{coq_example}
-Import EQ.theory.
-Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
-\end{coq_example}
-
-Still, no concrete type is in the \texttt{EQ} class.  We amend that by equipping \texttt{nat}
-with a comparison relation.
-
-\begin{coq_example}
-Fail Check 3 == 3.
-Definition nat_eq (x y : nat) := nat_compare x y = Eq.
-Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
-Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
-Check 3 == 3.
-Eval compute in 3 == 4.
-\end{coq_example}
-
-This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
-also that the infix relation was bound to the \texttt{nat\_eq} relation.  This
-relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}.  This
-can be read in the line declaring the canonical structure \texttt{nat\_EQty},
-where the first argument to \texttt{Pack} is the key and its second argument
-a group of canonical values associated to the key.  In this case we associate
-to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
-member).  The use of the projection \texttt{op} requires its argument to be in
-the class \texttt{EQ}, and uses such a member (function) to actually compare
-its arguments.
-
-Similarly, we could equip any other type with a comparison relation, and
-use the \texttt{==} notation on terms of this type.
-
-\subsection{Derived Canonical Structures}
-
-We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
-Here we show how to deal with type constructors, i.e. how to make the
-following example work:
-
-\begin{coq_example}
-Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). 
-\end{coq_example}
-
-The error message is telling that Coq has no idea on how to compare
-pairs of objects.  The following construction is telling Coq exactly how to do
-that.
-
-\begin{coq_example}
-Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
-  fst x == fst y /\ snd x == snd y.
-Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
-Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
-  EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
-Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
-Check forall n m : nat, (3,4) == (n,m).
-\end{coq_example}
-
-Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
+Note that in practice the user may want to declare ``EQ.obj`` as a
+coercion, but we will not do that here.
+
+The following line tests that, when we assume a type ``e`` that is in
+theEQ class, then we can relates two of its objects with ``==``.
+
+.. coqtop:: all
+  
+  Import EQ.theory.
+  Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
+
+Still, no concrete type is in the ``EQ`` class.
+
+.. coqtop:: all
+
+  Fail Check 3 == 3.
+
+We amend that by equipping ``nat`` with a comparison relation.
+
+.. coqtop:: all
+  
+   Definition nat_eq (x y : nat) := Nat.compare x y = Eq.
+   Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq.
+   Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl.
+   Check 3 == 3.
+   Eval compute in 3 == 4.
+
+This last test shows that |Coq| is now not only able to typecheck ``3 == 3``,
+but also that the infix relation was bound to the ``nat_eq`` relation.
+This relation is selected whenever ``==`` is used on terms of type nat.
+This can be read in the line declaring the canonical structure
+``nat_EQty``, where the first argument to ``Pack`` is the key and its second
+argument a group of canonical values associated to the key. In this
+case we associate to nat only one canonical value (since its class,
+``nat_EQcl`` has just one member). The use of the projection ``op`` requires
+its argument to be in the class ``EQ``, and uses such a member (function)
+to actually compare its arguments.
+
+Similarly, we could equip any other type with a comparison relation,
+and use the ``==`` notation on terms of this type.
+
+
+Derived Canonical Structures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show
+how to deal with type constructors, i.e. how to make the following
+example work:
+
+
+.. coqtop:: all
+
+  Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
+
+The error message is telling that |Coq| has no idea on how to compare
+pairs of objects. The following construction is telling Coq exactly
+how to do that.
+
+.. coqtop:: all
+
+  Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) :=
+    fst x == fst y /\ snd x == snd y.
+  
+  Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2).
+
+  Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type :=
+      EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).
+
+  Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b).
+
+  Check forall n m : nat, (3, 4) == (n, m).
+
+Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison
 relation for pairs whenever it is able to build a comparison relation
-for each component of the pair.  The declaration associates to the key
-\texttt{*} (the type constructor of pairs) the canonical comparison relation
-\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
-being themselves in the \texttt{EQ} class.
-
-\section{Hierarchy of structures}
-
-To get to an interesting example we need another base class to be available.
-We choose the class of types that are equipped with an order relation,
-to which we associate the infix \texttt{<=} notation.
-
-\begin{coq_example}
-Module LE.
-  Record class T := Class { cmp : T -> T -> Prop }.
-  Structure type := Pack { obj : Type; class_of : class obj }.
-  Definition op (e : type) : obj e -> obj e -> Prop :=
-    let 'Pack _ (Class _ f) := e in f.
-  Arguments op {_} x y : simpl never.
-  Arguments Class {T} cmp.
-  Module theory.
-  Notation "x <= y" := (op x y) (at level 70).
-  End theory.
-End LE.
-\end{coq_example}
-
-As before we register a canonical \texttt{LE} class for \texttt{nat}.
-
-\begin{coq_example}
-Import LE.theory.
-Definition nat_le x y := nat_compare x y <> Gt.
-Definition nat_LEcl : LE.class nat := LE.Class nat_le.
-Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
-\end{coq_example}
-
-And we enable Coq to relate pair of terms with \texttt{<=}.
-
-\begin{coq_example}
-Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
-  fst x <= fst y /\ snd x <= snd y.
-Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
-Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
-  LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
-Check (3,4,5) <= (3,4,5).
-\end{coq_example}
-
-At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
-like tuples of natural numbers, but we can't develop an algebraic
-theory over the types that are equipped with both relations.
-
-\begin{coq_example}
-Check 2 <= 3 /\ 2 == 2.
-Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
-Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
-\end{coq_example}
-
-We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
-
-\begin{coq_example}
-Module LEQ.
-  Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
-    Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
-  Record class T := Class {
-    EQ_class    : EQ.class T;
-    LE_class    : LE.class T;
-    extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
-  Structure type := _Pack { obj : Type; class_of : class obj }.
-  Arguments Mixin {e le} _.
-  Arguments Class {T} _ _ _.
-\end{coq_example}
-
-The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
-we are adding to \texttt{EQ} and \texttt{LE}.  In particular it contains the requirement
+for each component of the pair. The declaration associates to the key ``*``
+(the type constructor of pairs) the canonical comparison
+relation ``pair_eq`` whenever the type constructor ``*`` is applied to two
+types being themselves in the ``EQ`` class.
+
+Hierarchy of structures
+----------------------------
+
+To get to an interesting example we need another base class to be
+available. We choose the class of types that are equipped with an
+order relation, to which we associate the infix ``<=`` notation.
+
+.. coqtop:: all
+
+  Module LE.
+
+    Record class T := Class { cmp : T -> T -> Prop }.
+
+    Structure type := Pack { obj : Type; class_of : class obj }.
+
+    Definition op (e : type) : obj e -> obj e -> Prop :=
+      let 'Pack _ (Class _ f) := e in f.
+
+    Arguments op {_} x y : simpl never.
+
+    Arguments Class {T} cmp.
+  
+    Module theory.
+
+      Notation "x <= y" := (op x y) (at level 70).
+
+    End theory.
+
+  End LE.
+
+As before we register a canonical ``LE`` class for ``nat``.
+
+.. coqtop:: all
+
+  Import LE.theory.
+
+  Definition nat_le x y := Nat.compare x y <> Gt.
+
+  Definition nat_LEcl : LE.class nat := LE.Class nat_le.
+
+  Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
+
+And we enable |Coq| to relate pair of terms with ``<=``.
+
+.. coqtop:: all
+
+  Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
+     fst x <= fst y /\ snd x <= snd y.
+
+  Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2).
+
+  Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
+     LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2).
+
+  Check (3,4,5) <= (3,4,5).
+
+At the current stage we can use ``==`` and ``<=`` on concrete types, like
+tuples of natural numbers, but we can’t develop an algebraic theory
+over the types that are equipped with both relations.
+
+.. coqtop:: all
+
+  Check 2 <= 3 /\ 2 == 2.
+
+  Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
+
+  Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
+
+We need to define a new class that inherits from both ``EQ`` and ``LE``.
+
+
+.. coqtop:: all
+
+  Module LEQ.
+
+    Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) :=
+      Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }.
+    
+    Record class T := Class {
+                        EQ_class : EQ.class T;
+                        LE_class : LE.class T;
+                        extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
+
+    Structure type := _Pack { obj : Type; class_of : class obj }.
+
+    Arguments Mixin {e le} _.
+
+    Arguments Class {T} _ _ _.
+
+The mixin component of the ``LEQ`` class contains all the extra content we
+are adding to ``EQ`` and ``LE``. In particular it contains the requirement
 that the two relations we are combining are compatible.
 
-Unfortunately there is still an obstacle to developing the algebraic theory
-of this new class.
-
-\begin{coq_example}
-  Module theory.
-  Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
-\end{coq_example}
-
-The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
-a subclass relation.  In other words Coq does not see that an object
-of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
-
-The following two constructions tell Coq how to canonically build
-the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
-on the same type.
-
-\begin{coq_example}
-  Definition to_EQ (e : type) : EQ.type :=
-    EQ.Pack (obj e) (EQ_class _ (class_of e)).
-  Canonical Structure to_EQ.
-  Definition to_LE (e : type) : LE.type :=
-    LE.Pack (obj e) (LE_class _ (class_of e)).
-  Canonical Structure to_LE.
-\end{coq_example}
-We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
-\begin{coq_example}
-  Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
-   now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
-  Arguments lele_eq {e} x y _ _.
-  End theory.
-End LEQ.
-Import LEQ.theory.
-Check lele_eq.
-\end{coq_example}
+Unfortunately there is still an obstacle to developing the algebraic
+theory of this new class.
+
+.. coqtop:: all
+
+    Module theory.
+
+    Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
+
+
+The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by
+a subclass relation. In other words |Coq| does not see that an object of
+the ``LEQ`` class is also an object of the ``LE`` class.
+
+The following two constructions tell |Coq| how to canonically build the
+``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same
+type.
+
+.. coqtop:: all
+
+    Definition to_EQ (e : type) : EQ.type :=
+       EQ.Pack (obj e) (EQ_class _ (class_of e)).
+
+    Canonical Structure to_EQ.
+
+    Definition to_LE (e : type) : LE.type :=
+       LE.Pack (obj e) (LE_class _ (class_of e)).
+ 
+    Canonical Structure to_LE.
+
+We can now formulate out first theorem on the objects of the ``LEQ``
+structure.
+
+.. coqtop:: all
+
+     Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
+
+     now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. 
+
+     Qed.
+
+     Arguments lele_eq {e} x y _ _.
+
+     End theory.
+
+  End LEQ.
+
+  Import LEQ.theory.
+
+  Check lele_eq.
 
 Of course one would like to apply results proved in the algebraic
 setting to any concrete instate of the algebraic structure.
 
-\begin{coq_example}
-Example test_algebraic (n m : nat) :  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-  n <= m -> m <= n -> n == m.
- Fail apply (lele_eq n m). Abort.
-\end{coq_example}
-
-Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
-the type constructor \texttt{*} interacts with the \texttt{LEQ} class.  In the following
-proofs are omitted for brevity.
-
-\begin{coq_example}
-Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-split.
-  unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-  case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ].
-  now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K.
-unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq.
-case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ].
-intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ].
-case (nat_compare_eq_iff m m); intros _ H1.
-now rewrite H1; auto; intro H2; discriminate H2.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
-Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
-n <= m /\ m <= n <-> n == m.
-\end{coq_example}
-\begin{coq_eval}
-
-case n; case m; unfold EQ.op; unfold LE.op; simpl.
-intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ].
-  now split; apply lele_eq.
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1).
-case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2).
-intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4.
-now case H1; case H2; split; split.
-Qed.
-\end{coq_eval}
-\begin{coq_example}
-Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
-\end{coq_example}
-
-The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
-type constructor \texttt{*}.  It also tests that they work as expected.
-
-Unfortunately, these declarations are very verbose.  In the following
-subsection we show how to make these declaration more compact.
+.. coqtop:: all
 
-\begin{coq_example}
-Module Add_instance_attempt.
-  Canonical Structure nat_LEQty : LEQ.type :=
-    LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
-  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
-    LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
-      (LEQ.Class
-        (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
-        (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
-        (pair_LEQmx l1 l2)).
   Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-  Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
-   now apply (lele_eq n m). Qed.
-End Add_instance_attempt.
-\end{coq_example}
 
-Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
-user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}.  What the user provides is a proof of
-this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
-constructor preserves this property.  The combination of these two facts is a
-simple form of proof search that Coq performs automatically while inferring
-canonical structures.
+  Fail apply (lele_eq n m). 
+
+  Abort.
+
+  Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+       n <= m -> m <= n -> n == m.
+
+  Fail apply (lele_eq n m). 
+
+  Abort.
+
+Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and
+how the type constructor ``*`` interacts with the ``LEQ`` class. In the
+following proofs are omitted for brevity.
+
+.. coqtop:: all
+
+  Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m.
+
+  Admitted.
+
+  Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat.
+
+  Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
+     n <= m /\ m <= n <-> n == m.
+
+  Admitted.
+
+  Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
+
+The following script registers an ``LEQ`` class for ``nat`` and for the type
+constructor ``*``. It also tests that they work as expected.
+
+Unfortunately, these declarations are very verbose. In the following
+subsection we show how to make these declaration more compact.
 
-\subsection{Compact declaration of Canonical Structures}
+.. coqtop:: all
+
+  Module Add_instance_attempt.
+
+    Canonical Structure nat_LEQty : LEQ.type :=
+      LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx).
+
+    Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type :=
+      LEQ._Pack (LEQ.obj l1 * LEQ.obj l2)
+        (LEQ.Class
+           (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2)))
+           (LE.class_of (pair_LEty (to_LE l1) (to_LE l2)))
+           (pair_LEQmx l1 l2)).
+
+     Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m.
+
+     now apply (lele_eq n m). 
+
+     Qed.
+
+     Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m.
+
+     now apply (lele_eq n m). Qed.
+  
+  End Add_instance_attempt.
+
+Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by
+the user for ``n`` and m of type ``nat * nat``. What the user provides is a
+proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the
+pair constructor preserves this property. The combination of these two
+facts is a simple form of proof search that |Coq| performs automatically
+while inferring canonical structures.
+
+Compact declaration of Canonical Structures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 We need some infrastructure for that.
 
-\begin{coq_example*}
-Require Import Strings.String.
-\end{coq_example*}
-\begin{coq_example}
-Module infrastructure.
-  Inductive phantom {T : Type} (t : T) : Type := Phantom.
-  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
-    phantom t1 -> phantom t2.
-  Definition id {T} {t : T} (x : phantom t) := x.
-  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-    (at level 50, v ident, only parsing).
-  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-    (at level 50, v ident, only parsing).
-  Notation "'Error : t : s" := (unify _ t (Some s))
-    (at level 50, format "''Error'  :  t  :  s").
-  Open Scope string_scope.
-End infrastructure.
-\end{coq_example}
-
-To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one
-of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}.
-It should be read as: ``find a class e such that its objects have type T
-or fail with message "T is not an EQ.type"''.
-
-The other utilities are used to ask Coq to solve a specific unification
-problem, that will in turn require the inference of some canonical
-structures.  They are explained in mode details in~\cite{CSwcu}.
-
-We now have all we need to create a compact ``packager'' to declare
-instances of the \texttt{LEQ} class.
-
-\begin{coq_example}
-Import infrastructure.
-Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
-    [find e  | EQ.obj e ~ T       | "is not an EQ.type" ]
-    [find o  | LE.obj o ~ T       | "is not an LE.type" ]
+.. coqtop:: all
+
+  Require Import Strings.String.
+
+  Module infrastructure.
+
+    Inductive phantom {T : Type} (t : T) : Type := Phantom.
+
+    Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
+      phantom t1 -> phantom t2.
+
+    Definition id {T} {t : T} (x : phantom t) := x.
+
+    Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
+      (at level 50, v ident, only parsing).
+
+    Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
+      (at level 50, v ident, only parsing).
+
+    Notation "'Error : t : s" := (unify _ t (Some s))
+      (at level 50, format "''Error' : t : s").
+
+    Open Scope string_scope.
+
+  End infrastructure.
+
+To explain the notation ``[find v | t1 ~ t2]`` let us pick one of its
+instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be
+read as: “find a class e such that its objects have type T or fail
+with message "T is not an EQ.type"”.
+
+The other utilities are used to ask |Coq| to solve a specific unification
+problem, that will in turn require the inference of some canonical structures.
+They are explained in mode details in :cite:`CSwcu`.
+
+We now have all we need to create a compact “packager” to declare
+instances of the ``LEQ`` class.
+
+.. coqtop:: all
+
+  Import infrastructure.
+
+  Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
+    [find e | EQ.obj e ~ T | "is not an EQ.type" ]
+    [find o | LE.obj o ~ T | "is not an LE.type" ]
     [find ce | EQ.class_of e ~ ce ]
     [find co | LE.class_of o ~ co ]
-    [find m  | m ~ m0             | "is not the right mixin" ]
-  LEQ._Pack T (LEQ.Class ce co m).
-Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
-\end{coq_example}
-
-The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}.  It infers all
-the other pieces of the class \texttt{LEQ} and declares them as canonical values
-associated to the \texttt{T} key.  All in all, the only new piece of information
-we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
-for \texttt{T} and hence can be inferred by Coq.
-
-\texttt{Pack} is a notation, hence it is not type checked at the time of its
-declaration.  It will be type checked when it is used, an in that case
-\texttt{T} is going to be a concrete type.  The odd arguments \texttt{\_} and \texttt{id} we
-pass to the 
-packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference.  Again, for all the details the
-reader can refer to~\cite{CSwcu}. 
+    [find m | m ~ m0 | "is not the right mixin" ]
+    LEQ._Pack T (LEQ.Class ce co m).
+
+   Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
+
+The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all
+the other pieces of the class ``LEQ`` and declares them as canonical
+values associated to the ``T`` key. All in all, the only new piece of
+information we add in the ``LEQ`` class is the mixin, all the rest is
+already canonical for ``T`` and hence can be inferred by |Coq|.
+
+``Pack`` is a notation, hence it is not type checked at the time of its
+declaration. It will be type checked when it is used, an in that case ``T`` is
+going to be a concrete type. The odd arguments ``_`` and ``id`` we pass to the
+packager represent respectively the classes to be inferred (like ``e``, ``o``,
+etc) and a token (``id``) to force their inference. Again, for all the details
+the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-\begin{coq_example}
-Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
-Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
-  Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
-\end{coq_example}
+.. coqtop:: all
+
+  Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
+  
+  Canonical Structure pair_LEQty (l1 l2 : LEQ.type) :=
+     Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).
 
 Error messages are also quite intelligible (if one skips to the end of
 the message).
 
-\begin{coq_example}
-Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
-\end{coq_example}
+.. coqtop:: all
+
+  Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx.
 
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 4566db494..af54f0bd6 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -43,6 +43,8 @@ Table of contents
 .. toctree::
    :caption: Addendum
 
+   addendum/canonical-structures
+
 .. toctree::
    :caption: Reference
 
-- 
cgit v1.2.3


From 179aa79f50f4be2c9db3f818413f147f3ad7e2c4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 11:21:16 +0100
Subject: [Sphinx] Move chapter 21 to new infrastructure

---
 Makefile.doc                    |   2 +-
 doc/refman/Omega.tex            | 249 ----------------------------------------
 doc/refman/Reference-Manual.tex |   1 -
 doc/sphinx/addendum/omega.rst   | 249 ++++++++++++++++++++++++++++++++++++++++
 4 files changed, 250 insertions(+), 251 deletions(-)
 delete mode 100644 doc/refman/Omega.tex
 create mode 100644 doc/sphinx/addendum/omega.rst

diff --git a/Makefile.doc b/Makefile.doc
index df1e2d3c4..b46d93373 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -61,7 +61,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
   RefMan-pro.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
-  Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
+  Program.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
   Setoid.v.tex Classes.v.tex Universes.v.tex \
   Misc.v.tex)
 
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
deleted file mode 100644
index 82765da6e..000000000
--- a/doc/refman/Omega.tex
+++ /dev/null
@@ -1,249 +0,0 @@
-\achapter{Omega: a solver of quantifier-free problems in
-Presburger Arithmetic}
-%HEVEA\cutname{omega.html}
-\aauthor{Pierre Crégut}
-\label{OmegaChapter}
-
-\asection{Description of {\tt omega}}
-\tacindex{omega}
-\label{description}
-
-{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
-quantified formula made of equations and inequations. Equations may
-be specified either on the type \verb=nat= of natural numbers or on
-the type \verb=Z= of binary-encoded integer numbers. Formulas on
-\verb=nat= are automatically injected into \verb=Z=.  The procedure
-may use any hypothesis of the current proof session to solve the goal.
-
-Multiplication is handled by {\tt omega} but only goals where at
-least one of the two multiplicands of products is a constant are
-solvable. This is the restriction meant by ``Presburger arithmetic''.
-
-If the tactic cannot solve the goal, it fails with an error message.
-In any case, the computation eventually stops.
-
-\asubsection{Arithmetical goals recognized by {\tt omega}}
-
-{\tt omega} applied only to quantifier-free formulas built from the
-connectors
-
-\begin{quote}
-\verb=/\, \/, ~, ->=
-\end{quote}
-
-on atomic formulas. Atomic formulas are built from the predicates 
-
-\begin{quote}
-\verb!=, le, lt, gt, ge!
-\end{quote}
-
- on \verb=nat= or from the predicates
-
-\begin{quote}
-\verb!=, <, <=, >, >=!
-\end{quote}
-
- on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
-
-\begin{quote}
-\verb!plus, minus, mult, pred, S, O!
-\end{quote}
-
-and in expressions of type \verb=Z=, {\tt omega} recognizes 
-
-\begin{quote}
-\verb!+, -, *, Z.succ!, and constants.
-\end{quote}
-
-All expressions of type \verb=nat= or \verb=Z= not built on these
-operators are considered abstractly as if they
-were arbitrary variables of type \verb=nat= or \verb=Z=.
-
-\asubsection{Messages from {\tt omega}}
-\label{errors}
-
-When {\tt omega} does not solve the goal, one of the following errors
-is generated:
-
-\begin{ErrMsgs}
-
-\item \errindex{omega can't solve this system}
-
-  This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try {\tt intros} first; if it contains
-  existentials quantifiers too, {\tt omega} is not strong enough to solve your
-  goal). This may happen also if your goal contains arithmetical
-  operators unknown from {\tt omega}. Finally, your goal may be really
-  wrong!
-
-\item \errindex{omega: Not a quantifier-free goal}
-  
-  If your goal is universally quantified, you should first apply {\tt
-    intro} as many time as needed.
-
-\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
-
-\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
-  
-\item \errindex{omega: Can't solve a goal with proposition variables}
-
-\item \errindex{omega: Unrecognized proposition}
-
-\item \errindex{omega: Can't solve a goal with non-linear products}
-
-\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
-
-\end{ErrMsgs}
-
-%% This code is currently unplugged
-%% 
-% \asubsection{Control over the output}
-% There are some flags that can be set to get more information on the procedure
-
-% \begin{itemize}
-% \item \verb=Time= to get the time used by the procedure
-% \item \verb=System= to visualize the normalized systems.
-% \item \verb=Action= to visualize the actions performed by the OMEGA
-%      procedure (see \ref{technical}).
-% \end{itemize}
-
-% \comindex{Set omega Time}
-% \comindex{UnSet omega Time}
-% \comindex{Switch omega Time}
-% \comindex{Set omega System}
-% \comindex{UnSet omega System}
-% \comindex{Switch omega System}
-% \comindex{Set omega Action}
-% \comindex{UnSet omega Action}
-% \comindex{Switch omega Action}
-
-% Use {\tt Set omega {\rm\sl flag}} to set the flag
-% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
-% {\tt Switch omega {\rm\sl flag}} to toggle it.
-
-\section{Using {\tt omega}}
-
-The {\tt omega} tactic does not belong to the core system. It should be
-loaded by
-\begin{coq_example*}
-Require Import Omega.
-Open Scope Z_scope.
-\end{coq_example*}
-
-\example{}
-
-\begin{coq_example}
-Goal forall m n:Z, 1 + 2 * m <> 2 * n.
-intros; omega.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\example{}
-
-\begin{coq_example}
-Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
-intro; omega.
-\end{coq_example}
-
-% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
-
-\section{Options}
-
-\begin{quote}
-  \optindex{Stable Omega}
-  {\tt Unset Stable Omega}
-\end{quote}
-This deprecated option (on by default) is for compatibility with Coq
-pre 8.5. It resets internal name counters to make executions of
-{\tt omega} independent.
-
-\begin{quote}
-  \optindex{Omega UseLocalDefs}
-  {\tt Unset Omega UseLocalDefs}
-\end{quote}
-This option (on by default) allows {\tt omega} to use the bodies of
-local variables.
-
-\begin{quote}
-  \optindex{Omega System}
-  {\tt Set Omega System}
-  \optindex{Omega Action}
-  {\tt Set Omega Action}
-\end{quote}
-These two options (off by default) activate the printing of debug
-information.
-
-\asection{Technical data}
-\label{technical}
-
-\asubsection{Overview of the tactic}
-\begin{itemize}
-
-\item The goal is negated twice and the first negation is introduced as an
-     hypothesis.
-\item Hypothesis are decomposed in simple equations or inequations. Multiple
-     goals may result from this phase.
-\item Equations and inequations over \verb=nat= are translated over
-     \verb=Z=, multiple goals may result from the translation of
-     substraction.
-\item Equations and inequations are normalized.
-\item Goals are solved by the {\it OMEGA} decision procedure.
-\item The script of the solution is replayed.
-
-\end{itemize}
-
-\asubsection{Overview of the {\it OMEGA} decision procedure}
-
-The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
-a small subset of the decision procedure presented in
-
-\begin{quote}
-  "The Omega Test: a fast and practical integer programming
-algorithm for dependence analysis", William Pugh, Communication of the
-ACM , 1992, p 102-114.
-\end{quote}
-
-Here is an overview, look at the original paper for more information.
-
-\begin{itemize}
-
-\item Equations and inequations are normalized by division by the GCD of their
-     coefficients.
-\item Equations are eliminated, using the Banerjee test to get a coefficient 
-     equal to one.
-\item Note that each inequation defines a half space in the space of real value
-     of the variables.
-   \item Inequations are solved by projecting on the hyperspace
-     defined by cancelling one of the variable.  They are partitioned
-     according to the sign of the coefficient of the eliminated
-     variable. Pairs of inequations from different classes define a
-     new edge in the projection.
-   \item Redundant inequations are eliminated or merged in new
-     equations that can be eliminated by the Banerjee test.
-\item The last two steps are iterated until a contradiction is reached
-     (success) or there is no more variable to eliminate (failure).
-
-\end{itemize}
-
-It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure (dark shadow) are not implemented, so the 
-decision procedure is only partial.
-
-\asection{Bugs}
-
-\begin{itemize}
-\item The simplification procedure is very dumb and this results in
-  many redundant cases to explore.
-
-\item Much too slow.
-
-\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}.
-
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 231742e56..afc1b9c57 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -121,7 +121,6 @@ Options A and B of the licence are {\em not} elected.}
 \include{Coercion.v}%
 \include{CanonicalStructures.v}%
 \include{Classes.v}%
-\include{Omega.v}%
 \include{Micromega.v}
 \include{Extraction.v}%
 \include{Program.v}%
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
new file mode 100644
index 000000000..82765da6e
--- /dev/null
+++ b/doc/sphinx/addendum/omega.rst
@@ -0,0 +1,249 @@
+\achapter{Omega: a solver of quantifier-free problems in
+Presburger Arithmetic}
+%HEVEA\cutname{omega.html}
+\aauthor{Pierre Crégut}
+\label{OmegaChapter}
+
+\asection{Description of {\tt omega}}
+\tacindex{omega}
+\label{description}
+
+{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
+quantified formula made of equations and inequations. Equations may
+be specified either on the type \verb=nat= of natural numbers or on
+the type \verb=Z= of binary-encoded integer numbers. Formulas on
+\verb=nat= are automatically injected into \verb=Z=.  The procedure
+may use any hypothesis of the current proof session to solve the goal.
+
+Multiplication is handled by {\tt omega} but only goals where at
+least one of the two multiplicands of products is a constant are
+solvable. This is the restriction meant by ``Presburger arithmetic''.
+
+If the tactic cannot solve the goal, it fails with an error message.
+In any case, the computation eventually stops.
+
+\asubsection{Arithmetical goals recognized by {\tt omega}}
+
+{\tt omega} applied only to quantifier-free formulas built from the
+connectors
+
+\begin{quote}
+\verb=/\, \/, ~, ->=
+\end{quote}
+
+on atomic formulas. Atomic formulas are built from the predicates 
+
+\begin{quote}
+\verb!=, le, lt, gt, ge!
+\end{quote}
+
+ on \verb=nat= or from the predicates
+
+\begin{quote}
+\verb!=, <, <=, >, >=!
+\end{quote}
+
+ on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
+
+\begin{quote}
+\verb!plus, minus, mult, pred, S, O!
+\end{quote}
+
+and in expressions of type \verb=Z=, {\tt omega} recognizes 
+
+\begin{quote}
+\verb!+, -, *, Z.succ!, and constants.
+\end{quote}
+
+All expressions of type \verb=nat= or \verb=Z= not built on these
+operators are considered abstractly as if they
+were arbitrary variables of type \verb=nat= or \verb=Z=.
+
+\asubsection{Messages from {\tt omega}}
+\label{errors}
+
+When {\tt omega} does not solve the goal, one of the following errors
+is generated:
+
+\begin{ErrMsgs}
+
+\item \errindex{omega can't solve this system}
+
+  This may happen if your goal is not quantifier-free (if it is
+  universally quantified, try {\tt intros} first; if it contains
+  existentials quantifiers too, {\tt omega} is not strong enough to solve your
+  goal). This may happen also if your goal contains arithmetical
+  operators unknown from {\tt omega}. Finally, your goal may be really
+  wrong!
+
+\item \errindex{omega: Not a quantifier-free goal}
+  
+  If your goal is universally quantified, you should first apply {\tt
+    intro} as many time as needed.
+
+\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
+
+\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
+  
+\item \errindex{omega: Can't solve a goal with proposition variables}
+
+\item \errindex{omega: Unrecognized proposition}
+
+\item \errindex{omega: Can't solve a goal with non-linear products}
+
+\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
+
+\end{ErrMsgs}
+
+%% This code is currently unplugged
+%% 
+% \asubsection{Control over the output}
+% There are some flags that can be set to get more information on the procedure
+
+% \begin{itemize}
+% \item \verb=Time= to get the time used by the procedure
+% \item \verb=System= to visualize the normalized systems.
+% \item \verb=Action= to visualize the actions performed by the OMEGA
+%      procedure (see \ref{technical}).
+% \end{itemize}
+
+% \comindex{Set omega Time}
+% \comindex{UnSet omega Time}
+% \comindex{Switch omega Time}
+% \comindex{Set omega System}
+% \comindex{UnSet omega System}
+% \comindex{Switch omega System}
+% \comindex{Set omega Action}
+% \comindex{UnSet omega Action}
+% \comindex{Switch omega Action}
+
+% Use {\tt Set omega {\rm\sl flag}} to set the flag
+% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
+% {\tt Switch omega {\rm\sl flag}} to toggle it.
+
+\section{Using {\tt omega}}
+
+The {\tt omega} tactic does not belong to the core system. It should be
+loaded by
+\begin{coq_example*}
+Require Import Omega.
+Open Scope Z_scope.
+\end{coq_example*}
+
+\example{}
+
+\begin{coq_example}
+Goal forall m n:Z, 1 + 2 * m <> 2 * n.
+intros; omega.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\example{}
+
+\begin{coq_example}
+Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
+intro; omega.
+\end{coq_example}
+
+% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
+
+\section{Options}
+
+\begin{quote}
+  \optindex{Stable Omega}
+  {\tt Unset Stable Omega}
+\end{quote}
+This deprecated option (on by default) is for compatibility with Coq
+pre 8.5. It resets internal name counters to make executions of
+{\tt omega} independent.
+
+\begin{quote}
+  \optindex{Omega UseLocalDefs}
+  {\tt Unset Omega UseLocalDefs}
+\end{quote}
+This option (on by default) allows {\tt omega} to use the bodies of
+local variables.
+
+\begin{quote}
+  \optindex{Omega System}
+  {\tt Set Omega System}
+  \optindex{Omega Action}
+  {\tt Set Omega Action}
+\end{quote}
+These two options (off by default) activate the printing of debug
+information.
+
+\asection{Technical data}
+\label{technical}
+
+\asubsection{Overview of the tactic}
+\begin{itemize}
+
+\item The goal is negated twice and the first negation is introduced as an
+     hypothesis.
+\item Hypothesis are decomposed in simple equations or inequations. Multiple
+     goals may result from this phase.
+\item Equations and inequations over \verb=nat= are translated over
+     \verb=Z=, multiple goals may result from the translation of
+     substraction.
+\item Equations and inequations are normalized.
+\item Goals are solved by the {\it OMEGA} decision procedure.
+\item The script of the solution is replayed.
+
+\end{itemize}
+
+\asubsection{Overview of the {\it OMEGA} decision procedure}
+
+The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
+a small subset of the decision procedure presented in
+
+\begin{quote}
+  "The Omega Test: a fast and practical integer programming
+algorithm for dependence analysis", William Pugh, Communication of the
+ACM , 1992, p 102-114.
+\end{quote}
+
+Here is an overview, look at the original paper for more information.
+
+\begin{itemize}
+
+\item Equations and inequations are normalized by division by the GCD of their
+     coefficients.
+\item Equations are eliminated, using the Banerjee test to get a coefficient 
+     equal to one.
+\item Note that each inequation defines a half space in the space of real value
+     of the variables.
+   \item Inequations are solved by projecting on the hyperspace
+     defined by cancelling one of the variable.  They are partitioned
+     according to the sign of the coefficient of the eliminated
+     variable. Pairs of inequations from different classes define a
+     new edge in the projection.
+   \item Redundant inequations are eliminated or merged in new
+     equations that can be eliminated by the Banerjee test.
+\item The last two steps are iterated until a contradiction is reached
+     (success) or there is no more variable to eliminate (failure).
+
+\end{itemize}
+
+It may happen that there is a real solution and no integer one. The last
+steps of the Omega procedure (dark shadow) are not implemented, so the 
+decision procedure is only partial.
+
+\asection{Bugs}
+
+\begin{itemize}
+\item The simplification procedure is very dumb and this results in
+  many redundant cases to explore.
+
+\item Much too slow.
+
+\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}.
+
+\end{itemize}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3


From 109106cbd36d169de839066da4f3265f291bc924 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 22 Mar 2018 11:28:07 +0100
Subject: [Sphinx] Add chapter 21

Thanks to Pierre Letouzey for porting this chapter.
---
 doc/sphinx/addendum/omega.rst | 331 +++++++++++++++++-------------------------
 doc/sphinx/biblio.bib         |   2 +-
 doc/sphinx/index.rst          |   2 +
 3 files changed, 136 insertions(+), 199 deletions(-)

diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 82765da6e..20e40c550 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -1,249 +1,184 @@
-\achapter{Omega: a solver of quantifier-free problems in
-Presburger Arithmetic}
-%HEVEA\cutname{omega.html}
-\aauthor{Pierre Crégut}
-\label{OmegaChapter}
+.. _omega:
 
-\asection{Description of {\tt omega}}
-\tacindex{omega}
-\label{description}
+Omega: a solver for quantifier-free problems in Presburger Arithmetic
+=====================================================================
 
-{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
+:Author: Pierre Crégut
+
+Description of ``omega``
+------------------------
+
+This tactic does not need any parameter:
+
+.. tacn:: omega
+
+``omega`` solves a goal in Presburger arithmetic, i.e. a universally
 quantified formula made of equations and inequations. Equations may
-be specified either on the type \verb=nat= of natural numbers or on
-the type \verb=Z= of binary-encoded integer numbers. Formulas on
-\verb=nat= are automatically injected into \verb=Z=.  The procedure
+be specified either on the type ``nat`` of natural numbers or on
+the type ``Z`` of binary-encoded integer numbers. Formulas on
+``nat`` are automatically injected into ``Z``.  The procedure
 may use any hypothesis of the current proof session to solve the goal.
 
-Multiplication is handled by {\tt omega} but only goals where at
+Multiplication is handled by ``omega`` but only goals where at
 least one of the two multiplicands of products is a constant are
-solvable. This is the restriction meant by ``Presburger arithmetic''.
+solvable. This is the restriction meant by "Presburger arithmetic".
 
 If the tactic cannot solve the goal, it fails with an error message.
 In any case, the computation eventually stops.
 
-\asubsection{Arithmetical goals recognized by {\tt omega}}
+Arithmetical goals recognized by ``omega``
+------------------------------------------
 
-{\tt omega} applied only to quantifier-free formulas built from the
-connectors
+``omega`` applied only to quantifier-free formulas built from the
+connectors::
 
-\begin{quote}
-\verb=/\, \/, ~, ->=
-\end{quote}
+   /\  \/  ~  ->
 
-on atomic formulas. Atomic formulas are built from the predicates 
+on atomic formulas. Atomic formulas are built from the predicates::
 
-\begin{quote}
-\verb!=, le, lt, gt, ge!
-\end{quote}
+   =  <  <=  >  >=
 
- on \verb=nat= or from the predicates
+on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes::
 
-\begin{quote}
-\verb!=, <, <=, >, >=!
-\end{quote}
+   +  -  *  S  O  pred
 
- on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes 
+and in expressions of type ``Z``, ``omega`` recognizes numeral constants and::
 
-\begin{quote}
-\verb!plus, minus, mult, pred, S, O!
-\end{quote}
+   +  -  *  Z.succ Z.pred
 
-and in expressions of type \verb=Z=, {\tt omega} recognizes 
-
-\begin{quote}
-\verb!+, -, *, Z.succ!, and constants.
-\end{quote}
-
-All expressions of type \verb=nat= or \verb=Z= not built on these
+All expressions of type ``nat`` or ``Z`` not built on these
 operators are considered abstractly as if they
-were arbitrary variables of type \verb=nat= or \verb=Z=.
+were arbitrary variables of type ``nat`` or ``Z``.
 
-\asubsection{Messages from {\tt omega}}
-\label{errors}
+Messages from ``omega``
+-----------------------
 
-When {\tt omega} does not solve the goal, one of the following errors
+When ``omega`` does not solve the goal, one of the following errors
 is generated:
 
-\begin{ErrMsgs}
-
-\item \errindex{omega can't solve this system}
+.. exn:: omega can't solve this system
 
   This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try {\tt intros} first; if it contains
-  existentials quantifiers too, {\tt omega} is not strong enough to solve your
+  universally quantified, try ``intros`` first; if it contains
+  existentials quantifiers too, ``omega`` is not strong enough to solve your
   goal). This may happen also if your goal contains arithmetical
-  operators unknown from {\tt omega}. Finally, your goal may be really
+  operators unknown from ``omega``. Finally, your goal may be really
   wrong!
 
-\item \errindex{omega: Not a quantifier-free goal}
-  
-  If your goal is universally quantified, you should first apply {\tt
-    intro} as many time as needed.
+.. exn:: omega: Not a quantifier-free goal
+
+  If your goal is universally quantified, you should first apply
+  ``intro`` as many time as needed.
 
-\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
+.. exn:: omega: Unrecognized predicate or connective: @ident
 
-\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
-  
-\item \errindex{omega: Can't solve a goal with proposition variables}
+.. exn:: omega: Unrecognized atomic proposition: ...
 
-\item \errindex{omega: Unrecognized proposition}
+.. exn:: omega: Can't solve a goal with proposition variables
 
-\item \errindex{omega: Can't solve a goal with non-linear products}
+.. exn:: omega: Unrecognized proposition
 
-\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
+.. exn:: omega: Can't solve a goal with non-linear products
 
-\end{ErrMsgs}
+.. exn:: omega: Can't solve a goal with equality on type ...
 
-%% This code is currently unplugged
-%% 
-% \asubsection{Control over the output}
-% There are some flags that can be set to get more information on the procedure
 
-% \begin{itemize}
-% \item \verb=Time= to get the time used by the procedure
-% \item \verb=System= to visualize the normalized systems.
-% \item \verb=Action= to visualize the actions performed by the OMEGA
-%      procedure (see \ref{technical}).
-% \end{itemize}
+Using ``omega``
+---------------
 
-% \comindex{Set omega Time}
-% \comindex{UnSet omega Time}
-% \comindex{Switch omega Time}
-% \comindex{Set omega System}
-% \comindex{UnSet omega System}
-% \comindex{Switch omega System}
-% \comindex{Set omega Action}
-% \comindex{UnSet omega Action}
-% \comindex{Switch omega Action}
+The ``omega`` tactic does not belong to the core system. It should be
+loaded by
 
-% Use {\tt Set omega {\rm\sl flag}} to set the flag
-% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
-% {\tt Switch omega {\rm\sl flag}} to toggle it.
+.. coqtop:: in
 
-\section{Using {\tt omega}}
+   Require Import Omega.
+
+.. example::
+
+  .. coqtop:: all
+
+     Require Import Omega.
+
+     Open Scope Z_scope.
+
+     Goal forall m n:Z, 1 + 2 * m <> 2 * n.
+     intros; omega.
+     Abort.
+
+     Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
+     intro; omega.
+     Abort.
 
-The {\tt omega} tactic does not belong to the core system. It should be
-loaded by
-\begin{coq_example*}
-Require Import Omega.
-Open Scope Z_scope.
-\end{coq_example*}
-
-\example{}
-
-\begin{coq_example}
-Goal forall m n:Z, 1 + 2 * m <> 2 * n.
-intros; omega.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\example{}
-
-\begin{coq_example}
-Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
-intro; omega.
-\end{coq_example}
-
-% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
-
-\section{Options}
-
-\begin{quote}
-  \optindex{Stable Omega}
-  {\tt Unset Stable Omega}
-\end{quote}
-This deprecated option (on by default) is for compatibility with Coq
-pre 8.5. It resets internal name counters to make executions of
-{\tt omega} independent.
-
-\begin{quote}
-  \optindex{Omega UseLocalDefs}
-  {\tt Unset Omega UseLocalDefs}
-\end{quote}
-This option (on by default) allows {\tt omega} to use the bodies of
-local variables.
-
-\begin{quote}
-  \optindex{Omega System}
-  {\tt Set Omega System}
-  \optindex{Omega Action}
-  {\tt Set Omega Action}
-\end{quote}
-These two options (off by default) activate the printing of debug
-information.
-
-\asection{Technical data}
-\label{technical}
-
-\asubsection{Overview of the tactic}
-\begin{itemize}
-
-\item The goal is negated twice and the first negation is introduced as an
-     hypothesis.
-\item Hypothesis are decomposed in simple equations or inequations. Multiple
-     goals may result from this phase.
-\item Equations and inequations over \verb=nat= are translated over
-     \verb=Z=, multiple goals may result from the translation of
-     substraction.
-\item Equations and inequations are normalized.
-\item Goals are solved by the {\it OMEGA} decision procedure.
-\item The script of the solution is replayed.
-
-\end{itemize}
-
-\asubsection{Overview of the {\it OMEGA} decision procedure}
-
-The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
-a small subset of the decision procedure presented in
-
-\begin{quote}
-  "The Omega Test: a fast and practical integer programming
-algorithm for dependence analysis", William Pugh, Communication of the
-ACM , 1992, p 102-114.
-\end{quote}
 
+Options
+-------
+
+.. opt:: Stable Omega
+
+This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
+resets internal name counters to make executions of ``omega`` independent.
+
+.. opt:: Omega UseLocalDefs
+
+This option (on by default) allows ``omega`` to use the bodies of local
+variables.
+
+.. opt:: Omega System
+
+This option (off by default) activate the printing of debug information
+
+.. opt:: Omega Action
+
+This option (off by default) activate the printing of debug information
+
+Technical data
+--------------
+
+Overview of the tactic
+~~~~~~~~~~~~~~~~~~~~~~
+
+ * The goal is negated twice and the first negation is introduced as an hypothesis.
+ * Hypothesis are decomposed in simple equations or inequations. Multiple
+   goals may result from this phase.
+ * Equations and inequations over ``nat`` are translated over
+   ``Z``, multiple goals may result from the translation of substraction.
+ * Equations and inequations are normalized.
+ * Goals are solved by the OMEGA decision procedure.
+ * The script of the solution is replayed.
+
+Overview of the OMEGA decision procedure
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The OMEGA decision procedure involved in the ``omega`` tactic uses
+a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
 Here is an overview, look at the original paper for more information.
 
-\begin{itemize}
-
-\item Equations and inequations are normalized by division by the GCD of their
-     coefficients.
-\item Equations are eliminated, using the Banerjee test to get a coefficient 
-     equal to one.
-\item Note that each inequation defines a half space in the space of real value
-     of the variables.
-   \item Inequations are solved by projecting on the hyperspace
-     defined by cancelling one of the variable.  They are partitioned
-     according to the sign of the coefficient of the eliminated
-     variable. Pairs of inequations from different classes define a
-     new edge in the projection.
-   \item Redundant inequations are eliminated or merged in new
-     equations that can be eliminated by the Banerjee test.
-\item The last two steps are iterated until a contradiction is reached
-     (success) or there is no more variable to eliminate (failure).
-
-\end{itemize}
+ * Equations and inequations are normalized by division by the GCD of their
+   coefficients.
+ * Equations are eliminated, using the Banerjee test to get a coefficient
+   equal to one.
+ * Note that each inequation defines a half space in the space of real value
+   of the variables.
+ * Inequations are solved by projecting on the hyperspace
+   defined by cancelling one of the variable.  They are partitioned
+   according to the sign of the coefficient of the eliminated
+   variable. Pairs of inequations from different classes define a
+   new edge in the projection.
+ * Redundant inequations are eliminated or merged in new
+   equations that can be eliminated by the Banerjee test.
+ * The last two steps are iterated until a contradiction is reached
+   (success) or there is no more variable to eliminate (failure).
 
 It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure (dark shadow) are not implemented, so the 
+steps of the Omega procedure (dark shadow) are not implemented, so the
 decision procedure is only partial.
 
-\asection{Bugs}
-
-\begin{itemize}
-\item The simplification procedure is very dumb and this results in
-  many redundant cases to explore.
-
-\item Much too slow.
+Bugs
+----
 
-\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}.
+ * The simplification procedure is very dumb and this results in
+   many redundant cases to explore.
 
-\end{itemize}
+ * Much too slow.
 
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
+ * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/.
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 4a9bd6c1a..247f32103 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -1312,7 +1312,7 @@ Languages},
   year        = {1994}
 }
 
-@article{ TheOmegaPaper,
+@article{TheOmegaPaper,
     author = "W. Pugh",
     title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
     journal = "Communication of the ACM",
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 4566db494..f1fbd2b7d 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -43,6 +43,8 @@ Table of contents
 .. toctree::
    :caption: Addendum
 
+   addendum/omega
+
 .. toctree::
    :caption: Reference
 
-- 
cgit v1.2.3