Merge PR coq#18989: Warn when automatically lowering an inductive dec…

…lared with `: Type` to Prop

Reviewed-by: ppedrot
Ack-by: jfehrle
Co-authored-by: ppedrot <[email protected]>

dev/ci/user-overlays/18989-SkySkimmer-warn-auto-lower.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi warn-auto-lower 18989

doc/changelog/06-Ltac2-language/18989-warn-auto-lower.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  :flag:`Automatic Proposition Inductives`, :flag:`Dependent Proposition Eliminators` and
+  :warn:`warning when automatically lowering an inductive declared with Type to Prop
+  <automatic-prop-lowering>`
+  (`#18989 <https://github.com/coq/coq/pull/18989>`_,
+  by Gaëtan Gilbert).

doc/sphinx/language/coq-library.rst

@@ -158,6 +158,15 @@ At times, it's helpful to know exactly what these notations represent.
   | or_intror (_:B).
   Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
 
+We also have the `Type` level negation:
+
+.. index::
+  single: notT (term)
+
+.. coqtop:: in
+
+  Definition notT (A:Type) := A -> False.
+
 Quantifiers
 +++++++++++
 
@@ -318,15 +327,9 @@ Programming
   Inductive bool : Set := true | false.
   Inductive nat : Set := O | S (n:nat).
   Inductive option (A:Set) : Set := Some (_:A) | None.
-  Inductive identity (A:Type) (a:A) : A -> Type :=
-    refl_identity : identity A a a.
 
 Note that zero is the letter ``O``, and *not* the numeral ``0``.
 
-The predicate ``identity`` is logically
-equivalent to equality but it lives in sort ``Type``.
-It is mainly maintained for compatibility.
-
 We then define the disjoint sum of ``A+B`` of two sets ``A`` and
 ``B``, and their product ``A*B``.
 
@@ -700,33 +703,6 @@ fixpoint equation can be proved.
   End FixPoint.
   End Well_founded.
 
-Accessing the Type level
-~~~~~~~~~~~~~~~~~~~~~~~~
-
-The standard library includes ``Type`` level definitions of counterparts of some
-logic concepts and basic lemmas about them.
-
-The module ``Datatypes`` defines ``identity``, which is the ``Type`` level counterpart
-of equality:
-
-.. index::
-   single: identity (term)
-
-.. coqtop:: in
-
-   Inductive identity (A:Type) (a:A) : A -> Type :=
-     identity_refl : identity A a a.
-
-Some properties of ``identity`` are proved in the module ``Logic_Type``, which also
-provides the definition of ``Type`` level negation:
-
-.. index::
-  single: notT (term)
-
-.. coqtop:: in
-
-  Definition notT (A:Type) := A -> False.
-
 Tactics
 ~~~~~~~
 

doc/sphinx/language/core/inductive.rst

@@ -42,10 +42,24 @@ Inductive types
    respectively correspond to
    on :g:`Type`, :g:`Prop`, :g:`Set` and :g:`SProp`.  Their types
    expresses structural induction/recursion principles over objects of
-   type :n:`@ident`.  The :term:`constant` :n:`@ident`\ ``_ind`` is always
-   generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect``
-   may be impossible to derive (for example, when :n:`@ident` is a
-   proposition).
+   type :n:`@ident`.  These :term:`constants <constant>` are generated when
+   possible (for instance :n:`@ident`\ ``_rect`` may be impossible to derive
+   when :n:`@ident` is a proposition).
+
+   .. flag:: Dependent Proposition Eliminators
+
+      The inductive principles express dependent elimination when the
+      inductive type allows it (always true when not using
+      :flag:`Primitive Projections`), except by default when the
+      inductive is explicitly declared in `Prop`.
+
+      Explicitly `Prop` inductive types declared when this flag is
+      enabled also automatically declare dependent inductive
+      principles. Name generation may also change when using tactics
+      such as :tacn:`destruct` on such inductives.
+
+      Note that explicit declarations through :cmd:`Scheme` are not
+      affected by this flag.
 
    :n:`{? %| {* @binder } }`
      The :n:`|` separates uniform and non uniform parameters.
@@ -148,6 +162,37 @@ by giving the type of its arguments alone.
 
       Inductive nat : Set := O | S (_:nat).
 
+Automatic Prop lowering
++++++++++++++++++++++++
+
+When an inductive is declared without an explicit sort, it is put in the
+smallest sort which permits large elimination (excluding
+`SProp`). For :ref:`empty and singleton <Empty-and-singleton-elimination>`
+types this means they are declared in `Prop`.
+
+.. flag:: Automatic Proposition Inductives
+
+   By default the above behaviour is extended to empty and singleton
+   inductives explicitly declared in `Type` (but not those in explicit
+   universes using `Type@{u}`, or in `Type` through an auxiliary definition
+   such as `Definition typ := Type.`).
+
+   Disabling this flag prevents inductives with an explicit non-`Prop`
+   type from being lowered to `Prop`. This will become the default in
+   a future version. Use :flag:`Dependent Proposition Eliminators` to
+   declare the inductive type in `Prop` while preserving compatibility.
+
+   Depending on universe minimization they may then be declared in
+   `Set` or in a floating universe level,
+   see also :flag:`Universe Minimization ToSet`.
+
+.. warn:: Automatically putting @ident in Prop even though it was declared with Type.
+   :name: automatic-prop-lowering
+
+   This warning is produced when :flag:`Automatic Proposition
+   Inductives` is enabled and resulted in an inductive type being
+   lowered to `Prop`.
+
 Simple indexed inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

doc/sphinx/language/core/variants.rst

@@ -53,9 +53,9 @@ be defined using :cmd:`Variant`.
 
    .. coqtop:: in
 
-      Variant bool : Type := true : bool | false : bool.
-      Variant unit : Type := tt : unit.
-      Variant Empty_set : Type :=.
+      Variant bool : Set := true : bool | false : bool.
+      Variant unit : Set := tt : unit.
+      Variant Empty_set : Set :=.
 
   The option and sum types are defined by:
 

doc/sphinx/language/extensions/canonical.rst

@@ -524,7 +524,7 @@ We need some infrastructure for that.
 
   Module infrastructure.
 
-    Inductive phantom {T : Type} (t : T) : Type := Phantom.
+    Inductive phantom {T : Type} (t : T) := Phantom.
 
     Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
       phantom t1 -> phantom t2.

plugins/funind/glob_term_to_relation.ml

@@ -1518,9 +1518,10 @@ let do_build_inductive evd (funconstants : pconstant list)
   try
     with_full_print
       (Flags.silently
-         (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds
-            ~cumulative:false ~poly:false ~private_ind:false
-            ~uniform:ComInductive.NonUniformParameters))
+         (Flags.without_option ComInductive.Internal.do_auto_prop_lowering
+            (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds
+               ~cumulative:false ~poly:false ~private_ind:false
+               ~uniform:ComInductive.NonUniformParameters)))
       Declarations.Finite
   with
   | UserError msg as e ->

test-suite/bugs/HoTT_coq_054.v

@@ -1,6 +1,6 @@
 Inductive Empty : Prop := .
 
-Inductive paths {A : Type} (a : A) : A -> Type :=
+Inductive paths {A : Type} (a : A) : A -> Prop :=
   idpath : paths a a.
 
 Notation "x = y :> A" := (@paths A x y) : type_scope.
@@ -46,10 +46,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y return Prop with
+           | inr x' => match y as y return match y  with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y return Prop with
+                                           end -> match f y  with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap

test-suite/bugs/bug_4116.v

@@ -36,7 +36,7 @@ Notation compose := (fun g f x => g (f x)).
 
 Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
 
-Inductive paths {A : Type} (a : A) : A -> Type :=
+Inductive paths {A : Type} (a : A) : A -> Prop :=
   idpath : paths a a.
 
 Arguments idpath {A a} , [A] a.

test-suite/bugs/bug_5501.v

@@ -5,7 +5,7 @@ Record Pred@{A} :=
   ; P : car -> Prop
   }.
 
-Class All@{A} (A : Pred@{A}) : Type :=
+Class All@{A} (A : Pred@{A}) :=
   { proof : forall (a : A), P A a
   }.
 

test-suite/output/ArgumentsScope.v

@@ -81,8 +81,8 @@ About g''.
 
 Module SectionTest1.
 
-  Inductive A:Type :=.
-  Inductive B:Type :=.
+  Inductive A :=.
+  Inductive B :=.
   Declare Scope X.
   Section S.
     Declare Scope Y.
@@ -99,7 +99,7 @@ End SectionTest1.
 
 Module SectionTest2.
 
-  Inductive A:Type :=.
+  Inductive A :=.
   Module M.
     Declare Scope X.
     Bind Scope X with A.

test-suite/output/bug_13266.v

@@ -1,4 +1,4 @@
-Inductive proc : Type -> Type :=
+Inductive proc : Type -> Prop :=
 | Tick : proc unit
 .
 

test-suite/output/inference.v

@@ -21,6 +21,6 @@ Print P.
 
 (* Note: exact numbers of evars are not important... *)
 
-Inductive T (n:nat) : Type := A : T n.
+Inductive T (n:nat) := A : T n.
 Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.

test-suite/success/AutoPropLowering.v

@@ -0,0 +1,17 @@
+Set Warnings "+automatic-prop-lowering".
+
+Fail Inductive foo : Type := .
+
+Unset Automatic Proposition Inductives.
+
+Inductive foo : Type := .
+
+Fail Check foo : Prop.
+
+Inductive bar := .
+
+Check bar : Prop.
+
+Inductive baz := Baz (_:True) (_:baz).
+
+Check baz : Prop.

test-suite/success/DependentPropositionEliminators.v

@@ -0,0 +1,6 @@
+
+Set Dependent Proposition Eliminators.
+
+Inductive bar : Prop := XBAR | YBAR.
+
+Check bar_ind : forall P : bar -> Prop, P XBAR -> P YBAR -> forall b : bar, P b.

theories/micromega/OrderedRing.v

@@ -43,7 +43,7 @@ Notation "x ~= y" := (~ req x y).
 Notation "x <= y" := (rle x y).
 Notation "x < y" := (rlt x y).
 
-Record SOR : Type := mk_SOR_theory {
+Record SOR : Prop := mk_SOR_theory {
   SORsetoid : Setoid_Theory R req;
   SORplus_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
   SORtimes_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2;