coq - 如何将当前目标/子目标保存为“断言”引理

Question

在证明过程中，我遇到了一种情况，即当前目标/子目标在同一定理的后期阶段证明是有用的。

是否有一种策略可以将当前目标“保存”为引理，就好像当前目标已被assert编辑一样？

当然，我可以 assert明确地复制并粘贴到目标，或者在当前定理之前写一个单独的引理。但我只是好奇是否存在捷径。

谢谢。

Answer 1

据我所知， 中没有这样的功能Coq，而且似乎也CoqIDE没有提供。ProofGeneral

Answer 2

如果您使用 Proof General，您可以安装提供此功能的company-coq扩展。它绑定了C-c C-a C-x键序列。

Answer 3

留下这个答案以供将来参考。

我不知道它什么时候存在，但也许抽象策略会有所帮助。它允许您命名证明的一部分并在以后重新使用它，即使您处于不同的子目标中。