Coq中的随机nat流和子集类型 [英] Random nat stream and subset types in Coq

问题描述

是的！

我需要一个随机的nat流，其中包含子集类型的保证，例如，该流只会给出0< nat< 10 。有人帮我解决这个问题吗？

I need a random stream of nats with guaranteed subset types, like this stream will only give 0 < nat < 10. Anyone up for helping me with this?

我发现此函数可以生成随机数：

I found this function for generating random numbers:

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

我想用任何子集替换 Z 类型，例如

I want to replace Z with any subset type, e.g.

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 。

Now the problem is that Zmod does accept Z but not Z_gt0.

我必须重新定义所有功能？还是已经有可以使用的库函数？

Do I have to redefine all functions? Or is there already a library function ready to use?

要修改：请为子集类型或优化类型添加标签。

TO MOD: Please add a tag for subset-types or refinement-types.

推荐答案

与您的类型有关的问题是 Zmod种子n2 是可以为0的正整数，因此 seed'可以为0，这意味着 seed'* n1 也可以为0。

The issue with your type is that Zmod seed n2 is a positive integer that can be 0, so seed' can be 0, which means that seed' * n1 can be 0 too.

最后，您的 CoFixpoint 是无法键入的，种子应该在某些 Z_ge0 类型，而不是 Z_gt0 。

In the end your CoFixpoint is not typable, the seed should be in some Z_ge0 type, not in Z_gt0.

编辑：要回答有关库的部分，您可能会感兴趣正类型，它是严格大于0的二进制整数。实际上， Z 定义为：

to answer the part about the library, you might be interested by the positive type, which is the type of binary integer strictly greater than 0. In fact, Z is defined as:

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

但是问题仍然相同：取正整数可以避开正，因为您可以以0结尾。

However the problem is still the same: taking the modulo of positive integer can escape positive since you can end up with 0.

这篇关于Coq中的随机nat流和子集类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！