An even better lemma extraction?

[Zimmi48]

Hi, I had been wanting to have a way to extract a lemma during a proof for quite some time so I was delighted to hear that you provide this function. I have two remarks on the current state of this feature though.

• The first is that ideally, the lemma should be inserted above the current proof, especially given that inlined lemmas are going to stop working in the next version of Coq (if we believe the warning Coq presently gives). But I also understand that some users relying on heavy automation don't want to have to play again their proof strict too many times so these people would not like that. Moreover, right before the current proof is not necessarily the best place in all cases. Would it be possible to have a way to navigate to the point where we want to extract our lemma, then do a very simple command to create it here?
• My second remark is that just generalizing the variables which are used in the current goal and selected hypotheses is not enough. Sometimes, you want to generalize further such as in this example when I did not want to get this extracted lemma:

Lemma Rlt_prod:
  forall a b x : R, f' x > 0 -> b - a > 0 -> f' x * (b - a) > 0.
Proof.

but this one instead:

Lemma Rlt_prod:
  forall a b : R, a > 0 -> b > 0 -> a * b > 0.
Proof.

Since in this case the type of terms f' x and b - a are known, it seems to me that it would be feasible to also ask "Which term do you want to generalize?" in the sense that if I want to generalize b - a, it means that I want to replace b - a by a fresh variable of the same type. Do you agree?

Thanks!

[cpitclaudel]

Hi Theo,

Thanks for your ideas and suggestions!

Would it be possible to have a way to navigate to the point where we want to extract our lemma, then do a very simple command to create it here?

I think this is already possible, actually :) Navigating to the point where you want the lemma extracted and pressing C-c C-a C-x will insert the lemma where the point is. Is that what you had in mind, or did I miss something?

Since in this case the type of terms f' x and b - a are known, it seems to me that it would be feasible to also ask "Which term do you want to generalize?

The types are known by Coq, but not by company-coq, so generalizing them is a bit tricky. This can be done using Ltac though, at least if I understand correctly. Something like the following?

  remember (b - a); remember (f' x)

Is that what you had in mind? If so, let's think of how we could integrate it smoothly -- there'll be issues with dependent types, for example.

Generally speaking, I'm not sure how much the lemma extraction should do by itself. I see it as a convenient tool because it allows you to manipulate your lemma with Ltac to get it in the right shape. I guess the question is whether remember is a common operation enough that it's worth it having it as an ad-hoc operation in lemma extraction.

[Zimmi48]

I think this is already possible, actually :) Navigating to the point where you want the lemma extracted and pressing C-c C-a C-x will insert the lemma where the point is. Is that what you had in mind, or did I miss something?

This is exactly what I had in mind. I was not aware of that. Perfect then ;)

I guess the question is whether remember is a common operation enough that it's worth it having it as an ad-hoc operation in lemma extraction.

Yes, this is also what I had in mind. Indeed, I cannot say if it would be much used. I feel like it's a common operation but I don't really know. Could company-coq do a trick such as inserting the remember steps, using the new goal and context for the lemma extraction then revert the addition?

[cpitclaudel]

This is exactly what I had in mind. I was not aware of that. Perfect then ;) Great!

Could company-coq do a trick such as inserting the remember steps, using the new goal and context for the lemma extraction then revert the addition?

Definitely; it's mostly what it does already (with generalize dependent and clear). What I'm not sure is whether it makes sense to give a special status to remember; one can always write the remember ... manually before extracting the lemma.

[cpitclaudel]

A related bug though is that company-coq doesn't offer remember _ as a completion. If it did, typing remember _ would be much faster. I'll fix that.