coq - 用Coq重写假设，保持含义

我正在做一份合格证明。我将P -> Q作为假设，并将(P -> Q) -> (~Q -> ~P)作为引理。如何将假设转换为~Q -> ~P？

当我尝试对其进行apply编码时，我只是生成了新的子目标，这没有帮助。

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

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

并以

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

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

最佳答案

这不只是apply那样优雅，但是您可以使用pose proof (lemma _ _ H) as H0，其中lemma是引理的名称。这将为上下文添加另一个具有正确类型的假设，名称为H0。

关于coq - 用Coq重写假设，保持含义，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47520531/