Stream: Coq devs & plugin devs

Topic: inductives implicitly Prop and template poly


view this post on Zulip Gaëtan Gilbert (Jun 09 2023 at 13:23):

Currently some inductives declared with : Type or no type annotation are automatically put in Prop:

Inductive foo := .
Check foo : Prop.
Inductive bar : Type := BB.
Check bar : Prop.

I want to remove this behaviour which has confused many people (so instead the first one would go in Set and the second in Set if minim to Set is on otherwise in a floating universe).

The main obstactle IMO is that such inductives implicitly put in Prop behave differently from explicit : Prop, so we can't just put a deprecation warning telling people to put : Prop if that's what they want.
Specifically the inductive is marked template poly and consequently:

(btw with #[universes(template=no)] Prop still gets inferred but using the explicit : Prop is truly equivalent to leaving it to be inferred AFAICT)

The Keep Equalities table was added to decouple template poly from other features but this was done incompletely since we still have scheme dependence. Because of its name probably we should not reuse Keep Equalities to control scheme dependence (they don't seem related) and instead we would need a new table (Dependent Schemes?) which "templates" get auto added to.

Then we add some #[proof-relevant] attribute to auto add an inductive to both tables, and finally we have the warning to require : Prop and which also says to use the attribute if template wasn't disabled.

Does this seem like a reasonable plan to everyone?

view this post on Zulip Paolo Giarrusso (Jun 09 2023 at 23:23):

is the new table needed over just "run Scheme Induction instead of Scheme Minimality"? I say it that way because the nondependent schemes are those on the : Prop types not the "template Prop" ones AFAICT (seems the opposite of what you said but maybe I misread):

Inductive foo := .
Inductive foo' : Prop := .
Inductive bar : Type := BB.
Inductive bar' : Prop := BB'.

Check foo_rect.
Check foo'_rect.
Check bar_rect.
Check bar'_rect.
(*
foo_rect
     : forall (P : foo -> Type) (f : foo), P f
foo'_rect
     : forall P : Type, foo' -> P
bar_rect
     : forall P : bar -> Type, P BB -> forall b : bar, P b
bar'_rect
     : forall P : Type, P -> bar' -> P
*)

view this post on Zulip Paolo Giarrusso (Jun 09 2023 at 23:25):

IIUC from the docs, Keep Equalities instead must be a table because it's tested later by the injection tactic, but I don't see what would need the default Scheme type later — docs claim Scheme needs an explicit scheme_type

view this post on Zulip Paolo Giarrusso (Jun 09 2023 at 23:27):

but generally, replacing odd heuristics with attributes to control such matters seems a good idea.


Last updated: Oct 13 2024 at 01:02 UTC