coq - `omega` 在这里到底做了什么？

Question

这个证明可以用一个omega来完成:

  a : Z
  b : Z                                                                                               
  H : a > 1
  H0 : b > 1
  H1 : b = 1                                                                                          
  H2 : a mod b = 0
  ============================
   False

这是为什么呢？ omega 在这里到底做了什么？既然H0和H1相互矛盾，难道就不能证明什么吗？另外，这可以在没有omega的情况下证明吗？怎么办？

Answer 1

1- 这里，omega意识到H0和H1是矛盾的，并使用它们来产生 False 的证明。通过重写 H1 直接显示这一点应该不难。进入H0 (结果为 1 > 1 )，然后应用一些引理来表明 a > b -> a <> b ，结果为1 <> 1 ，然后应用于我们的目标，产生一个新目标 1 = 1 ，可通过 reflexivity 放电。很难描述如何 omega工作原理很详细，因为它背后有一个复杂的算法，可以处理一大类相似的目标(粗略地说，Presburger arithmetic)

2- 是的。 H0和H1可以用来证明任何事情，包括False 。这有时称为 Principle of explosion 。但请注意，您只能证明特定上下文内的任何内容。。换句话说，并不是因为您在某些证明上下文中存在矛盾，您就能够证明任何其他。