Hi,

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

I have a record in which there are `Prop`

s 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 `Prop`

s 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?

Just prove the properties beforehand (`Lemma foo : P. ... Qed.`

) then create the record as usual (`Definition s := { prop := foo }.`

)

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`

.

ok i see. Then does that mean it's actually the best practice to use `Program`

if that is an option?

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.

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

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

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)

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