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: Nov 29 2023 at 05:01 UTC