如何在Coq中定義非空集？

Question

嘗試在完成許多教程之後創建我的第一個Coq定義。想知道如何定義簡單的字母表，如果定義如下：

Σ是一個字母iff它是一個有限的非空符號集。

得到這麼多：

Require Import Coq.Lists.ListSet. 

Definition alphabet := set. 

但你如何指定「必須是有限的，非空集」的一部分？

Answer 1

既然你選擇你alphabet是set，它在定義上是有限的，因爲set被定義爲list一個實例，歸納類型總是有限的。

您使用的定義ListSet庫emptyset所以你的第一選擇將是指出

Definition not_empty (a: alphabet) : Prop := a <> empty_set. 

或者你可以依靠的事實，你的一套是list和模式匹配的表達式：

Definition not_empty (a: alphabet) : bool := match a with 
    | nil => false 
    | _ => true 
end. 

（您也可以使用False和True來定義後者在Prop而不是bool。）

編輯：一些澄清亞瑟問（簡化這裏，抓住真正的課本約歸納類型，如果你想要一個更精確的解釋）：

：

的感應式可以通過居住

• 有限數量的元件（例如，bool）的，
• 元件的無限數量（例如，nat）
• 根本沒有元素（例如False）。

但是，任何電感類型的元素都是通過構造有限的。例如，您可以通過編寫有限次數的構造函數S來編寫任何自然數，但是您的有可以在某個點使用O，並「停止」構建術語。列表也一樣：你可以建立一個任意長列表，但其長度總是有限的。