Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

4 files changed, 41 insertions, 4 deletions

diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
new file mode 100644
index 0000000000..ba97f7c796
--- /dev/null
+++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
@@ -0,0 +1,5 @@
+- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now
+  support syntax `Inductive foo@{=i +j *k l}` to specify variance
+  information for their universes (in :ref:`Cumulative <cumulative>`
+  mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan
+  Gilbert).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1fb337b30a..064107d088 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation:
 .. coqtop:: all
 
    Polymorphic Cumulative Record packType := {pk : Type}.
+   About packType.
 
 :g:`packType` binds a covariant universe, i.e.
 
@@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
+Specifying cumulativity
+~~~~~~~~~~~~~~~~~~~~~~~
+
+The variance of the universe parameters for a cumulative inductive may be specified by the user.
+
+For the following type, universe ``a`` has its variance automatically
+inferred (it is irrelevant), ``b`` is required to be irrelevant,
+``c`` is covariant and ``d`` is invariant. With these annotations
+``c`` and ``d`` have less general variances than would be inferred.
+
+.. coqtop:: all
+
+   Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy.
+   About Dummy.
+
+Insufficiently restrictive variance annotations lead to errors:
+
+.. coqtop:: all
+
+   Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}.
+
 An example of a proof using cumulativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -280,7 +302,7 @@ An example of a proof using cumulativity
    End down.
 
 Cumulativity Weak Constraints
------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. flag:: Cumulativity Weak Constraints
 
@@ -383,6 +405,7 @@ Explicit Universes
    | _
    | @qualid
    univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
    univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 The syntax has been extended to allow users to explicitly bind names
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index d3bd787587..ad7d6f3963 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -8,13 +8,14 @@ Inductive types
 
 .. cmd:: Inductive @inductive_definition {* with @inductive_definition }
 
-   .. insertprodn inductive_definition constructor
+   .. insertprodn inductive_definition cumul_ident_decl
 
    .. prodn::
-      inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
       | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
+      cumul_ident_decl ::= @ident {? @cumul_univ_decl }
 
    This command defines one or more
    inductive types and its constructors.  Coq generates destructors
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index e6fc6188b7..dfd3a18908 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -434,6 +434,10 @@ univ_decl: [
 | "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
+cumul_univ_decl: [
+| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+]
+
 univ_constraint: [
 | universe_name [ "<" | "=" | "<=" ] universe_name
 ]
@@ -695,7 +699,7 @@ field_def: [
 ]
 
 inductive_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
+| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations
 ]
 
 constructors_or_record: [
@@ -707,6 +711,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+cumul_ident_decl: [
+| ident OPT cumul_univ_decl
+]
+
 filtered_import: [
 | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
 ]