coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] What's the best way to extract programs that use random numbers?
Chronological Thread
- From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] What's the best way to extract programs that use random numbers?
- Date: Tue, 22 Nov 2016 20:31:38 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f179.google.com
- Ironport-phdr: 9a23:rlmpORCkiuxN8y++HVftUyQJP3N1i/DPJgcQr6AfoPdwSPT7osbcNUDSrc9gkEXOFd2CrakV0KyM7uu5ATFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZb1/IA+ooQjRucUanJduJ6YswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UohyhqRxxzYDXfY+bKuZxc7jHct8GX2dMRNpdWzBDD466coABD/ABPeFdr4TlpFUOqR6+AA+2BOP01zRFmH723bcn0+QlEAHGxxErEtUPsHTQqdX6Lr0SUfuvwKbUzDXDde5W2TP86IjTaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik28nqwdrojiu3MggkIfJhpgNxlDA7yV5wZw5JdOiSEN9fNWqE4NQujmEO4dqRs4uWWJltSYgxrEbuJO3YTIGxIklyhPbbfGMbpKG7Qj5VOmLJDd1nHJld6y7hxa16UWgz/fzVsiw0FpTritEnMXAumkD1xDO6MWKTuFx/kim2TaI2ADT7v9LLVoomqrcLp4t2r8wlpwNvkTfBiL6hln6gauMekgn+uWk8fnrb7T7qpOGKoN5iAXzPrwrmsOlAOQ4NgYOX3Kc+eS5zLDj/En5QLBQgf0sianVqozVJcUBpq6kBw9V050j5g2wDzejytsYnH0HIEhZdxKAiojlI0vOL+zgDfejn1Ssly9myOzBPr34G5nCMnzDkKr6crtm8E5dyA8zzchF6J5OC7EBJujzWk7ru9DCAB85KV/8/+GyQt56z8YVXX+FKq6fKqLb91GSrKp7KO6VIYQRpTzVKv4/5veog2VvynEHeqz8/J8Sw2qjVt9nOVidYGGk1tYFFG4QpUw1Tfb3jFyZeTFWbne2Gak742doW8qdEY7fS9X10/S61yChE8gOaw==
Successfully fixed (ported?) it for Coq 8.5 pl 3.
(except Rplus.v file.)
On Tue, Nov 22, 2016 at 3:43 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
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.--IlmarsOn 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
- [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Xavier Leroy, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/22/2016
- Re: [Coq-Club] What's the best way to extract programs that use random numbers?, Ilmārs Cīrulis, 11/21/2016
Archive powered by MHonArc 2.6.18.