The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I did it.

> Lemma continuous2_app : forall `{c1:cpo D1} `{c2:cpo D2} `{c3:cpo D3}

>            (F : D1 -m> D2 -m> D3) {cF:continuous2 F} (k:D1), continuous (F k).

> red; intros.

> transitivity  (F (mlub (cte nat k))  (lub h)); auto.

> transitivity (lub ((F @2 (mon (cte nat k))) h)); auto.

> apply lub_le_compat; simpl; auto.

> Save.

On Tue, Nov 22, 2016 at 1:46 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Using Coq 8.5, I get error in the file Ccpo.v (of Alea, version 8), line 1729

> apply (fmonotonic2 F); auto.

> Unable to unify "monotonic2 (fun2 F)" with

>  "(F (mlub cte nat k)) (lub h) <= lub (F k @ h)".

I will try to fix it myself, of course, but I will be thankful for any hints. :)

On Mon, Nov 21, 2016 at 6:31 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Big thank you!

Yes, it helps.

It seems that Alea must be ported to Coq 8.5, but that seems easy to do. In progress.

--

Ilmars

On Mon, Nov 21, 2016 at 2:01 PM, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

On 11/21/2016 10:59 AM, Ilmārs Cīrulis wrote:
> I am thinking about the best way to use Coq for extracting correct programs
> that uses random numbers? (Preferably, into Haskell.)
> Is there some good library for such purposes? Or, if there's not, what's the
> best literature / articles to get useful insights.

You could certainly program (in Coq) using a probability monad, which
should extract nicely to Haskell or to Caml.

To formally reason about your probabilistic programs, the following
Coq libraries and tools could help:
- Alea  https://www.lri.fr/~paulin/ALEA/
- Certicrypt  http://certicrypt.gforge.inria.fr/

Hope this helps,

- Xavier Leroy