Merge PR #7634: Extend combined scheme to Schemes in Type

2 files changed, 59 insertions, 37 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index f99c539251..db9f04ba11 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2214,6 +2214,7 @@ and an explanation of the underlying technique.
    ``simple inversion``.
 
 .. tacv:: inversion @ident using @ident
+   :name: inversion ... using ...
 
    Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the
    local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 59cad3bea2..eacd7b4676 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -12,13 +12,15 @@ 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}
+.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j 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ᵢ`.
+  This command is a high-level tool for generating automatically
+  (possibly mutual) induction principles for given types and sorts.
+  Each :n:`@ident__j` is a different inductive type identifier belonging to
+  the same package of mutual inductive definitions.
+  The command generates the :n:`@ident__i`\s to be mutually recursive
+  definitions. Each term :n:`@ident__i` proves a general principle of mutual
+  induction for objects in type :n:`@ident__j`.
 
 .. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort}
 
@@ -44,9 +46,9 @@ induction for objects in type `identᵢ`.
 
     .. coqtop:: none
 
-     Axiom A : Set.	       
-     Axiom B : Set.	       
-   
+       Axiom A : Set.
+       Axiom B : Set.
+
     .. coqtop:: all
 
      Inductive tree : Set := node : A -> forest -> tree
@@ -79,7 +81,7 @@ induction for objects in type `identᵢ`.
    .. coqtop:: all
 
       Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n)
-      with even : nat -> Prop := 
+      with even : nat -> Prop :=
         | evenO : even 0
         | evenS : forall n:nat, odd n -> even (S n).
 
@@ -136,19 +138,20 @@ Automatic declaration of schemes
 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}
+.. cmd:: Combined Scheme @ident from {+, @ident__i}
 
-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.
+   This command is a tool for combining induction principles generated
+   by the :cmd:`Scheme` command.
+   Each :n:`@ident__i` is a different inductive principle that must  belong
+   to the same package of mutual inductive principle definitions.
+   This command generates :n:`@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.
+   In the case where all the inductive principles used are in sort
+   ``Prop``, the propositional conjunction ``and`` is used, otherwise
+   the simple product ``prod`` is used instead.
 
-.. example:: 
+.. example::
 
   We can define the induction principles for trees and forests using:
 
@@ -170,6 +173,23 @@ concluded by the conjunction of their conclusions.
 
     Check tree_forest_mutind.
 
+.. example::
+
+   We can also combine schemes at sort ``Type``:
+
+  .. coqtop:: all
+
+     Scheme tree_forest_rect := Induction for tree Sort Type
+     with forest_tree_rect := Induction for forest Sort Type.
+
+  .. coqtop:: all
+
+     Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect.
+
+  .. coqtop:: all
+
+     Check tree_forest_mutrect.
+
 .. _functional-scheme:
 
 Generation of induction principles with ``Functional`` ``Scheme``
@@ -186,7 +206,7 @@ schema:
 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 
+the recursive structure and case analyses of the corresponding function
 identᵢ’.
 
 .. warning::
@@ -196,7 +216,7 @@ identᵢ’.
    :cmd:`Function` generally produces smaller principles that are closer to how
    a user would implement them. See :ref:`advanced-recursive-functions` for details.
 
-.. example:: 
+.. example::
 
   Induction scheme for div2.
 
@@ -262,11 +282,11 @@ identᵢ’.
   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 :=
@@ -313,20 +333,21 @@ identᵢ’.
     Check tree_size_ind2.
 
 .. _derive-inversion:
-     
+
 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`.
+   This command generates an inversion principle for the
+   :tacn:`inversion ... using ...`  tactic. Let :g:`I` be an inductive
+   predicate and :g:`x` the variables occurring in t. This command
+   generates and stocks the inversion lemma for the sort :g:`sort`
+   corresponding to the instance :g:`∀ (x:T), I t` with the name
+   :n:`@ident` in the global environment. When applied, it is
+   equivalent to having inverted the instance with the tactic
+   :g:`inversion`.
+
 
 .. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort
 
@@ -347,7 +368,7 @@ having inverted the instance with the tactic `inversion`.
 
   Consider the relation `Le` over natural numbers and the following
   parameter ``P``:
-  
+
   .. coqtop:: all
 
     Inductive Le : nat -> nat -> Set :=
@@ -370,9 +391,9 @@ having inverted the instance with the tactic `inversion`.
 
   .. coqtop:: none
 
-    Goal forall (n m : nat) (H : Le (S n) m), P n m.			  
+    Goal forall (n m : nat) (H : Le (S n) m), P n m.
     intros.
-  
+
   .. coqtop:: all
 
     Show.