Combined Scheme tests sort to use either "*" or "/\"

And update documentation.

7 files changed, 132 insertions, 44 deletions

diff --git a/CHANGES b/CHANGES
index 8651c8e23a..f6c3985ba7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -164,6 +164,8 @@ Vernacular Commands
   scope. If you want the previous behavior, use `Global Set SsrHave
   NoTCResolution`.
 - Multiple sections with the same name are allowed.
+- Combined Scheme can now work when inductive schemes are generated in sort
+  Type. It used to be limited to sort Prop.
 
 Coq binaries and process model
 
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.
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 36a9598f36..026b7aa316 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -349,6 +349,9 @@ let coq_iff = lazy_init_reference ["Logic"] "iff"
 let coq_iff_left_proj  = lazy_init_reference ["Logic"] "proj1"
 let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
 
+let coq_prod = lazy_init_reference ["Datatypes"] "prod"
+let coq_pair = lazy_init_reference ["Datatypes"] "pair"
+
 (* Runtime part *)
 let build_coq_True ()  = Lazy.force coq_True
 let build_coq_I ()     = Lazy.force coq_I
@@ -364,6 +367,9 @@ let build_coq_iff ()   = Lazy.force coq_iff
 let build_coq_iff_left_proj ()  = Lazy.force coq_iff_left_proj
 let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 
+let build_coq_prod () = Lazy.force coq_prod
+let build_coq_pair () = Lazy.force coq_pair
+
 
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
diff --git a/library/coqlib.mli b/library/coqlib.mli
index b4bd1b0e06..8844684957 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -101,7 +101,7 @@ val glob_jmeq : GlobRef.t
    at compile time. Therefore, we can only provide methods to build
    them at runtime. This is the purpose of the [constr delayed] and
    [constr_pattern delayed] types. Objects of this time needs to be
-   forced with [delayed_force] to get the actual constr or pattern 
+   forced with [delayed_force] to get the actual constr or pattern
    at runtime. *)
 
 type coq_bool_data = {
@@ -167,7 +167,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 val build_coq_sumbool : GlobRef.t delayed
 
 (** {6 ... } *)
-(** Connectives 
+(** Connectives
    The False proposition *)
 val build_coq_False : GlobRef.t delayed
 
@@ -186,6 +186,10 @@ val build_coq_iff : GlobRef.t delayed
 val build_coq_iff_left_proj : GlobRef.t delayed
 val build_coq_iff_right_proj : GlobRef.t delayed
 
+(** Pairs *)
+val build_coq_prod : GlobRef.t delayed
+val build_coq_pair : GlobRef.t delayed
+
 (** Disjunction *)
 val build_coq_or : GlobRef.t delayed
 
diff --git a/test-suite/success/CombinedScheme.v b/test-suite/success/CombinedScheme.v
new file mode 100644
index 0000000000..d6ca7a299f
--- /dev/null
+++ b/test-suite/success/CombinedScheme.v
@@ -0,0 +1,35 @@
+Inductive even (x : bool) : nat -> Type :=
+| evenO : even x 0
+| evenS : forall n, odd x n -> even x (S n)
+with odd (x : bool) : nat -> Type :=
+| oddS : forall n, even x n -> odd x (S n).
+
+Scheme even_ind_prop := Induction for even Sort Prop
+with odd_ind_prop := Induction for odd Sort Prop.
+
+Combined Scheme even_cprop from even_ind_prop, odd_ind_prop.
+
+Check even_cprop :
+  forall (x : bool) (P : forall n : nat, even x n -> Prop)
+    (P0 : forall n : nat, odd x n -> Prop),
+    P 0 (evenO x) ->
+    (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) ->
+    (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) ->
+    (forall (n : nat) (e : even x n), P n e) /\
+    (forall (n : nat) (o : odd x n), P0 n o).
+
+Scheme even_ind_type := Induction for even Sort Type
+with odd_ind_type := Induction for odd Sort Type.
+
+(* This didn't work in v8.7 *)
+
+Combined Scheme even_ctype from even_ind_type, odd_ind_type.
+
+Check even_ctype :
+  forall (x : bool) (P : forall n : nat, even x n -> Prop)
+    (P0 : forall n : nat, odd x n -> Prop),
+    P 0 (evenO x) ->
+    (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) ->
+    (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) ->
+    (forall (n : nat) (e : even x n), P n e) *
+    (forall (n : nat) (o : odd x n), P0 n o).
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e86e108772..1ec15588ff 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -82,7 +82,7 @@ let _ =
 
 let is_eq_flag () = !eq_flag
 
-let eq_dec_flag = ref false 
+let eq_dec_flag = ref false
 let _ =
   declare_bool_option
     { optdepr  = false;
@@ -375,7 +375,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   and env0 = Global.env() in
   let sigma, lrecspec, _ =
     List.fold_right
-      (fun (_,dep,ind,sort) (evd, l, inst) -> 
+      (fun (_,dep,ind,sort) (evd, l, inst) ->
        let evd, indu, inst =
 	 match inst with
 	 | None ->
@@ -445,6 +445,9 @@ let fold_left' f = function
 let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
 let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
 
+let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ())
+let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ())
+
 let build_combined_scheme env schemes =
   let evdref = ref (Evd.from_env env) in
   let defs = List.map (fun cst ->
@@ -462,10 +465,25 @@ let build_combined_scheme env schemes =
   in
   let (c, t) = List.hd defs in
   let ctx, ind, nargs = find_inductive t in
+  (* We check if ALL the predicates are in Prop, if so we use propositional
+     conjunction '/\', otherwise we use the simple product '*'.
+  *)
+  let inprop =
+    let inprop (_,t) =
+      Retyping.get_sort_family_of env !evdref (EConstr.of_constr t)
+      == Sorts.InProp
+    in
+    List.for_all inprop defs
+  in
+  let mk_and, mk_conj =
+    if inprop
+    then (mk_coq_and, mk_coq_conj)
+    else (mk_coq_prod, mk_coq_pair)
+  in
   (* Number of clauses, including the predicates quantification *)
   let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
-  let sigma, coqand  = mk_coq_and !evdref in
-  let sigma, coqconj = mk_coq_conj sigma in
+  let sigma, coqand  = mk_and !evdref in
+  let sigma, coqconj = mk_conj sigma in
   let () = evdref := sigma in
   let relargs = rel_vect 0 prods in
   let concls = List.rev_map
@@ -483,7 +501,8 @@ let build_combined_scheme env schemes =
       (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
-  (!evdref, body, typ)
+  let sigma = Typing.check env !evdref (EConstr.of_constr body) (EConstr.of_constr typ) in
+  (sigma, body, typ)
 
 let do_combined_scheme name schemes =
   let open CAst in