Irene Yoon (Jun 13 2020 at 15:26): Irene Yoon (Jun 13 2020 at 15:26):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 Defined and Qed?
Paolo Giarrusso (Jun 13 2020 at 15:55):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.
Paolo Giarrusso (Jun 13 2020 at 15:58):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).
Paolo Giarrusso (Jun 13 2020 at 16:01):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.
Irene Yoon (Jun 13 2020 at 16:09):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?
Kenji Maillard (Jun 13 2020 at 17:14):The 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)
Paolo Giarrusso (Jun 13 2020 at 19:18):does abstract indeed create a separate top-level lemma?
Paolo Giarrusso (Jun 13 2020 at 19:21):@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 seal to Opaque, Typeclasses Opaque, Arguments foo : simpl never, ... (I wouldn’t call all of those “opaque” but they serve similar goals).
Irene Yoon (Jun 13 2020 at 19:31):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: Apr 18 2024 at 01:01 UTC