在 Coq 中将 `not A` 转换为 `A -> False`

【问题标题】：Transform `not A` into `A -> False` in Coq在 Coq 中将 `not A` 转换为 `A -> False`
【发布时间】：2019-09-28 11:53:17
【问题描述】：

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

我尝试了exfalso，但它并没有在我的假设中添加A...

【问题讨论】：

【解决方案1】：

最快的方法是intro x，它会给你x : A。 not A实际上定义为A -> False，所以已经是你想要的了：

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

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

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

【讨论】：