Joshua Grosso (Sep 23 2020 at 18:21): Joshua Grosso (Sep 23 2020 at 18:21):I'm assuming the answer is no, but just in case: Is there a way to tell Coq (or PG) to elide proof objects when printing? That is, if my goal contains a subterm x of some type H, where H : Prop, can I ask Coq to just print "<proof>" or something instead of printing x in its full glory?
Joshua Grosso (Sep 23 2020 at 18:22):(I'm assuming the "best" solution would be to use abstract where possible to avoid printing unwieldy witnesses, but I'm curious in general.)
Enrico Tassi (Sep 23 2020 at 18:35):My favourite trick is to define an identity function and attach to it a notation that hides the argument. But there oyher tricks, it depends on you proof script.
Paolo Giarrusso (Sep 23 2020 at 20:28):@Joshua Grosso is this about transparent definitions?
Paolo Giarrusso (Sep 23 2020 at 20:28):There you should be using abstract or program obligations anyway.
Paolo Giarrusso (Sep 23 2020 at 20:29):as a rule of thumb, if a Definition is not Qed-ed, it should usually not be defined using tactics — with the exceptions of tactics that give you a pretty predictable proof term, such as decide equality.
Paolo Giarrusso (Sep 23 2020 at 20:30):I’m sure there are more exceptions but this is the main one.
Paolo Giarrusso (Sep 23 2020 at 20:31):the reason is that definition bodies that aren’t hidden by Qed are part of your interface, not just of your implementation (and not just for Definition). In particular, of the interface to proofs about the definition in question.
Paolo Giarrusso (Sep 23 2020 at 20:34):and large proof objects affect performance of Coq, also performance of humans reading goals (as you saw :-)), and stability of the proof scripts.
Joshua Grosso (Sep 24 2020 at 17:30):@Paolo Giarrusso Weirdly enough, I'm not actually using Defined anywhere (as such, I'm not 100% sure myself where the transparent proof terms are coming from) :-P
Paolo Giarrusso (Sep 24 2020 at 17:31):for one, Program obligations are transparent by default
Paolo Giarrusso (Sep 24 2020 at 17:31):and Defined
Joshua Grosso (Sep 24 2020 at 17:32):@Paolo Giarrusso I do have Unset Transparent Obligations--I'm not 100% sure how it works though, so is that enough to avoid unnecessarily-transparent obligations?
Paolo Giarrusso (Sep 24 2020 at 17:32):you can Unset Transparent Obligations. or such, which I learned from theories/base.v in std++
Paolo Giarrusso (Sep 24 2020 at 17:32):oh
Paolo Giarrusso (Sep 24 2020 at 17:33):it might be easier to look at the actual definition containing the proof terms
Paolo Giarrusso (Sep 24 2020 at 17:33):Print it, Print its obligations, check if the flag is actuall unset there...
Joshua Grosso (Sep 24 2020 at 17:33):Enrico Tassi said:
My favourite trick is to define an identity function and attach to it a notation that hides the argument. But there oyher tricks, it depends on you proof script.
For posterity: As a quick-and-dirty hack, I temporarily added
Notation "'PROOF'" := (Morphisms.iff_flip_impl_subrelation _ _ _ _) (at level 40).
Notation "'PROOF'" := (foo_obligation_1 _ _) (at level 40).
Notation "'PROOF'" := (foo_obligation_3 _) (at level 40).
Notation "'PROOF'" := (bar_obligation_1 _ _) (at level 40).
to the beginning of my proof (and removed them after I finished).
Paolo Giarrusso (Sep 24 2020 at 17:34):AFAIK it should work, but Unset is not Global Unset,
Paolo Giarrusso (Sep 24 2020 at 17:34):ah, but that does sound like the obligation might be opaque
Paolo Giarrusso (Sep 24 2020 at 17:35):the _call_ still appears in the proof term
Paolo Giarrusso (Sep 24 2020 at 17:35):OTOH, for some Program definition, even the calls might not need to appear in the unfolding lemma — which Equations would generate for you
Paolo Giarrusso (Sep 24 2020 at 17:38):e.g. https://github.com/Blaisorblade/minidot/blob/silr/ecoop17/dot_wfrel.v#L285 does not mention any obligation, even tho the proof term does
Paolo Giarrusso (Sep 24 2020 at 17:39):(I always link to that code, not because it’s pretty, but because I had little clue back then, and even doing that was hard
Joshua Grosso (Sep 24 2020 at 17:55):Honest n00b question: What exactly is an unfolding lemma? (Having never "needed" to write one manually, I'm a bit unclear how it's different from regular-old computational reduction.) e.g. the unfolding lemma in the minidot example seems to me to be real similar to the definition itself.
Enrico Tassi (Sep 24 2020 at 17:57):You can prove by reflexivity, for example, plus (S n) m = S (plus n m), corresponding to one branch of the fixpoint. By rewriting with it you are sure 1, and only one, "simplification step" is performed. If you call simpl... it may make more, or unfold too much...
Enrico Tassi (Sep 24 2020 at 17:58):(the job done by simpl/cbn is not trivial at all, so sometimes they don't work as you want)
Paolo Giarrusso (Sep 24 2020 at 18:02):I’m afraid I was unclear: Enrico is right, but that’s not what I meant here.
Paolo Giarrusso (Sep 24 2020 at 18:02):(nevermind that the duplication there could be reduced)
Paolo Giarrusso (Sep 24 2020 at 18:03):@Joshua Grosso the lemma _looks_ identical to the _input_ of Program, but it’s very different from its _output_
Paolo Giarrusso (Sep 24 2020 at 18:03):well, the lemma essentially _is_ identical to the definition.
Joshua Grosso (Sep 24 2020 at 18:04):Ohhhh, I totally forgot that Program modifies the definition... duh!
Paolo Giarrusso (Sep 24 2020 at 18:04):that definition uses well-founded recursion
Paolo Giarrusso (Sep 24 2020 at 18:05):so that proof left some scars
Paolo Giarrusso (Sep 24 2020 at 18:06):other times, with dependent pattern matching, the “source equations” aren’t even well-typed; however, Equations proves each of those equations as an unfolding lemma (whose proof is very much not reflexivity)
Paolo Giarrusso (Sep 24 2020 at 18:07):anyway: with Equations unfolding lemmas, reduction avoids exposing obligations — at least in many cases.
Joshua Grosso (Sep 24 2020 at 18:09):I assume one would have to manually apply the lemmas in lieu of using simpl/cbn... does that make proofs way longer and/or more manual than usual, out of curiosity?
Paolo Giarrusso (Sep 24 2020 at 18:09):equations gives you a tactic simp foo that reduces foo using those lemmas.
Paolo Giarrusso (Sep 24 2020 at 18:10):the proof terms do get bigger (rewrites are more expensive), but at least here we’re rewriting by equality, so it’s not as bad as setoid rewriting.
Gaëtan Gilbert (Sep 24 2020 at 21:41):there's some Hide Obligations option which could be helpful
Joshua Grosso (Sep 24 2020 at 23:32):do you know how well-supported it is, by chance? I tried enabling it and now I'm getting "Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/." :-P
EDIT: "it" = the Hide Obligations option
Paolo Giarrusso (Sep 25 2020 at 00:24):If you report a bug it might get fixed? Not sure what "it" is
Paolo Giarrusso (Sep 25 2020 at 00:25):But I better leave that question to the experts, for once :big_smile:
Last updated: Nov 29 2023 at 05:01 UTC