Случайные типы потоков и подмножества в Coq

Question

Yo!

Мне нужен случайный поток натов с гарантированным типом подмножества, например 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.