8

在编写程序时refine，我试图inversion在目标是. 这是我尝试做的证明的简化版本。FalseType

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？

4

2 回答 2

9

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

这个问题是由于inversion通过案例分析来实现的。在 Coq 的逻辑中，如果结果是某种计算性质的事物（即，如果返回的事物的类型是 a ），则通常不能对逻辑假设（即类型为 a 的事物）进行案例分析。这样做的一个原因是，Coq 的设计者希望在以合理的方式将证明参数从程序中提取到代码中时，可以删除它们：因此，仅允许对假设进行案例分析以产生计算结果，如果被破坏的东西不能改变结果。这包括：PropType

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

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

在您的示例中，inversion仅仅因为在这种情况下无法对某种类型的事物进行案例分析就放弃了，这太保守了0 < 0。诚然，它不能直接按照逻辑规则对其进行案例分析，如前所述；然而，人们可以考虑做一个稍微更聪明的实现，inversion它承认我们正在消除一个矛盾的假设，并False作为中间步骤添加，就像你做的那样。不幸的是，似乎我们需要手动完成这个技巧才能使其发挥作用。

于 2014-12-05T21:15:22.397 回答
0

除了 Arthur 的回答之外，还有一个使用constructive_defined_description公理的解决方法。在函数中使用这个公理将不允许执行计算并从中提取代码，但它仍然可以用于其他证明：

From Coq Require Import Description.

Definition strange1: forall T:Type, 0>0 -> T.
  intros T H.
  assert (exists! t:T, True) as H0 by inversion H.
  apply constructive_definite_description in H0.
  destruct H0 as [x ?].
  exact x.
Defined.

或无校样编辑模式的相同功能：

Definition strange2 (T: Type) (H: 0 > 0): T :=
  proj1_sig (constructive_definite_description (fun _ => True) ltac: (inversion H)).

还有一个更强的公理constructive_indefinite_description将一个命题exists x:T, P x（没有唯一性）转换为相应的 sigma-type {x:T | P x}。

于 2022-01-24T13:00:39.823 回答