coq - Coq：处理不等式 (<>)

Question

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

• 当<>存在于目标中时，doingintros contra.将目标更改为False并将目标移至假设，但<>切换为=。我想我理解它的声音。如果我有 as 目标a <> b，那么a = bas 假设会产生矛盾。

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

• When <>is in a hypothesis H，doingdestruct H.将删除该假设（我不能这样做destruct (H) eqn:H.），它会将任何目标切换到相同H但使用<>switched for =。我不明白这里的逻辑。如果我有一个不等式的假设，我不明白没有它与将平等作为目标是一样的。

  不等式如何归纳使用destruct？

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

所以，事实上，我有 4 个相关的问题用粗体标记。

标签： coqprooftheorem-provingcoq-tactic

Answer 1

这intros[on a goal a = b] 在逻辑上合理吗？

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

不等式如何归纳使用destruct？

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

为什么不能像inversion G.对假设那样做类似的事情S n = 0？

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