Stream: Coq users

Topic: best practice for records carrying proofs


view this post on Zulip Jason Hu (Jul 08 2022 at 15:43):

Hi,

my Coq skill has been rusty so please pardon me if this is elementary.

I have a record in which there are Props to regulate the data. Is there a way to construct instances of such record, so that the data part is transparent but the proofs for the Props are opaque. It is similar to Instance for type classes, except that I find it strange to make this record a type class. Another possibility I can think of from my very vague memory is to just Program to make the proof opaque. Is there a more primitive way to achieve that?

view this post on Zulip Guillaume Melquiond (Jul 08 2022 at 15:45):

Just prove the properties beforehand (Lemma foo : P. ... Qed.) then create the record as usual (Definition s := { prop := foo }.)

view this post on Zulip Guillaume Melquiond (Jul 08 2022 at 15:46):

This requires duplicating the data (first in foo then in s), but hopefully it is not too much of an issue. At worst, they can themselves be Defined.

view this post on Zulip Jason Hu (Jul 08 2022 at 15:51):

ok i see. Then does that mean it's actually the best practice to use Program if that is an option?

view this post on Zulip Guillaume Melquiond (Jul 08 2022 at 15:56):

Yes and no. It really depends on your own definition of "best practice". As far as I am concerned, it would not occur to me to use Program in that case.

view this post on Zulip Paolo Giarrusso (Jul 08 2022 at 23:42):

I regularly use Program here, but there's a few pitfalls to account for (stdpp settings fix most of them, Unset Program Case is about the last one).

view this post on Zulip Paolo Giarrusso (Jul 08 2022 at 23:42):

There's also the abstract tactic, which has fewer pitfalls: if it works at all, you're good.

view this post on Zulip Paolo Giarrusso (Jul 08 2022 at 23:45):

The upside is that you avoid restating the extra properties, the downside is that you must beware a set of pitfalls. (I should maybe repeat them here but I'm tired; maybe I should post them on some gist)

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 07:52):

I also prefer to prove such statements upfront. For complicated records, say records with > 10 proofs, I tend to use modules to instantiate them. This might be biased by the fact that libraries I use (e.g. CompCert) use modules, so that this is quite convenient.


Last updated: Jan 27 2023 at 01:03 UTC