coq - 归纳 Coq 定义中存在量词和全称量词之间的关系

Question

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

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 standard library 中定义。 。以下是 ex 的定义:

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

它是使用一个构造函数和通用量化来定义的，就像您的 substring 类型一样，因此您的 susbtring 类型在某些方面似乎是“存在的”也就不足为奇了点。

当然，您可以使用 exists 定义类型，甚至不需要 Inducing。

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