1 files changed, 418 insertions, 0 deletions
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
new file mode 100644
index 00000000..707ee824
--- /dev/null
+++ b/doc/refman/RefMan-sch.tex
@@ -0,0 +1,418 @@
+\chapter{Proof schemes}
+
+\section{Generation of induction principles with {\tt Scheme}}
+\label{Scheme}
+\index{Schemes}
+\comindex{Scheme}
+
+The {\tt Scheme} command is a high-level tool for generating
+automatically (possibly mutual) induction principles for given types
+and sorts.  Its syntax follows the schema:
+\begin{quote}
+{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\\
+        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
+        {\sort$_m$}}
+\end{quote}
+where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
+identifiers belonging to the same package of mutual inductive
+definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
+to be mutually recursive definitions. Each term {\ident$_i$} proves a
+general principle of mutual induction for objects in type {\term$_i$}.
+
+\begin{Variants}
+\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
+    with\\
+    \mbox{}\hspace{0.1cm} \dots\ \\
+    with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
+    {\sort$_m$}}
+
+  Same as before but defines a non-dependent elimination principle more
+  natural in case of inductively defined relations.
+
+\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
+
+  Tries to generate a boolean equality and a proof of the
+  decidability of the usual equality. If \ident$_i$ involves
+  some other inductive types, their equality has to be defined first.
+
+\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\\
+        with Induction for {\ident$_m$} Sort
+        {\sort$_m$}}
+
+  If you do not provide the name of the schemes, they will be automatically
+  computed from the sorts involved (works also with Minimality).
+
+\end{Variants}
+\label{Scheme-examples}
+
+\firstexample
+\example{Induction scheme for \texttt{tree} and \texttt{forest}}
+
+The definition of principle of mutual induction for {\tt tree} and
+{\tt forest} over the sort {\tt Set} is defined by the command:
+
+\begin{coq_eval}
+Reset Initial.
+Variables A B : Set.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
+
+Scheme tree_forest_rec := Induction for tree Sort Set
+  with forest_tree_rec := Induction for forest Sort Set.
+\end{coq_example*}
+
+You may now look at the type of {\tt tree\_forest\_rec}:
+
+\begin{coq_example}
+Check tree_forest_rec.
+\end{coq_example}
+
+This principle involves two different predicates for {\tt trees} and
+{\tt forests}; it also has three premises each one corresponding to a
+constructor of one of the inductive definitions.
+
+The principle {\tt forest\_tree\_rec} shares exactly the same
+premises, only the conclusion now refers to the property of forests.
+
+\begin{coq_example}
+Check forest_tree_rec.
+\end{coq_example}
+
+\example{Predicates {\tt odd} and {\tt even} on naturals}
+
+Let {\tt odd} and {\tt even} be inductively defined as:
+
+% Reset Initial.
+\begin{coq_eval}
+Open Scope nat_scope.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive odd : nat -> Prop :=
+    oddS : forall n:nat, even n -> odd (S n)
+with even : nat -> Prop :=
+  | evenO : even 0
+  | evenS : forall n:nat, odd n -> even (S n).
+\end{coq_example*}
+
+The following command generates a powerful elimination
+principle:
+
+\begin{coq_example}
+Scheme odd_even := Minimality for   odd Sort Prop
+  with even_odd := Minimality for even Sort Prop.
+\end{coq_example}
+
+The type of {\tt odd\_even} for instance will be:
+
+\begin{coq_example}
+Check odd_even.
+\end{coq_example}
+
+The type of {\tt even\_odd} shares the same premises but the
+conclusion is {\tt (n:nat)(even n)->(Q n)}.
+
+\subsection{Automatic declaration of schemes}
+\comindex{Set Equality Schemes}
+\comindex{Set Elimination Schemes}
+
+It is possible to deactivate the automatic declaration of the induction
+ principles when defining a new inductive type  with the
+ {\tt Unset Elimination Schemes} command. It may be
+reactivated at any time with {\tt Set Elimination Schemes}.
+\\
+
+You can also activate the automatic declaration of those boolean equalities
+(see the second variant of {\tt Scheme})  with the {\tt Set Equality Schemes}
+ command. However you have to be careful with this option since
+\Coq~ may now reject well-defined inductive types because it cannot compute
+a boolean equality for them.
+
+\subsection{\tt Combined Scheme}
+\label{CombinedScheme}
+\comindex{Combined Scheme}
+
+The {\tt Combined Scheme} command is a tool for combining
+induction principles generated by the {\tt Scheme} command.
+Its syntax follows the schema :
+\begin{quote}
+{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}
+\end{quote}
+where
+\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
+the same package of mutual inductive principle definitions. This command
+generates {\ident$_0$} to be the conjunction of the principles: it is
+built from the common premises of the principles and concluded by the
+conjunction of their conclusions.
+
+\Example
+We can define the induction principles for trees and forests using:
+\begin{coq_example}
+Scheme tree_forest_ind := Induction for tree Sort Prop
+  with forest_tree_ind := Induction for forest Sort Prop.
+\end{coq_example}
+
+Then we can build the combined induction principle which gives the
+conjunction of the conclusions of each individual principle:
+\begin{coq_example}
+Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
+\end{coq_example}
+
+The type of {\tt tree\_forest\_mutrec} will be:
+\begin{coq_example}
+Check tree_forest_mutind.
+\end{coq_example}
+
+\section{Generation of induction principles with {\tt Functional Scheme}}
+\label{FunScheme}
+\comindex{Functional Scheme}
+
+The {\tt Functional Scheme} command is a high-level experimental
+tool for generating automatically induction principles
+corresponding to (possibly mutually recursive) functions.  Its
+syntax follows the schema:
+\begin{quote}
+{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\ \\
+        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
+        {\sort$_m$}}
+\end{quote}
+where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
+names (they must be in the same order as when they were defined).
+This command generates the induction principles
+\ident$_1$\dots\ident$_m$, following the recursive structure and case
+analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
+
+\Rem
+There is a difference between obtaining an induction scheme by using
+\texttt{Functional Scheme} on a function defined by \texttt{Function}
+or not. Indeed \texttt{Function} generally produces smaller
+principles, closer to the definition written by the user.
+
+\firstexample
+\example{Induction scheme for \texttt{div2}}
+\label{FunScheme-examples}
+
+We define the function \texttt{div2} as follows:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Require Import Arith.
+Fixpoint div2 (n:nat) : nat :=
+  match n with
+  | O => 0
+  | S O => 0
+  | S (S n') => S (div2 n')
+  end.
+\end{coq_example*}
+
+The definition of a principle of induction corresponding to the
+recursive structure of \texttt{div2} is defined by the command:
+
+\begin{coq_example}
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
+\end{coq_example}
+
+You may now look at the type of {\tt div2\_ind}:
+
+\begin{coq_example}
+Check div2_ind.
+\end{coq_example}
+
+We can now prove the following lemma using this principle:
+
+\begin{coq_example*}
+Lemma div2_le' : forall n:nat, div2 n <= n.
+intro n.
+ pattern n , (div2 n).
+\end{coq_example*}
+
+\begin{coq_example}
+apply div2_ind; intros.
+\end{coq_example}
+
+\begin{coq_example*}
+auto with arith.
+auto with arith.
+simpl; auto with arith.
+Qed.
+\end{coq_example*}
+
+We can use directly the \texttt{functional induction}
+(\ref{FunInduction}) tactic instead of the pattern/apply trick:
+\tacindex{functional induction}
+
+\begin{coq_example*}
+Reset div2_le'.
+Lemma div2_le : forall n:nat, div2 n <= n.
+intro n.
+\end{coq_example*}
+
+\begin{coq_example}
+functional induction (div2 n).
+\end{coq_example}
+
+\begin{coq_example*}
+auto with arith.
+auto with arith.
+auto with arith.
+Qed.
+\end{coq_example*}
+
+\Rem There is a difference between obtaining an induction scheme for a
+function by using \texttt{Function} (see Section~\ref{Function}) and by
+using \texttt{Functional Scheme} after a normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
+
+
+\example{Induction scheme for \texttt{tree\_size}}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+We define trees by the following mutual inductive type:
+
+\begin{coq_example*}
+Variable A : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | empty : forest
+  | cons : tree -> forest -> forest.
+\end{coq_example*}
+
+We define the function \texttt{tree\_size} that computes the size
+of a tree or a forest. Note that we use \texttt{Function} which
+generally produces better principles.
+
+\begin{coq_example*}
+Function tree_size (t:tree) : nat :=
+  match t with
+  | node A f => S (forest_size f)
+  end
+ with forest_size (f:forest) : nat :=
+  match f with
+  | empty => 0
+  | cons t f' => (tree_size t + forest_size f')
+  end.
+\end{coq_example*}
+
+\Rem \texttt{Function} generates itself non mutual induction
+principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
+
+\begin{coq_example}
+Check tree_size_ind.
+\end{coq_example}
+
+The definition of mutual induction principles following the recursive
+structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
+by the command:
+
+\begin{coq_example*}
+Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+with forest_size_ind2 := Induction for forest_size Sort Prop.
+\end{coq_example*}
+
+You may now look at the type of {\tt tree\_size\_ind2}:
+
+\begin{coq_example}
+Check tree_size_ind2.
+\end{coq_example}
+
+\section{Generation of inversion principles with \tt Derive Inversion}
+\label{Derive-Inversion}
+\comindex{Derive Inversion}
+
+The syntax of {\tt Derive Inversion} follows the schema:
+\begin{quote}
+{\tt Derive Inversion {\ident} with forall
+  $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort}
+\end{quote}
+
+This command generates an inversion principle for the
+\texttt{inversion \dots\ using} tactic.
+\tacindex{inversion \dots\ using}
+Let $I$ be an inductive predicate and $\vec{x}$ the variables
+occurring in $\vec{t}$. This command generates and stocks the
+inversion lemma for the sort \sort~ corresponding to the instance
+$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
+global} environment. When applied, it is equivalent to having inverted
+the instance with the tactic {\tt inversion}.
+
+\begin{Variants}
+\item \texttt{Derive Inversion\_clear {\ident} with forall
+  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
+  \comindex{Derive Inversion\_clear}
+  When applied, it is equivalent to having
+  inverted the instance with the tactic \texttt{inversion}
+  replaced by the tactic \texttt{inversion\_clear}.
+\item \texttt{Derive Dependent Inversion {\ident} with forall
+  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
+  \comindex{Derive Dependent Inversion}
+  When applied, it is equivalent to having
+  inverted the instance with the tactic \texttt{dependent inversion}.
+\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall
+  $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\
+  \comindex{Derive Dependent Inversion\_clear}
+  When applied, it is equivalent to having
+  inverted the instance with the tactic \texttt{dependent inversion\_clear}.
+\end{Variants}
+
+\Example
+
+Let us consider the relation \texttt{Le} over natural numbers and the
+following variable:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive Le : nat -> nat -> Set :=
+  | LeO : forall n:nat, Le 0 n
+  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
+Variable P : nat -> nat -> Prop.
+\end{coq_example*}
+
+To generate the inversion lemma for the instance
+\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do:
+
+\begin{coq_example*}
+Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
+\end{coq_example*}
+
+\begin{coq_example}
+Check leminv.
+\end{coq_example}
+
+Then we can use the proven inversion lemma:
+
+\begin{coq_eval}
+Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+intros.
+\end{coq_eval}
+
+\begin{coq_example}
+Show.
+\end{coq_example}
+
+\begin{coq_example}
+inversion H using leminv.
+\end{coq_example}
+