Stream: Coq users

Topic: ✔ Difference between Two Definitions of an Indprop


view this post on Zulip Jiahong Lee (Jun 22 2022 at 08:11):

Makes sense! I'll prefer factoring variables to parameters then :D

view this post on Zulip Notification Bot (Jun 22 2022 at 08:11):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Jun 22 2022 at 09:18):

Indexes can allow you to have "more strict" types, but they come at the cost of being awkward to pattern match.

view this post on Zulip Jiahong Lee (Jun 22 2022 at 11:23):

Ali Caglayan said:

Indexes can allow you to have "more strict" types, but they come at the cost of being awkward to pattern match.

I suppose by index, you meant the n : nat in le' that is not parameterised. Is there a benefit to having a "more strict" type?

view this post on Zulip Gaëtan Gilbert (Jun 22 2022 at 11:25):

no

view this post on Zulip Gaëtan Gilbert (Jun 22 2022 at 11:26):

the types are equivalent, indices are just more annoying to work with

view this post on Zulip Gaëtan Gilbert (Jun 22 2022 at 11:27):

I don't know what Ali means by "more strict"

view this post on Zulip Ali Caglayan (Jun 22 2022 at 11:48):

I didn't mean much by it, just this:

Inductive TheSkyIsBlue : bool -> Prop :=
| i_agree_that : TheSkyIsBlue true
.

Fail
Inductive TheSkyIsBlue' (b : bool) : Prop :=
i_agree_that' : TheSkyIsBlue' true
.

There is no way to write the type with a parameter and in that sense having a parameter is more lax, and an index lets you be more specific.

view this post on Zulip Jiahong Lee (Jun 23 2022 at 00:26):

My understanding is that the type of an indprop has to be a function X -> Prop, for any X : Type. Without breaking that constraint, you're free to factor out variables as the parameters. So it's not about "strictness", but how Coq recognises an indprop as an indprop (instead of treating it as normal inductive data type).

view this post on Zulip Paolo Giarrusso (Jun 23 2022 at 02:39):

Indprops are normal inductive types (that live in Prop)

view this post on Zulip Paolo Giarrusso (Jun 23 2022 at 02:39):

Both indices and parameters are supported for all sorts — Prop, Set, Type


Last updated: Jan 29 2023 at 05:03 UTC