"Omit proof" on a Let in a section leads to warning

[RalfJung]

"Omit proof" on a Let in a section leads to warning

[RalfJung]

Let's see what the Coq devs say in coq/coq#17199. I don't quite understand what the warning is about either...

[erikmd]

Dear @RalfJung, thanks for your feedback.

I can reproduce this behavior, but I wouldn't call this a "bug", as omit-proofs precisely ignores the whole proof script reflexivity. Qed. proof and replaces it with Admitted., we get:

Section test.
Let Fact: 0 = 0.
Proof. Admitted.
(* Warning: Let definition Fact declared as an axiom. [let-as-axiom,vernacular]
Fact is declared *)

so I guess we can just mark this issue as wontfix / upstream.

[RalfJung]

I think it is a bug to get a warning here. Enabling the "omit proofs" feature should just make things go faster, it shouldn't cause any other side-effects like this.

Though I can imagine that fixing this bug might be hard due to Coq constraints.

[erikmd]

This is just an upstream warning.
Actually, I can understand this warning that in the presence of an Admitted. proof and a local definition (Let),
there is some risk that the generated axioms forgets or doesn't list in good order the section's hypothesis.

[erikmd]

But precisely, this can be handled by the Proof using … clause :)
I'll come with an example.

[RalfJung]

Let me just say that the user experience here is quite bad: I have a huge file that used to always work fine, and now suddenly I get this strange warning. I spend a bunch of time to figure out what this is about (there's no line number or anything that would even tell me where in my proof script the issue arises), only to realize that actually my proof script is completely fine and the warning is caused by "omit proofs".

It's an upstream warning about code I didn't write, and a warning that doesn't indicate anything wrong with my code. If that's not a bug I don't know what is.^^

[erikmd]

Hi! Yes I understand your point.

Actually I'm not really sure of the "usefulness" caused by this upstream warning.

In my second comment, I had guessed it could be related to the risk that Coq generalizes section hypothesese too eagerly.
I'm not sure of the intent, but that looks plausible.

But in this case, lemmas fact2 and fact3 below involving Proof using … shouldn't raise this warning as the generalization at section-closing-time is properly handled in this case.

Section test.
Hypothesis hyp : True.
Hypothesis hyp2 : True /\ True.
Let fact1: 0 = 0.
Proof. Admitted.
(* > Proof. Admitted.
>        ^^^^^^^^^
Warning: Let definition fact1 declared as an axiom. [let-as-axiom,vernacular]
fact1 is declared
*)

Let fact2: 0 = 0.
Proof using hyp2. Admitted. (* only use hyp2 *)
(* > Proof using hyp2. Admitted.
>                   ^^^^^^^^^
Warning: Let definition fact2 declared as an axiom. [let-as-axiom,vernacular]
fact2 is declared
*)

Let fact3: 0 = 0.
Proof using Type. Admitted. (* placeholder to use no section hyp *)
(* > Proof using Type. Admitted.
>                   ^^^^^^^^^
Warning: Let definition fact3 declared as an axiom. [let-as-axiom,vernacular]
fact3 is declared
*)

End test.
Check fact1.
(* fact1 *)
(*      : True -> True /\ True -> 0 = 0 *)
Check fact2.
(* fact2 *)
(*      : True /\ True -> 0 = 0 *)
Check fact3.
(* fact3 *)
(*      : 0 = 0 *)

[erikmd]

To address the usability issue, I think Coq should disable the warning, at least when a Proof using … clause is included, or ideally always, for simplicity. Feel free to open an issue upstream if you can!

In the meantime, you can just disable this warning in your _CoqProject;
and I'm going to add a comment in the PG documentation…

I'm sorry if the experience is not as smooth as expected currently, but actually doing C-u C-c C-RET is precisely intended as a syntactic facility for replacing on-the-fly whole proofs with Admitted, which is not an exotic workflow… (I was doing this everytime before omit-proofs… without a shortcut 😅)

[erikmd]

In the meantime, you can just disable this warning in your _CoqProject;

for the record, the exact snippet is:

_CoqProject

-arg -w -arg -let-as-axiom

[hendriktews]

Thanks for reporting this, we should do something about it, though we will probably not really fix it.

[...] Enabling the "omit proofs" feature should just make things go faster, it shouldn't cause any other side-effects like this.

I can understand this expectation, but this is impossible to achieve without completely parsing the input. If you make this a requirement, we would have to disable the omit proofs feature. The feature consists only of little more than two regular expressions that search for "Proof" and "Qed". It only works on a quite restricted subset of the Coq syntax. "Let" is apparently outside this subset. I would suggest to deal with this issue as follows: - Add a warning in the manual and change the wording for the option to make clear that omitting proofs may have strange side effects. - Describe more clearly the requirements on the input for the feature. - Include another regexp that searches for stuff that breaks omitting proofs and aborting proof omission when there is a match. The code already disables the omission when it recognizes nested proofs. This would be similar. "Let" should be in this regexp. This regexp won't ever be complete, but it will hopefully catch a number of cases. What do you think?

[RalfJung]

Disabling omitting proofs for Let makes sense to me.

[erikmd]

Disabling omitting proofs for Let makes sense to me.

Yes, this seems to be the natural solution after the discussion in coq/coq#17199 (comment)

However, note that as pointed out by the coq devs, your use case of Let…Qed is somehow deprecated! at the very best, the cooked proof terms are not opaque.

So I see another solution for you, which does not require changing PG:
replace Let…Qed. with either Lemma…Qed. or Let…Defined.

And I realize all this discussion took place thanks to this warning… which was useful actually :)

[RalfJung]

Yeah we had no idea this was deprecated, it has worked fine for us.^^

[hendriktews]

See also #689.