当目标是一个类型时,为什么Coq不允许反转,破坏等？

Question

当refine一个程序,当我的目标是a时,我试图通过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的逻辑中,如果结果具有计算性质(即,如果返回的事物的类型是a ),则通常不能对逻辑假设(即,类型为a的事物Prop)执行案例分析Type.这样做的一个原因是Coq的设计者希望能够在以一种合理的方式将代码提取到代码中时从程序中删除证明参数:因此,只允许对假设进行案例分析以产生一些计算,如果被破坏的东西不能改变结果.这包括:

1. 没有构造函数的命题,例如False.
2. 只有一个构造函数的命题,只要该构造函数不带有计算性质的参数.这包括True,Acc(可访问性预测用来做有根有据递归),但不包括存在量词ex.

然而,正如您所注意到的那样,通过将您想要用于生成结果的某个命题转换为另一个可以直接进行案例分析的命题,可以规避该规则.因此,如果你有一个矛盾的假设,就像在你的情况下,你可以先用它来证明False(这是允许的,因为False是a Prop),然后消除False产生你的结果(这是上述规则所允许的).

在你的例子中,inversion放弃是过于保守,因为它无法0 < 0对该上下文中的某些类型进行案例分析.确实,它不能直接通过逻辑规则对其进行案例分析,如上所述; 然而,人们可以想到做一个稍微聪明的实现inversion,认识到我们正在消除一个矛盾的假设,并添加False为中间步骤,就像你一样.不幸的是,似乎我们需要手动完成这个技巧才能使其发挥作用.