coq - 如何证明相同的子目标

Question

我有两个相同的子目标，如下所示：

prove_me (x::xs) = true

---

prove_me (x::xs) = true

证明将是平等的。如何使用第一个目标解决第二个目标？

Answer 1

您不能从字面上将一个目标的证明重用于另一个目标，但您可以证明一个辅助引理：

assert (H : prove_me (x::xs) = true).
{ (* proof of result *) }

然后，您可以H在两个子目标出现后将其释放。