Stream: Miscellaneous

Topic: Automatically hide proof witnesses?


view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:28):

@Joshua Grosso is this about transparent definitions?

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:28):

There you should be using abstract or program obligations anyway.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 20:30):

I’m sure there are more exceptions but this is the main one.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:31):

for one, Program obligations are transparent by default

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:31):

and Defined

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:32):

you can Unset Transparent Obligations. or such, which I learned from theories/base.v in std++

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:32):

oh

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:33):

it might be easier to look at the actual definition containing the proof terms

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:33):

Print it, Print its obligations, check if the flag is actuall unset there...

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:34):

AFAIK it should work, but Unset is not Global Unset,

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:34):

ah, but that does sound like the obligation might be opaque

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 17:35):

the _call_ still appears in the proof term

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:02):

(nevermind that the duplication there could be reduced)

view this post on Zulip 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_

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:03):

well, the lemma essentially _is_ identical to the definition.

view this post on Zulip Joshua Grosso (Sep 24 2020 at 18:04):

Ohhhh, I totally forgot that Program modifies the definition... duh!

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:04):

that definition uses well-founded recursion

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:05):

so that proof left some scars

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:07):

anyway: with Equations unfolding lemmas, reduction avoids exposing obligations — at least in many cases.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 24 2020 at 18:09):

equations gives you a tactic simp foo that reduces foo using those lemmas.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 24 2020 at 21:41):

there's some Hide Obligations option which could be helpful

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 25 2020 at 00:24):

If you report a bug it might get fixed? Not sure what "it" is

view this post on Zulip Paolo Giarrusso (Sep 25 2020 at 00:25):

But I better leave that question to the experts, for once :big_smile:


Last updated: Aug 19 2022 at 20:03 UTC