\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}