歸納式Coq定義中存在變量和通用量詞之間的關係

假設我想要一個子串的歸納定義（字符串只是列表的同義詞）。歸納式Coq定義中存在變量和通用量詞之間的關係

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進行歸納定義？

來源

2016-11-08 AntlerM

需要注意的一點是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來定義您的類型，而您甚至不需要Inductive。

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

來源

2016-11-08 09:26:00 eponier

整潔，謝謝！（Jibadiba podajiba brm brm brm - 需要更多的字符） – AntlerM

@AntlerM即使我回答了你最初的問題，你應該等我的文章選擇爲解決方案之前，因爲它可能會阻止其他用戶發表一些有趣的主題。 – eponier

那麼，對我而言，這是有道理的，存在主義肯定遵循普遍的（當然，如果x中的A，P x則存在x'：A，P x'假設A不是空的），這就解釋了我想知道的所有事情關於;他說，正如其他人可能在某個時候偶然發現的那樣，爲這個問題留下更多「興趣」的空間似乎是合理的。可悲的是，我不能用13個代表把你放在船上:)。 – AntlerM

歸納式Coq定義中存在變量和通用量詞之間的關係

回答

相關問題