Как сохранить текущую цель/подзаголовок в качестве леммы `assert`

Question

Во время доказательства я пришел к ситуации, когда текущая цель/подцель оказалась полезной на более позднем этапе той же теоремы.

Есть ли тактика, чтобы «сохранить» текущую цель в качестве лемм, как если бы текущая цель assert ed?

Конечно, я могу скопировать & пасту на assert цели явно или написать отдельную лемму перед текущей теоремой. Но мне просто интересно, есть ли ярлыки.

Спасибо.

Answer 1

Насколько мне известно, такой функции нет в Coq, и ни один CoqIDE, ни ProofGeneral, кажется, один.

Answer 2

Если вы используете Proof General, вы можете установить расширение company-coq, предоставляющее эту функцию. Он связан с последовательностью клавиш C-c C-a C-x.