The Coq mailing list

[Allyx FONTAINE <allyx.fontaine AT labri.fr>]

Hello,

Is there a way to test (complex) functions based on monads used in the 
alea library for randomized algorithm ? I want to know if the functions 
I make really corresponds to what I expect them to do before starting to 
analyze them.

For example, I want to produce a list of bits generated by a coin flip. 
I want to stop it as soon as true is flipped. I made this function below :

Add LoadPath "../alea-v5".
Require Export Prog.
Require Import List.

Instance Test_mon :
  monotonic (fun (f: (list nat) -> distr (list nat)) (x: (list nat)) =>
      (Mif Flip (f (1%nat::x)) (Munit (0%nat::x)))).
red;intros;intro p;apply Mif_le_compat;auto.
Qed.

Definition Test : ((list nat) -> distr (list nat)) -m> ((list nat) -> 
distr (list nat)) :=
  mon (fun (f: (list nat) -> distr (list nat)) (x: (list nat)) =>
  (Mif Flip (f (1%nat:: x)) (Munit (0%nat::x)))).

This function stops when a false is flipped (and not true as I wanted). 
Is there a means to detect this error ? Are some possible outputs be 
computed ?

Thanks in advance,
Allyx