coq - 用 Coq 重写假设，保留蕴涵

Question

我正在做 Coq 证明。我将 P -> Q 作为假设，将 (P -> Q) -> (~Q -> ~P) 作为引理。如何将假设转化为~Q -> ~P？

当我尝试应用它时，我只是产生新的子目标，这没有帮助。

换句话说，我希望从以下开始:

P : Prop
Q : Prop
H : P -> Q

最终得到

P : Prop
Q : Prop
H : ~Q -> ~P

给定上面的引理 - 即(P -> Q) -> (~Q -> ~P)。

Answer 1

这不像apply那么优雅，但您可以使用姿势证明(引理_ _ H)作为H0，其中引理 > 是你的引理的名称。这会将另一个具有正确类型的假设添加到上下文中，名称为 H0。