Can someone remind me why we are using IDProp
instead of True
? I feel like we are doing a disservice to our users by making elaborated terms more complicated than they actually are. But perhaps there are some contexts in which True
would not work?
Iirc, the reason is to work also in an empty environment, where True
is not declared.
But IDProp
is given by the prelude, which also contains True
. (In fact, True
is declared in a smaller subset of the prelude than IDProp
, so even if someone were to use a smaller prelude, they would still benefit from using True
.)
In -noinit, IDProp is expanded in its definition, and this remains convertible.
There would probably not be a lot of risks of incompatibilities to use True
by default and forall X:Prop, X -> X
only if True
is undefined though. Or to let the use of True
be registered (so that e.g. HoTT can declared its one).
we are doing a disservice to our users by making elaborated terms more complicated than they actually are
You mean at the intuitive/pedagogical level? Otherwise, IDProp
and True
are technically isomorphic.
(Actually, if we want go to the intuitive way, we should eventually have impossible cases corresponding to no branch at all already in the kernel...)
Or to let the use of True be registered (so that e.g. HoTT can declared its one).
Since there would be nothing to lose to add the ability to register how the default impossible case is represented, and since True
would be indeed more intuitive, I'll support such parameterization.
Funnily enough in HoTT we register both True and IDProp as the same thing. So I am not sure what IDProp is for really. https://github.com/HoTT/Coq-HoTT/blob/c09f5eec60b852cab5d969e9d05cc0ec54b2b9d9/theories/Basics/Overture.v#L725-L728
I think the reason for IDProp was so that tactics could have some sort of sort parameterization, however by making True registerable that doesn't necesserily cause any issues.
Of course, there is still lots of tactics code that will break when something with an incorrect sort is registered, but those are typically fixed on a case by case basis.
I'm all for simplyfying the current status quo.
Hugo Herbelin said:
You mean at the intuitive/pedagogical level? Otherwise,
IDProp
andTrue
are technically isomorphic.
Yes, at the intuitive/pedagogical level. Every Coq user, even beginner, knows what True
means; hardly any user knows what IDProp
means. When you Print
a definition with irrelevant branches, this strange symbol pops up. (Using True
is not perfect though. It would presumably be better to use unit
when the sort is not Prop
, to avoid having to talk about cumulativity.)
It probably needs something for SProp too
SProp: yes, as in:
Check fun x : 0 = 1 => (match x with end : False). (* ok *)
Inductive SFalse : SProp :=.
Fail Check fun x : 0 = 1 => (match x with end : SFalse). (* would need using STrue/IDSProp *)
(* expected elaboration: *)
Inductive STrue : SProp := SI.
Check fun x : 0 = 1 => (match x in _ = y return match y return SProp with 0 => STrue | _ => _ end with eq_refl => SI end : SFalse). (* or eventually using a polymorphic True *)
(* Incidentally... *)
Fail Check fun x : 0 = 1 => (match x with eq_refl => SI end : SFalse). (* anomaly IllTypedInstance *)
(Using True is not perfect though. It would presumably be better to use unit when the sort is not Prop, to avoid having to talk about cumulativity.)
Yes, it could be unit
when the final result is not in not a proposition (for the pedagogy).
When you Print a definition with irrelevant branches, this strange symbol pops up.
An alternative would also be that the default printer does not print impossible cases. This would require a precise analysis of the reconstructibility of the pattern-matching (probably easier when small inversion is performed systematically).
Funnily enough in HoTT we register both True and IDProp as the same thing
I forgot that it is already possible to register IDProp
. The name is confusing though: it should reflect the role (filling the impossible branch) not the way it is defined. So, using True
is technically a line to change in Datatypes.v
(even if, say, a core.impossible_case.default_value
key would make more sense, it seems??).
Last updated: Oct 13 2024 at 01:02 UTC