在Coq中将非A转换为A-> False

Question

我想通过假设not A并找到A来证明False。将目标not A转换为A -> False的最短，最通用的方法是什么？

我尝试过exfalso，但没有将A添加到我的假设中...

Answer 1

最快的方法是执行intro x，它将获得x : A。not A实际上定义为A -> False，因此它已经是您想要的：

not = fun A : Prop => A -> False
     : Prop -> Prop

如果您真的想将目标更改为A -> False，unfold not就可以了。

最后exfalso是用False替换当前目标的策略。目的是说明当前上下文不一致。