Coq中的随机nat流和子集类型

Question

Yo！

我需要一个具有保证子集类型的随机nat流，比如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。

EDIT：要回答关于库的部分，您可能对positive类型感兴趣，它是严格大于0的二进制整数的类型。事实上，Z被定义为：

Inductive Z : Set :=
    Z0 : Z (* 0 *)
  | Zpos : positive -> Z (* z > 0 *)
  | Zneg : positive -> Z (* z < 0 *)

然而，问题仍然是一样的：取正整数的模可以转义positive，因为你最终可以得到0。