Coq中的隨機nat流和子集類型

Question

喲！

我需要一個有保證子集類型的nats隨機流，如this stream will only give 0 < nat < 10。有人幫我做這個？

我發現這個函數用於產生隨機數：

CoFixpoint rand (seed n1 n2 : Z) : Stream Z := 
    let seed' := Zmod seed n2 in Cons seed' (rand (seed' * n1) n1 n2). 

我想與任意子集類型，例如以取代Z

Definition Z_gt0 := { Z | Z > 0}. 

因此，我們有：

CoFixpoint rand (seed n1 n2 : Z_gt0) : Stream Z_gt0 := 
    let seed' := Zmod seed n2 in Cons seed' (rand (seed' * n1) n1 n2). 

現在的問題是，Zmod不接受Z但不Z_gt0。

我是否必須重新定義所有功能？還是已經有一個庫函數可以使用了？

TO MOD：請爲子集類型或優化類型添加標籤。

Answer 1

你的類型的問題是Zmod seed n2是一個正整數，可以是0，所以seed'可以是0，這意味着seed' * n1也可以是0。

最後您的CoFixpoint是不可分類的，種子應該在Z_ge0類型中，而不是Z_gt0。

編輯：回答有關庫中的一部分，你可能有興趣在positive類型，它是二進制整數嚴格大於0其實更大的類型，Z被定義爲：

​​

然而，問題仍然是一樣的：取正整數的模可以跳過positive，因爲最終可能爲0.