帰納的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タイプのように、1つのコンストラクタとユニバーサル定量化を使用して定義されたので、あなたのsusbtringタイプがいくつかの点で「実存」のようだということは驚くべきことではありません。

もちろん、existsを使用してタイプを定義でき、Inductiveは必要ありません。

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