Merge PR #6993: Sphinx doc chapter 13

2 files changed, 375 insertions, 0 deletions

diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index f3b852d454..443e5c10fa 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -30,6 +30,7 @@ Table of contents
    :caption: User extensions
 
    user-extensions/syntax-extensions
+   user-extensions/proof-schemes
 
 .. toctree::
    :caption: Practical tools
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
new file mode 100644
index 0000000000..583b73e53d
--- /dev/null
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -0,0 +1,374 @@
+.. _proofschemes:
+
+Proof schemes
+===============
+
+Generation of induction principles with ``Scheme``
+--------------------------------------------------------
+
+The ``Scheme`` command is a high-level tool for generating automatically
+(possibly mutual) induction principles for given types and sorts. Its
+syntax follows the schema:
+
+.. cmd:: Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+
+where each `ident'ᵢ` is a different inductive type identifier 
+belonging to the same package of mutual inductive definitions. This
+command generates the `identᵢ`s to be mutually recursive
+definitions. Each term `identᵢ` proves a general principle of mutual
+induction for objects in type `identᵢ`.
+
+.. cmdv:: Scheme ident := Minimality for ident' Sort sort {* with ident := Minimality for ident' Sort sort}
+
+  Same as before but defines a non-dependent elimination principle more
+  natural in case of inductively defined relations.
+
+.. cmdv:: Scheme Equality for ident
+
+   Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
+   involves some other inductive types, their equality has to be defined first.
+
+.. cmdv:: Scheme Induction for ident Sort sort {* with Induction for ident Sort sort}
+
+   If you do not provide the name of the schemes, they will be automatically computed from the
+   sorts involved (works also with Minimality).
+
+.. example::
+
+   Induction scheme for tree and forest.
+
+   The definition of principle of mutual induction for tree and forest
+   over the sort Set is defined by the command:
+
+    .. coqtop:: none
+
+     Axiom A : Set.	       
+     Axiom B : Set.	       
+   
+    .. coqtop:: all
+
+     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.
+
+  You may now look at the type of tree_forest_rec:
+
+  .. coqtop:: all
+
+    Check tree_forest_rec.
+
+  This principle involves two different predicates for trees andforests;
+  it also has three premises each one corresponding to a constructor of
+  one of the inductive definitions.
+
+  The principle `forest_tree_rec` shares exactly the same premises, only
+  the conclusion now refers to the property of forests.
+
+.. example::
+
+  Predicates odd and even on naturals.
+
+  Let odd and even be inductively defined as:
+
+   .. coqtop:: all
+
+      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).
+
+  The following command generates a powerful elimination principle:
+
+   .. coqtop:: all
+
+    Scheme odd_even := Minimality for odd Sort Prop
+    with even_odd := Minimality for even Sort Prop.
+
+  The type of odd_even for instance will be:
+
+  .. coqtop:: all
+
+    Check odd_even.
+
+  The type of `even_odd` shares the same premises but the conclusion is
+  `(n:nat)(even n)->(P0 n)`.
+
+
+Automatic declaration of schemes
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+It is possible to deactivate the automatic declaration of the
+induction principles when defining a new inductive type with the
+``Unset Elimination Schemes`` command. It may be reactivated at any time with
+``Set Elimination Schemes``.
+
+The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record``
+(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction
+principles. It can be activated with the command
+``Set Nonrecursive Elimination Schemes``. It can be deactivated again with
+``Unset Nonrecursive Elimination Schemes``.
+
+In addition, the ``Case Analysis Schemes`` flag governs the generation of
+case analysis lemmas for inductive types, i.e. corresponding to the
+pattern-matching term alone and without fixpoint.
+You can also activate the automatic declaration of those Boolean
+equalities (see the second variant of ``Scheme``) with respectively the
+commands ``Set Boolean Equality Schemes`` and ``Set Decidable Equality
+Schemes``. 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.
+
+.. opt:: Rewriting Schemes
+
+   This flag governs generation of equality-related schemes such as congruence.
+
+Combined Scheme
+~~~~~~~~~~~~~~~~~~~~~~
+
+The ``Combined Scheme`` command is a tool for combining induction
+principles generated by the ``Scheme command``. Its syntax follows the
+schema :
+
+.. cmd:: Combined Scheme ident from {+, ident}
+
+where each identᵢ after the ``from`` is a different inductive principle that must
+belong to the same package of mutual inductive principle definitions.
+This command generates the leftmost `ident` 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:
+
+  .. coqtop:: all
+
+    Scheme tree_forest_ind := Induction for tree Sort Prop
+    with forest_tree_ind := Induction for forest Sort Prop.
+
+  Then we can build the combined induction principle which gives the
+  conjunction of the conclusions of each individual principle:
+
+  .. coqtop:: all
+
+    Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.
+
+  The type of tree_forest_mutrec will be:
+
+  .. coqtop:: all
+
+    Check tree_forest_mutind.
+
+Generation of induction principles with ``Functional`` ``Scheme``
+-----------------------------------------------------------------
+
+The ``Functional Scheme`` command is a high-level experimental tool for
+generating automatically induction principles corresponding to
+(possibly mutually recursive) functions. First, it must be made
+available via ``Require Import FunInd``. Its syntax then follows the
+schema:
+
+.. cmd:: Functional Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort}
+
+where each `ident'ᵢ` is a different mutually defined function
+name (the names must be in the same order as when they were defined). This
+command generates the induction principle for each `identᵢ`, following
+the recursive structure and case analyses of the corresponding function 
+identᵢ’.
+
+Remark: There is a difference between obtaining an induction scheme by
+using ``Functional Scheme`` on a function defined by ``Function`` or not.
+Indeed, ``Function`` generally produces smaller principles, closer to the
+definition written by the user.
+
+.. example:: 
+
+  Induction scheme for div2.
+
+  We define the function div2 as follows:
+
+  .. coqtop:: all
+
+   Require Import FunInd.
+   Require Import Arith.
+
+   Fixpoint div2 (n:nat) : nat :=
+   match n with
+   | O => 0
+   | S O => 0
+   | S (S n') => S (div2 n')
+   end.
+
+  The definition of a principle of induction corresponding to the
+  recursive structure of `div2` is defined by the command:
+
+  .. coqtop:: all
+
+    Functional Scheme div2_ind := Induction for div2 Sort Prop.
+
+  You may now look at the type of div2_ind:
+
+  .. coqtop:: all
+
+    Check div2_ind.
+
+  We can now prove the following lemma using this principle:
+
+  .. coqtop:: all
+
+    Lemma div2_le' : forall n:nat, div2 n <= n.
+    intro n.
+    pattern n, (div2 n).
+    apply div2_ind; intros.
+    auto with arith.
+    auto with arith.
+    simpl; auto with arith.
+    Qed.
+
+  We can use directly the functional induction (:ref:`TODO-8.5.5`) tactic instead
+  of the pattern/apply trick:
+
+  .. coqtop:: all
+
+    Reset div2_le'.
+
+    Lemma div2_le : forall n:nat, div2 n <= n.
+    intro n.
+    functional induction (div2 n).
+    auto with arith.
+    auto with arith.
+    auto with arith.
+    Qed.
+
+  Remark: There is a difference between obtaining an induction scheme
+  for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using
+  ``Functional Scheme`` after a normal definition using ``Fixpoint`` or
+  ``Definition``. See :ref:`advanced-recursive-functions` for details.
+
+.. example::
+
+  Induction scheme for tree_size.
+
+  We define trees by the following mutual inductive type:
+
+  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+   
+  .. coqtop:: reset all
+
+     Axiom A : Set.
+     
+     Inductive tree : Set :=
+     node : A -> forest -> tree
+     with forest : Set :=
+     | empty : forest
+     | cons : tree -> forest -> forest.
+
+  We define the function tree_size that computes the size of a tree or a
+  forest. Note that we use ``Function`` which generally produces better
+  principles.
+
+  .. coqtop:: all
+
+    Require Import FunInd.
+
+    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.
+
+  Remark: Function generates itself non mutual induction principles
+  tree_size_ind and forest_size_ind:
+
+  .. coqtop:: all
+
+    Check tree_size_ind.
+
+  The definition of mutual induction principles following the recursive
+  structure of `tree_size` and `forest_size` is defined by the command:
+
+  .. coqtop:: all
+
+    Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+    with forest_size_ind2 := Induction for forest_size Sort Prop.
+
+  You may now look at the type of `tree_size_ind2`:
+
+  .. coqtop:: all
+
+    Check tree_size_ind2.
+     
+Generation of inversion principles with ``Derive`` ``Inversion``
+-----------------------------------------------------------------
+
+The syntax of ``Derive`` ``Inversion`` follows the schema:
+
+.. cmd:: Derive Inversion ident with forall (x : T), I t Sort sort
+
+This command generates an inversion principle for the `inversion … using` 
+tactic. Let `I` be an inductive predicate and `x` the variables occurring
+in t. This command generates and stocks the inversion lemma for the
+sort `sort` corresponding to the instance `∀ (x:T), I t` with the name
+`ident` in the global environment. When applied, it is equivalent to
+having inverted the instance with the tactic `inversion`.
+
+.. cmdv:: Derive Inversion_clear ident with forall (x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance with the
+   tactic inversion replaced by the tactic `inversion_clear`.
+
+.. cmdv:: Derive Dependent Inversion ident with forall (x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance with
+   the tactic `dependent inversion`.
+
+.. cmdv:: Derive Dependent Inversion_clear ident with forall(x:T), I t Sort sort
+
+   When applied, it is equivalent to having inverted the instance
+   with the tactic `dependent inversion_clear`.
+
+.. example::
+
+  Let us consider the relation `Le` over natural numbers and the following
+  variable:
+
+  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+  
+  .. coqtop:: all
+
+    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).
+
+    Axiom P : nat -> nat -> Prop.
+
+  To generate the inversion lemma for the instance `(Le (S n) m)` and the
+  sort `Prop`, we do:
+
+  .. coqtop:: all
+
+    Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
+    Check leminv.
+
+  Then we can use the proven inversion lemma:
+
+  .. the original LaTeX did not have any Coq code to setup the goal
+
+  .. coqtop:: none
+
+    Goal forall (n m : nat) (H : Le (S n) m), P n m.			  
+    intros.
+  
+  .. coqtop:: all
+
+    Show.
+
+    inversion H using leminv.