归纳Coq定义中存在量词与全称量词的关系

Question

假设我想要一个子字符串的归纳定义(string只是list的同义词)。

Inductive substring {A : Set} (w : string A) :
                    (string A) -> Prop :=
  | SS_substr : forall x y z : string A,
                  x ++ y ++ z = w ->
                  substring w y.

在这里我可以举例证明如下:

Theorem test : substring [3;4;1] [4].
Proof.
  eapply SS_substr.
  cbn.
  instantiate (1:=[1]).
  instantiate (1:=[3]).
  reflexivity.
Qed.

然而，证明是"存在的"而不是"全称的"，尽管归纳定义陈述了forall x y z，然后才限制了它们的形状。这对我来说似乎有些不直观。到底发生了什么事?

还有，是否可以用exists x : string A, exists y : string A, exists z : string, x ++ y ++ z = w -> substring w y做一个归纳定义?

Answer 1

需要注意的重要一点是，exists不是Coq的内置功能(与forall相反)。实际上，exists本身是一个符号，但后面有一个名为ex的归纳类型。表示法和归纳类型在Coq标准库中定义。下面是ex的定义:

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
    ex_intro : forall x:A, P x -> ex (A:=A) P.

它是使用一个构造函数和一个通用量化定义的，就像你的substring类型一样，所以你的susbtring类型在某些时候似乎是"存在的"，这并不奇怪。

当然，你可以使用exists来定义你的类型，你甚至不需要Inductive。

Definition substring' {A : Set} (w y : string A) : Prop :=
    exists x z, x ++ y ++ z = w.