Naming hypotheses for lemma extraction

[nickgian]

Is it possible to implement naming the hypotheses when using lemma extraction, or at least keeping the names from the current proof goal. For example (from the company-coq-tutorial):

    Lemma test:
      forall (n m : nat) (IHm: n + m = m + n), n + m.+1 = m.+1 + n.

instead of

    Lemma test:
      forall n m : nat, n + m = m + n -> n + m.+1 = m.+1 + n.

[cpitclaudel]

Yup, that would be nice! I'll think about the best way to do this. One thing I'm a bit wary of is that in many cases one might not want all the hypotheses to be named (it's kind of nice that the lemma statement makes it obvious which hypotheses are directly used in what follows them).

[cpitclaudel]

Here's a slightly different idea: what would you think of following the inserted lemma with an explicit intros command? This would prevent names from cluttering the lemma statement, but it would still yield the right names in the body of the lemma.

Would that work for you?

[cpitclaudel]

I think I have a working implementation of the proposal above. Let me know if the idea sounds good; if so, I'll push that change.

[cpitclaudel]

Thanks for your suggestion, too!

[nickgian]

Hey, thanks for the quick reply.

I like your idea, but I am not sure how useful it will be to me because I prefer to name hypotheses in my lemma statements and I'd rather be consistent about it. It is still a nice enhancement.

My idea about how to implement this is to be able to optionally name a hypotheses by some predefined syntax, e.g. name_to_use: current_name

Perhaps it can be a different command as well, I guess not everyone wants to use named hypotheses. Anyway, I guess there are many options, let's think about it more and hopefully get more feedback as well.

[cpitclaudel]

I like your idea, but I am not sure how useful it will be to me because I prefer to name hypotheses in my lemma statements and I'd rather be consistent about it. It is still a nice enhancement.

Ok; I guess I can push the new code after testing it a bit further locally, but still leave this open.

My idea about how to implement this is to be able to optionally name a hypotheses by some predefined syntax, e.g. name_to_use: current_name

Are you thinking of this as a global option, or as something you would type after starting lemma extraction?

Perhaps it can be a different command as well, I guess not everyone wants to use named hypotheses. Anyway, I guess there are many options, let's think about it more and hopefully get more feedback as well.

Indeed. In terms of implementation, the issue is that currently it's Coq that puts the lemma statement together for us: what currently happens is that we revert all hypotheses that the user wants to keep, then clear anything that we can clear, and finally revert the rest. The lemma statement is then exactly the contents of the goal. The nice part of this is that the risk for mistakes in building the lemma statement is minimized, and Coq does the dependency analysis for us.

There are three ways to implement your suggestion:

• Get Coq to display all hypothesis names in the goal (which amounts to disabling the -> notation: I don't know how to do that.
• Add a spurious term in the goal to force all names to be displayed, and remove it later. Something like cut (Some (...) = None), with arg names in the ... section, but finding the right names is hard.
• Building the full lemma manually. This is not ideal, because it relies on my goal parsing code being correct, which is a significant assumption.

[jonleivent]

Clement - I think there is an easy trick to doing bullet 2 above (the spurious term with all hyp names). I will see if I can create a mock up for you...

[jonleivent]

Here's the idea, roughly - create a constr from a tactic-in-term that contains all of the hyps (as args to a trivial function), and pose that, then revert all:

Ltac revertall := repeat lazymatch goal with H: |- _ => revert H end.

Goal forall (a b : nat)(c d : bool), True. intros. let x := constr:(ltac:(revert_all; constructor):True) in pose x. revert_all.

[cpitclaudel]

Ah, neat! Though that only works in 8.5. I wonder how easy to splice out the resulting term will be. With complex notations, properly removing that additional term will be tricky.

[jonleivent]

You can give a name to the posed definition of that term (pose x as dummyterm) so that you can find it easily. You can also wrap the value of the term in some function call with a notation that makes it easy to parse. If you give me some idea what makes it difficult to splice out, I can offer some more suggestions...

[jonleivent]

As for making it work in 8.4, that's a challenge...

[cpitclaudel]

The difficulty is that I'll be trying to find and erase that term after copying the goal for insertion as a separate lemma. If it has notations, it may be tricky to find it. Introducing notations could be a way to go, but I'm afraid that this is getting really tricky.

And indeed, 8.4 support would be nice.

[cpitclaudel]

@jonleivent, do you have an opinion about adding intros?

[jonleivent]

This hides it with implicits:

Ltac revertall := repeat lazymatch goal with H: |- _ => revert H end.

Definition DummyFun {T}{a:T} := I.

Goal forall (a b:nat)(c d:bool), True. intros. let x := constr:(ltac:(revertall;constructor):True) in idtac x; pose (@DummyFun x). revert_all.

[jonleivent]

I don't think 84 can use anything like the same trick.

[jonleivent]

My opinion on adding intros? I have not used this feature yet (I'm not fond of nested definitions in Coq), so maybe I'm not the right person to ask.

[cpitclaudel]

Re intros: Fair enough. I don't generally nest these definitions myself: I just move them up once I'm done with the proof.

[jonleivent]

Maybe a suggestion for an enhancement to Coq: allow a subgoal, suitably pruned of unneeded hyps, to become a named obligation that is proved later. I think Idris does things like this.

How about the hiding via implicits? If the "let _ := DummyFun in" is still too much for you to splice out, I think that can be hidden as well via another trick (use an apply on the conclusion to alter its type to something like DummyFun that carries the hyp names implicitly, and just returns the conclusion type).

[jonleivent]

Ltac revertall := repeat lazymatch goal with H: |- _ => revert H end.

Definition DummyFun {T}{a:T}(S:Type) : Type := S.

Variable T : Type.

Goal forall (a b:nat)(c d:bool), T. intros. let x := constr:(ltac:(revertall;constructor):True) in idtac x; lazymatch goal with |- ?G => change G with (@DummyFun x G) end. revert_all.

[cpitclaudel]

Thanks Jonathan. I think that's enough material to try something out on my side. I'll need to think about whether the divergence between 8.4 and 8.5 is worth it, too; especially since not everyone will want all hypotheses to be named.