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?
(I'm assuming the "best" solution would be to use abstract
where possible to avoid printing unwieldy witnesses, but I'm curious in general.)
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.
@Joshua Grosso is this about transparent definitions?
There you should be using abstract
or program obligations anyway.
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
.
I’m sure there are more exceptions but this is the main one.
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.
and large proof objects affect performance of Coq, also performance of humans reading goals (as you saw :-)), and stability of the proof scripts.
@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
for one, Program
obligations are transparent by default
and Defined
@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?
you can Unset Transparent Obligations.
or such, which I learned from theories/base.v
in std++
oh
it might be easier to look at the actual definition containing the proof terms
Print
it, Print
its obligations, check if the flag is actuall unset there...
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).
AFAIK it should work, but Unset
is not Global Unset
,
ah, but that does sound like the obligation might be opaque
the _call_ still appears in the proof term
OTOH, for some Program
definition, even the calls might not need to appear in the unfolding lemma — which Equations
would generate for you
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
(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
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.
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...
(the job done by simpl/cbn is not trivial at all, so sometimes they don't work as you want)
I’m afraid I was unclear: Enrico is right, but that’s not what I meant here.
(nevermind that the duplication there could be reduced)
@Joshua Grosso the lemma _looks_ identical to the _input_ of Program, but it’s very different from its _output_
well, the lemma essentially _is_ identical to the definition.
Ohhhh, I totally forgot that Program
modifies the definition... duh!
that definition uses well-founded recursion
so that proof left some scars
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
)
anyway: with Equations unfolding lemmas, reduction avoids exposing obligations — at least in many cases.
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?
equations gives you a tactic simp foo
that reduces foo
using those lemmas.
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.
there's some Hide Obligations option which could be helpful
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
If you report a bug it might get fixed? Not sure what "it" is
But I better leave that question to the experts, for once :big_smile:
Last updated: Jun 01 2023 at 12:01 UTC