coq - 現在のゴール/サブゴールを assert 補題として保存する方法

Question

証明中に、現在のゴール/サブゴールが同じ定理の後の段階で役立つことが判明した状況に遭遇しました。

assert現在の目標がedであるかのように、現在の目標を補題として「保存」する戦術はありますか?

もちろん、 assertゴールに明示的にコピー&ペーストすることも、現在の定理の前に別の Lemma を書くこともできます。しかし、ショートカットが存在するかどうかは興味があります。

ありがとう。

Answer 1

私の知る限り、 にはそのような機能はなくCoq、どちらCoqIDEもProofGeneral提供していないようです。

Answer 2

Proof General を使用している場合は、この機能を提供するcompany-coq拡張機能をインストールできます。C-c C-a C-xキーシーケンスがバインドされています。