I've been using
Program Definition to define my sigma types, and I was wondering if there was a way to make parts of my proof within the same obligation opaque. Is there a more convenient way to define the first projection of the sigma type transparent and the second projection opaque, instead of defining each projection as separate lemmas and using
I usually make sure to use different obligations (with an underscore for the first part), and use Unset Transparent Obligations (from coq-stdpp) so all obligations are opaque.
Then you still need a separate Defined lemma for the first projection if you want proof mode and ltac:() isn’t enough, but writing transparent definitions with tactics can be fragile so I mostly don’t (except for decide equality).
Others use various “partially opaque identity functions” to block reduction of part of a term, and they might be useful, but there are subtle differences : Coq has different ways to make things “opaque”, and they’re not equivalent.
I see, thanks! Do you know where I might be able to find examples of these "partially opaque identity functions"? Also, just for clarification, what are the differences between the different "opaque"-nesses in Coq? Is it that they end up having different observable behavior depending on the reduction strategy, or that their implementation is different?
abstract tactic can alleviate the cost of defining an independent opaque lemma (but I think it also has its own share of shortcomings and surprising interactions with the rest of the system)
abstract indeed create a separate top-level lemma?
@Irene Yoon happy to elaborate, but can you add why do you want some things to be opaque? There’s information hiding, performance and more ... There are different motivations and different solutions, and solutions range from
Qed to stdpp’s
Arguments foo : simpl never, ... (I wouldn’t call all of those “opaque” but they serve similar goals).
I have some nested sigma types in my proof context, and I would like
cbn to not unfold the proof of the predicate because it's irrelevant & makes the proof context unwieldy.
Last updated: Jan 28 2023 at 07:30 UTC