Random nat streams and subset types in Coq

Question

Yo!

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

I found this function to generate random numbers:

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

I want to replace Z with any type of subset, like

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

So we have:

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

Now the problem is that Zmod accepts Z , but not Z_gt0 .

Do I need to redefine all functions? Or is there already a library ready for use?

TO MOD: Add a tag for subset types or refinement types.

Answer 1

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

In the end, your CoFixpoint not typical, the seed should be in some Z_ge0 , and not in Z_gt0 .

EDIT: to answer part of the library, you might be interested in the positive type, which is a binary integer type 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 *) 

However, the problem is the same: taking modulo a positive integer can exit positive , since you can get 0.