coq - Coq 需要什么才能为 Inductive 类型生成消除组合器？

Question

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 非常相似的不同类型的消除组合器，但不知道如何构造它。

Answer 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.

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