The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 20 May 2011 19:20:56 +0200,
Allyx FONTAINE 
<fontaine AT labri.fr>
 a écrit :

> 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)?

I wrote some tutorial on extraction here[1] (but I guess it is not a
good one to start)

What Pierre mean, AFAIU, is that you may want to have some extraction
of axiom to do what you want.

Record distr (A:Type) : Type := 
  {μ : M A;
   mu_stable_inv : stable_inv μ; 
   mu_stable_plus : stable_plus μ;
   mu_stable_mult : stable_mult μ;
   mu_continuous : continuous μ}.

Definition Flip : distr bool.

is not good for you to test, as it won't provide dices throws.
If you want to test with some Monte-Carlo methods or so, you will need
to have a dice trower, and tell coq to use it instead of your "distr"
which only computes probabilities.

For that you can try:

Extract Constant distr => "unit -> 'a".
Extract Inductive bool => "bool" ["true" "false"].
Extract Constant Flip => "Random.bool".

And so on, but if you are not familiar to extraction I would not advise
you to do so; maybe have a try on simpler libraries for extraction
before venturing forth.

So for an answer, you only have to use extraction, but you need to take
a look at all the functionnalities of the extraction mechanism (and
know of the OCaml functions and types to inform the extractor).

[1] http://coq.inria.fr/cocorico/AUGER_ExtractionTuto

> 
> 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
> >
>