coq - 当目标是 Type 时，为什么 Coq 不允许反转、破坏等？

Question

当refine在一个程序中，我试图通过 inversion 结束证明在 False假设当目标是 Type .这是我尝试做的证明的简化版本。

Lemma strange1: forall T:Type, 0>0 -> T.
  intros T H.
  inversion H.  (* Coq refuses inversion on 'H : 0 > 0' *)

Coq 提示

Error: Inversion would require case analysis on sort 
Type which is not allowed for inductive definition le

但是，由于我对 T 什么也没做，应该没关系，...或者？

我摆脱了T像这样，证明通过了:

Lemma ex_falso: forall T:Type, False -> T.
  inversion 1.
Qed.  

Lemma strange2: forall T:Type, 0>0 -> T.
  intros T H.
  apply ex_falso.  (* this changes the goal to 'False' *)
  inversion H.
Qed.

Coq 提示的原因是什么？难道只是inversion的不足之处吗？ , destruct ， 等等。 ？

Answer 1

我以前从未见过这个问题，但这是有道理的，尽管有人可能会争辩说这是 inversion 中的一个错误。 .

这个问题是由于inversion通过案例分析来实现。在 Coq 的逻辑中，如果结果是计算性质的(即，如果返回的事物的类型是Prop)。这样做的一个原因是 Coq 的设计者希望在以合理的方式将它们提取到代码中时，可以从程序中删除证明参数:因此，只有当被破坏的东西不能改变结果。这包括:

没有构造函数的命题，例如 Type .

只有一个构造函数的命题，只要该构造函数不接受计算性质的参数。这包括 False , True (用于进行有根据的递归的可访问性谓词)，但不包括存在量词 Acc .

但是，正如您所注意到的，可以通过将要用于产生结果的某些命题转换为另一个可以直接进行案例分析的命题来规避该规则。因此，如果你有一个矛盾的假设，比如你的情况，你可以先用它来证明 ex (这是允许的，因为 False 是 False )，然后消除 Prop产生你的结果(这是上述规则所允许的)。

在您的示例中，False仅仅因为它不能对 inversion 类型的东西进行案例分析而放弃，这太保守了。在这种情况下。诚然，它不能直接按照逻辑规则对其进行案例分析，如上所述；但是，人们可以考虑对 0 < 0 进行更智能的实现。认识到我们正在消除一个矛盾的假设并添加 inversion作为中间步骤，就像您一样。不幸的是，似乎我们需要手动完成这个技巧才能使其工作。