如何定義一般參數N:nat,N個元素的有限集合$ A_ {0},... A_ {N-1} $? 有沒有一種優雅的方式來做到遞歸定義?有人能夠將我推薦爲關於這種結構的推理嗎?如何定義Coq中N個元素的有限集合?
1
A
回答
5
一個非常方便的解決方案是定義n
次序,'I_n
作爲記錄:
Definition ordinal n := {
val :> nat;
_ : val < n;
}.
也就是說,一對的自然數,加上一個證明,這樣的自然數小於n
,其中< : nat -> nat -> bool
。在這裏使用可計算的比較運算符是非常方便的,尤其意味着證明本身不是非常「重要的」,這正是您通常想要的。
這是math-comp使用的解決方案,它具有良好的性能,主要注入的val
,val_inj : injective val
,這意味着你可以重複使用最標準的操作在nat
與您的新的數據類型。請注意,您可能希望將添加定義爲add i j := max n.-1 (i+j)
或(i+j) %% n
。
此外,上面鏈接的庫提供了使用有限類型的一般定義,包括將它們映射到它們的基數序號。
+0
不應該是'記錄序號n'嗎? – jaam
相關問題
- 1. 如何在打字稿中定義5個元素的有限集合?
- 2. 類型包含Coq中的N個元素的所有功能
- 3. 從集合中取出n個元素
- 4. 如何在Coq中定義非空集?
- 5. 獲得集合的第n個元素
- 6. 如何從集合中返回N個連續的元素?
- 7. 如何從集合中跳過第n個元素?
- 8. 在Coq中,如何定義一個像A = {x |的集合f(x)= 0}?
- 9. 如何生成數組中所有n個元素的組合?
- 10. 如何在Java中遞歸地生成N元素集合中的所有k元素子集
- 11. 如何定義第一個元素不是n = 0的向量?
- 12. 如何將一個元素及其所有元素放入一個集合中?
- 13. 我如何找到一個集合的所有子集,正好有n個元素?
- 14. 從陣列中省略'N'個元素集合
- 15. WPF如何綁定到集合中的特定元素
- 16. 6SUM:給定n個整數的集合S,是否有S的子集,正好有6個元素,總和爲0?如何比O(n^3)做得更好?
- 17. Agda有限集的定義
- 18. k個元素的全部組合n
- 19. 確定當前元素是集合的最後一個元素?
- 20. 'else'的定義 - Coq
- 21. Mysql:獲得N個記錄的給定子集的n個元素
- 22. 從集合ArrayList中返回一個元素,其中每個集合具有不同的元素類型
- 23. 朱莉婭:具有替換的n個元素的唯一集合
- 24. 如何更新另一個集合內的集合中的元素?
- 25. 如何檢查自定義集合中元素的java數據類型?
- 26. 查找n個k個元素的所有組合
- 27. 從大的MongoDB集合中選擇每個第N個元素w/PHP?
- 28. 如何在Coq中寫入沒有參數的定義?
- 29. 有沒有辦法搜索集合中的每個元素c#
- 30. 如何有效地追蹤集合中最小的元素?
請參閱標準庫的['Fin.t'](https://coq.inria.fr/library/Coq.Vectors.Fin.html#t)獲取遞歸定義。 –
是的,我喜歡。我正在尋找更簡單的東西,沒有這麼大的依賴關係 – kakaz
什麼是大量的依賴關係?對不起,我沒跟着。它在標準庫中。如果您不想導入模塊,可以複製定義。當然,這不是一個簡單的類型,不像ejgallego的建議。 –