Coq 需要什么来为 Inductive 类型生成消除组合器？答案

【问题标题】：What is required for Coq to generate an elimination combinator for an Inductive type?Coq 需要什么来为 Inductive 类型生成消除组合器？
【发布时间】：2016-09-29 11:39:55
【问题描述】：

Coq 的 Finite_sets 库有一个归纳类型，指定某个集成是有限的：

Inductive Finite : Ensemble U -> Prop :=
| Empty_is_finite : Finite (Empty_set U)
| Union_is_finite :
  forall A:Ensemble U,
    Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).

我试图证明有限集合中的成员资格可按如下方式确定：

Lemma Finite_dec (A:Type) : forall f:Ensemble A, Finite A f ->
  forall x:A, {In A f x} + {~In A f x}.
Proof.
intros.
induction H.

但是，Coq 会产生以下错误消息：

Cannot find the elimination combinator Finite_rec, the
elimination of the inductive definition Finite on sort Set is
probably not allowed.

我的问题是，为什么 Coq 不能为 Finite 生成消除组合器？要使这成为可能，需要什么归纳类型？

注意：我需要一个用于不同类型的消除组合器，它与 Finite 非常相似，但不知道如何构造它。

【问题讨论】：

在这种情况下，特殊的问题是Finite inductive 是 prop 类型，因此您无法从中提取“真实”信息，而您的可判定性是。如果您将目标更改为In A f x \/ ~In A f x，它将通过。您可以通过不同的假设获得结果，但我会特别使用其他方法，即将我的有限集编码为带有商的列表。
在this 回复相关question Arthur Azevedo De Amorim 完美地解释了原因。只需在他的解释中将inversion 替换为induction。
谢谢，但我需要 sumbool 才能在我定义的函数中使用引理，因此仅对命题证明它是不够的。

标签： coq

【解决方案1】：

正如@ejgallego 指出的那样，一个问题是您不能对诸如Finite 之类的命题进行归纳，以获得诸如{P} + {~ P} 之类的计算。然而，还有一个更深层次的问题：如果不假设某种排中形式，您的结果是不可证明的，因为这意味着所有类型都具有可判定的相等性。

Goal (forall (A : Type) (f : Ensemble A),
        Finite A f -> forall x, In A f x \/ ~ In A f x) ->
     forall (A : Type) (x y : A), x = y \/ x <> y.
Proof.
intros fin_dec A x y.
assert (fin : Finite A (Add A (Empty_set A) x)).
{ apply Union_is_finite.
  - apply Empty_is_finite.
  - intros []. }
specialize (fin_dec _ _ fin y).
destruct fin_dec as [H | H].
- destruct H.
  + destruct H.
  + destruct H. now left.
- right.
  contradict H. rewrite H. right. constructor.
Qed.

如果您不想使用额外的公理，我建议您使用列表而不是集成库，并使用具有可判定相等性的类型。

【讨论】：

我意识到了可判定相等性的问题，但试图只为具有可判定相等性的类型证明这一点仍然使我处于无法证明该属性的状态。尽管我可以按照上面的建议更改为列表，但我仍然想知道是否有可能证明使用像 Finite 这样的东西，即使仅适用于具有可判定相等性的类型。

【解决方案2】：

在尝试了一些东西之后，我从其中一条错误消息中得到了一些启发

Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs

这给了我尝试将返回类型从 Prop 更改为 Type 的灵感。在这种情况下，我可以调用归纳法，下面的证明很简单。

Inductive Finite (U:Type) : Ensemble U -> Type :=
| Empty_is_finite : Finite U (Empty_set U)
| Union_is_finite :
  forall A:Ensemble U,
    Finite U A -> forall x:U, ~ In U A x -> Finite U (Add U A x).

Definition eq_dec (U:Type) : forall x y:U, {x=y} + {x<>y}.

Lemma Finite_dec (A:Type) : forall f:Ensemble A, Finite A f ->
  forall x:A, {In A f x} + {~In A f x}.
Proof.
intros.
induction X.

虽然我不完全明白其中的原因。

【讨论】：

This 可能会为您澄清一些事情。