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?
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
*)
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
but generally, replacing odd heuristics with attributes to control such matters seems a good idea.
Last updated: Oct 13 2024 at 01:02 UTC