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: Oct 13 2024 at 01:02 UTC