Coq:处理不等式 (<>)

Question

我试图理解在 Coq 中处理不等式的逻辑。

当<>存在于目标中，执行 intros contra.将目标更改为 False并将目标移至假设，但使用 <>切换到 = .我想我理解它的声音。如果我有目标a <> b ，然后 a = b因为假设会产生矛盾。

但是，我不能在 Coq 中做相反的事情。如果我有目标a = b , 我不能 intros contra.为了拥有False作为目标和a <> b作为假设。 这个intros合乎逻辑吗？是否因为从不需要完成证明而不受支持？

当<>在一个假设中 H , 做 destruct H.将删除假设(我做不到 destruct (H) eqn:H. )，它将任何目标切换到与 H 相同的目标但与 <>切换到 = . 我不明白这里的逻辑 .如果我有一个不等式的假设，我不明白没有它与将平等作为目标是一样的。

destruct 使用不等式是如何归纳的?

如果我有一个矛盾的假设 G 0 <> 0 ，为了完成证明并告诉它是矛盾的，我需要做destruct G. (* now the goal is 0 = 0 *). reflexivity. 为什么不能只做 inversion G. 之类的事情？ ，就像你对假设所做的那样 S n = 0 ?.

所以我实际上有 4 个相关问题标记为 粗体 .

Answer 1

Would this intros [on a goal a = b] be logically sound?

如果我理解你的问题，你想知道是否有可能
有一个目标 a = b , 调用 intros contra ，并将其转换为目标 H : a <> b |- False .这是合理的，但在 Coq 的 a 的基本构造逻辑中是不可推导的。和 b任意类型:它断言命题 a = b支持双重否定消除 ( ~ (~ a = b) -> a = b)。 Coq 不支持这一点，因为这意味着以不同的逻辑形式工作。

How an inequality is inductive to be used by destruct?

正如 yeputons 所说， a <> b定义为 a = b -> False ，并且虚假被归纳定义为没有构造子的命题；因此，破坏 False 类型的东西简单地完成了证明。此外，调用 destruct在 A -> B 类型的东西上大致具有生成 A 类型目标的效果, 将该证明输入到蕴涵中以获得 B 的证明，然后调用 destruct在 B 的证明上.就您而言，这意味着完全按照您的描述进行操作。

Why is it not possible to just do something like inversion G., as you would do with an hypothesis S n = 0?

我的猜测是 inversion不像 destruct那么宽大，并且没有扩展到我上面解释的含义上。