当目标是类型时，为什么Coq不允许反转，破坏等？ [英] Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?

问题描述

在精炼程序时，我尝试通过 inversion 在上结束证明当目标是类型 时，错误的假设。这是我尝试做的证明的简化版本。

When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do.

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

但是，因为我对<$ c $不做任何操作c> T ，没关系，...或？

However, since I do nothing with T, it shouldn't matter, ... or ?

我摆脱了 T 这样，证明就通过了：

I got rid of the T like this, and the proof went through:

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抱怨的原因是什么？仅仅是反转，破坏等的缺陷吗？

What is the reason Coq complained? Is it just a deficiency in inversion, destruct, etc. ?

推荐答案

我以前从未见过此问题，但这是有道理的，尽管有人可能会认为这是 inversion 。

I had never seen this issue before, but it makes sense, although one could probably argue that it is a bug in inversion.

此问题是由于案例分析实现了 inversion 的事实。按照Coq的逻辑，通常不能根据对逻辑假设进行案例分析（即，类型为 Prop ），如果结果是计算性质的（即，如果要返回的事物的类型是 Type ）。原因之一是Coq的设计人员希望以合理的方式将程序中的证明参数提取到代码中时，可以从程序中删除这些证明参数：因此，只允许对假设进行案例分析，以在计算结果时产生某种计算结果。被破坏的事物不能改变结果。这包括：

This problem is due to the fact that inversion is implemented by case analysis. In Coq's logic, one cannot in general perform case analysis on a logical hypothesis (i.e., something whose type is a Prop) if the result is something of computational nature (i.e., if the sort of the type of the thing being returned is a Type). One reason for this is that the designers of Coq wanted to make it possible to erase proof arguments from programs when extracting them into code in a sound way: thus, one is only allowed to do case analysis on a hypothesis to produce something computational if the thing being destructed cannot alter the result. This includes:

1. 没有构造函数的命题，例如 False 。


2. 只有一个构造函数的命题，只要该构造函数不接受计算性质的参数即可。其中包括 True ， Acc （用于进行有根据的递归的可访问性谓词），但不包括存在量词 ex 。

1. Propositions with no constructors, such as False.
2. Propositions with only one constructor, as long as that constructor takes no arguments of computational nature. This includes True, Acc (the accessibility predicated used for doing well-founded recursion), but excludes the existential quantifier ex.

但是，您可能会规避该规则通过将您想要用于产生结果的某些命题转换为另一个命题，您可以直接进行案例分析。因此，如果您有一个自相矛盾的假设（例如您的情况），则可以首先使用它来证明 False （这是允许的，因为 False 是 Prop ），然后 then 消除 False 来产生您的结果（上述规则允许）。

As you noticed, however, it is possible to circumvent that rule by converting some proposition you want to use for producing your result to another one you can do case analysis on directly. Thus, if you have a contradictory assumption, like in your case, you can first use it to prove False (which is allowed, since False is a Prop), and then eliminating False to produce your result (which is allowed by the above rules).

在您的示例中，反转过于保守只是因为它无法对类型 0<在这种情况下为0 。如上所述，确实不能直接通过逻辑规则对其进行案例分析；但是，可以想到对 inversion 进行更智​​能的实现，该实现认识到我们正在消除矛盾的假设，并添加了 False 作为中间步骤，就像您所做的一样。不幸的是，似乎我们需要手工做这个技巧才能使它起作用。

In your example, inversion is being too conservative by giving up just because it cannot do case analysis on something of type 0 < 0 in that context. It is true that it can't do case analysis on it directly by the rules of the logic, as explained above; however, one could think of making a slightly smarter implementation of inversion that recognizes that we are eliminating a contradictory hypothesis and adds False as an intermediate step, just like you did. Unfortunately, it seems that we need to do this trick by hand to make it work.

这篇关于当目标是类型时，为什么Coq不允许反转，破坏等？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！