Reputation: 22560

How to save the current goal / subgoal as an `assert` lemma

During a proof, I come to a situation where the current goal/subgoal turned out to be useful in a later stage of the same theorem.

Is there a tactic to "save" the current goal as a lemma as if the current goal is asserted?

Of course, I can copy&paste to assert the goal explicitly, or write a separate Lemma before the current theorem. But I am just curious if shortcuts exist.

Thanks.

Upvotes: 3

Answers (3)

frabala

Reputation: 369

Leaving this answer for future reference.

I don't know since when it exists, but maybe the abstract tactic could help. It allows you to name a part of the proof and re-use it later, even if you are in a different sub-goal.

Upvotes: 1

krokodil

Reputation: 1366

If you are using Proof General, you can install a company-coq extension which provides this functionality. It is bound the C-c C-a C-x key sequence.

Upvotes: 0

Vinz

Reputation: 6057

To my knowledge, there is no such feature in Coq, and neither CoqIDE nor ProofGeneral seems to provide one.

Upvotes: 1

How to save the current goal / subgoal as an `assert` lemma

Answers (3)

Related Questions