Warn on Qed Let declaration

[SkySkimmer]

cf #10459

[silene]

This is bad. Turning the Let Qed tests into Let Defined ones makes it impossible to interactively navigate the files. For the sake of your sanity, I won't even copy-paste what Coqide looks like at that point.

It is better to disable the warning for these files and keep Let Qed. Hopefully, one day we have an actual command or attribute that make it possible to discard definitions from sections.

[SkySkimmer]

Hopefully, one day we have an actual command or attribute that make it possible to discard definitions from sections.

I don't see a way to have it make sense.

[silene]

I don't see a way to have it make sense.

Why? We already have a Reset command in Coq. Having the section's End do a reset to the start of the section does not seem so farfetched to me.

[ejgallego]

Having the section's End do a reset to the start of the section does not seem so farfetched to me.

Actually this what the actual implementation does, then replays some stuff, IIRC, no?

[SkySkimmer]

This is bad. Turning the Let Qed tests into Let Defined ones makes it impossible to interactively navigate the files. For the sake of your sanity, I won't even copy-paste what Coqide looks like at that point.

We could do something like the current Qed hack for Opaque variables, or only omit the bodies when printing the goal. It makes more sense for Opaque as that's not supposed to be as strong as Qed.

Why? We already have a Reset command in Coq. Having the section's End do a reset to the start of the section does not
seem so farfetched to me.

How is that related? I don't think I understand what you mean by "discard definitions from sections".

[silene]

I mean this:

Section Foo.
  Example foo : True.
  Proof. exact I. Qed.
End Foo.
Reset Foo.
About foo.
(* foo not a defined object. *)

[Alizter]

That's great but what about when the user does:

Section Foo.
  Example foo : True.
  Proof. exact I. Qed.
  Definition bar : True.
  Proof. apply foo. Defined.
End Foo.

What is the definition of bar?

[silene]

There is no definition of bar. The whole point is to discard a section, e.g., the Section Examples from Qfield.v.

[Alizter]

So what you really want is a way to abort a section?

[silene]

That is another way to phrase it, yes. (Was "discard" really that strange a concept?)

[SkySkimmer]

For me it was the phrasing as "discard definitions from sections" instead of "discard sections", the first one sounds like it is about discarding a subset of the section at least in the context of this PR.

[Alizter]

But to let @SkySkimmer make progress on this PR, you are suggesting to implement that feature before this one so that the behavior of the examples in the file are adequate?

[silene]

Not at all. I am suggesting that the changes to Qfield.v and similar ones should be reverted and replaced by a local disabling of the new warning.

[SkySkimmer]

Not at all. I am suggesting that the changes to Qfield.v and similar ones should be reverted and replaced by a local disabling of the new warning.

I made a section per example instead, that way they don't interfere with each other.
We should not rely on the LetQed behaviour if at all possible.

[ppedrot]

ping @silene about the new state of the PR

[silene]

I am fine with the way the examples are written. (I suppose that, in the long run, we should stop storing Goal statements into modules, which would solve this mess in a more intuitive way.)

No longer relevant.

[SkySkimmer]

changed doc

[ppedrot]

@coqbot merge now

[jfehrle]

A few more wording suggestions

[jfehrle]

a :cmd:`Let` with :cmd:`Qed` with `Let` -> a :cmd:`Let` with :cmd:`Qed`

[jfehrle]

    the body when checking, and it will be treated the same as a
   :cmd:`Defined` `Let` when the section is closed.

->

   the body when checking.  When the section is closed,
   it will be treated as if :cmd:`Defined` had been specified.

(the same as a :cmd:`Defined` `Let` seemed awkward.)

[proux01]

User report: the feature is indeed used in MathComp. Replacing Qed with Defined there incurs an acceptable slowdown but clutters the environment of subsequent proofs and doing a bunch of clearbody manually there is not very practical. So we currently resorted to silence the warning.

What about having Qed in Let trigger an abstract?

Otherwise, would it make sense to add an attribute clearbody to Let that would automatically perform the clearbody in every subsequent proof in the section?

[SkySkimmer]

What about having Qed in Let trigger an abstract?

Wouldn't that be the same as using Lemma with Qed? If that's what you want why not use Lemma?

Otherwise, would it make sense to add an attribute clearbody to Let that would automatically perform the clearbody in every subsequent proof in the section?

That would be OK IMO
I guess it would just use the current fake-Qed mechanism under the hood.

[ppedrot]

While we're at it, I think it would be great to have attributes for Let declarations that allow to control their inlining at section closure. Such a mechanism seems to have a cross-section with the topic discussed here.

[proux01]

What about having Qed in Let trigger an abstract?

Wouldn't that be the same as using Lemma with Qed? If that's what you want why not use Lemma?

No, Let puts the lemma in the section context (so that it can be picked up by assumption for instance), that's what it is used for in MathComp. (We did try to use Lemma but that required adding a lot of Hint)

[herbelin]

Maybe an idle talk, but would it make sense to add an opaque flag also to local definitions, that is to have the additional typing rule:

Γ, x : A ⊢ t : B       Γ ⊢ u : A
----------------------------------------
Γ ⊢ let opaque x := u : A in t : B[x:=u]

which, in other words, means to internalize the usual substitution as an explicit constructor of the syntax?

[SkySkimmer]

How would it reduce?

[herbelin]

I guess we can consider that it reduces to t[x:=u] (that is that the opacity is only about not adding the definitional equality x ≣ u when typing t).

Or we may also imagine that it is blocked (as it would be for a global definition), providing some proof-irrelevance, that is identifying let opaque x := u in t and let opaque x := v in t (it looks a bit strange though).

[herbelin]

BTW, what is the attribute to make opaque a Definition (if there is one)? If there isn't, could #[clearbody] work also for Definition?

[SkySkimmer]

I guess we can consider that it reduces to t[x:=u] (that is that the opacity is only about not adding the definitional equality x ≣ u when typing t).

But then isn't there no difference between let opaque x := v in w and (fun x => w) v?

BTW, what is the attribute to make opaque a Definition (if there is one)? If there isn't, could #[clearbody] work also for Definition?

The point of clearbody is that it is not opaque, it is some adhoc thing for section letins.

[herbelin]

But then isn't there no difference between let opaque x := v in w and (fun x => w) v?

Yes, no difference except that one is a beta-redex and the other an explicit substitution. With an explicit substitution, one can directly simulate a context Section S. Let x : t. exact u. Qed.. With a fun, it would be more far-stretched to do so.

[herbelin]

Is this the "ad hoc" thing you are mentioning?

Section S.
#[clearbody]
Let a:=0.
Lemma e : a = 0. Fail exact eq_refl. Abort.
Definition e : a = 0 := eq_refl. (* works *)

[herbelin]

I still have my question: is there an attribute to tell that Definition a := t. should be considered opaque? And if not, couldn't we provide one?

[SkySkimmer]

Isn't that basically rocq-prover/rfcs#42 ?

[herbelin]

Wouldn't it be more consistent to grant variable opacity for all declarations and not only for interactively proved declarations? Alternatively. would there be compatibility issues at making a Qed-ed or clearbody-ed local definition opaque for all the rest of the section?

[herbelin]

Isn't that basically rocq-prover/rfcs#42 ?

If only a decision is needed to at least already implement sealed/unsealed from rocq-prover/rfcs#42, I propose we take it!

[herbelin]

For the record, that is not a problem, but clearbody fails on Context

Section S.
#[clearbody] Context (b:=0).
(* This command does not support this attribute: clearbody. *)