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如何归纳不等式？

  如果我有一个矛盾的假设G0 <> 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 类型的东西就可以简单地完成证明。此外，对 A -> B 类型的对象调用 destruct 大致会产生一个 A 类型的目标，将该证明输入到蕴涵中以获得 B 的证明，然后在 B 的证明上调用 destruct。在您的情况下，这意味着完全按照您的描述进行操作。

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

我的猜测是 inversion 不像 destruct 那样宽松，并且没有像我上面解释的那样扩展到处理影响。