我正在做 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, where lemma是你的引理的名字。这将向上下文中添加另一个具有正确类型的假设，其名称为H0.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
