The Coq mailing list

[Allyx FONTAINE <fontaine AT labri.fr>]

Thank you Pierre for your answer.

That's exactly it. Before launching into probability evaluations, I 
would like to test my functions.

You speak about translations. Does that mean that, instead of using the 
Coq extraction command, I'll have to translate my Coq function using the 
existant randomized Ocaml functions  (I am not really familiar with code 
extraction)?

Allyx

Le 20/05/2011 17:48, Pierre Corbineau a écrit :
> Dear Allyx,
>
> Within Coq, all you can do with Alea distrs is evaluate the 
> probability of a certain (computable) event to happen by using the mu 
> function (which is actually a projection). This probably isn't what 
> you want.
>
> I think you might try to extract Alea Functions to a randomized Ocaml 
> program using the following translation:
>
>
> Distr A => 'a distr == unit -> 'a (random function)
>
> let draw d = d ();;
>
> Flip => (Random.bool: bool distr)
>
> Munit => fun x => fun () => x :'a -> 'a distr
>
> Mlet => fun d f => f (draw d) : 'a distr -> (a' -> 'b distr) -> 'b distr
>
>
> Maybe another Pierre can help you there...
>
> Pierre Corbineau
>
>
>
> Le 20/05/2011 17:24, Allyx FONTAINE a écrit :
> > 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