The Coq mailing list

[Allyx FONTAINE <fontaine AT labri.fr>]

Thanks a lot ! So I'll have a look at all those functionnalities.

Allyx

Le 20/05/2011 19:30, AUGER Cedric a écrit :
> 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