在 Coq 中对两个子目标使用相同的证明

Question

在对归纳类型进行归纳之后，我有两个子目标要证明。假设和目标略有不同，但可以通过相同的（长）证明来解决，目前看起来像这样：

induction x.
{
  admit.
}
{
  <long proof>
}
{
  <copy-paste of long proof>
}

有没有办法避免这种复制粘贴并保持交互性，例如通过编写类似于以下内容的内容？

induction x.
{
  admit.
}
all:
{
  <long proof>
}

Answer 1

有时您可以使用中间引理解决这些目标：

assert (H : statement_of_lemma).
{ 
  proof...
}

稍后，您只需将H 应用于每个子案例。