Stream: Coq devs & plugin devs

Topic: IDProp vs True


view this post on Zulip Guillaume Melquiond (Apr 18 2023 at 07:04):

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?

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 08:19):

Iirc, the reason is to work also in an empty environment, where True is not declared.

view this post on Zulip Guillaume Melquiond (Apr 18 2023 at 08:33):

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.)

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 09:40):

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...)

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 09:45):

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.

view this post on Zulip Ali Caglayan (Apr 18 2023 at 10:57):

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

view this post on Zulip Ali Caglayan (Apr 18 2023 at 10:59):

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.

view this post on Zulip Ali Caglayan (Apr 18 2023 at 10:59):

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.

view this post on Zulip Ali Caglayan (Apr 18 2023 at 11:00):

I'm all for simplyfying the current status quo.

view this post on Zulip Guillaume Melquiond (Apr 18 2023 at 11:10):

Hugo Herbelin said:

You mean at the intuitive/pedagogical level? Otherwise, IDProp and True 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.)

view this post on Zulip Gaëtan Gilbert (Apr 18 2023 at 11:14):

It probably needs something for SProp too

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 12:03):

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 *)

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 12:07):

(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).

view this post on Zulip Hugo Herbelin (Apr 18 2023 at 12:47):

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: May 18 2024 at 10:02 UTC