coq - 引用 Coq 中先前证明的结论的证明

Question

假设我要证明一个等价关系:

P <-> Q

我已经设法证明了蕴涵部分:

P -> Q

但是当我试图证明另一个方向时，那就是

Q -> P

事实证明，我需要使用 P -> Q .我可以问一下，组织证明需要在上面几行中立即得出结论的策略是什么？

Answer 1

您可以从 assert 开始在拆分等价之前 P <-> Q :

Goal forall P Q, P <-> Q.
Proof.
intros P Q.
assert (PimpliesQ : P -> Q).
{  admit. (* your proof *)
}
split; [assumption|].