Stream: Coq users

Topic: ✔ using ALEA module


view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 16:22):

I'm trying to use the ALEA module, more specifically create a random list like in
https://www.lri.fr/~paulin/ALEA/html/ALEA.RandomList.html.
I have successfully imported ALEA but I get the following error:
Error: the reference distr was not found in the current environment.
distr is a variant provided by Probas. I import Probas like:
Require Import Probas.
Also, when I do:
Print Probas.Proba.
I see that distr is a variant inside module UP.

I'm using nix but not the toolbox, I don't know if that would help with this issue.

Maybe the issue is with my coqProject?

view this post on Zulip Li-yao (Jun 05 2022 at 16:32):

Locate distr will tell you how to qualify it/what modules to import.

view this post on Zulip Li-yao (Jun 05 2022 at 16:34):

Probas.v only defines a module functor, which gets instantiated in Prog.v, so maybe try Require Import Prog.

view this post on Zulip Li-yao (Jun 05 2022 at 16:35):

Also this is where you can check out the sources, as they seem to have evolved quite a bit https://github.com/coq-community/alea

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 16:47):

@Li-yao thanks! I have imported all of the modules in ALEA, I do locate distr and I get:
No object of basename distr

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 16:48):

Yes, I get the sources from coq-community

view this post on Zulip Li-yao (Jun 05 2022 at 16:55):

Ah all of the library has been functorized, so to use it you need to instantiate it with a module implementing the Universe module signature.

view this post on Zulip Li-yao (Jun 05 2022 at 16:59):

The simple solution is for you to make a functor as well.

From ALEA Require Import Utheory Cover.

Module MyM (Univ : Universe).

Module Export Cover := CoverFun Univ.
Export RP.
Export PP.

Print distr.

(* work here *)

End MyM.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 17:05):

I get:
Error: "Universe" is not a module type.
Is universe also something I have to import? I tried to no avail

view this post on Zulip Li-yao (Jun 05 2022 at 17:15):

Universe lives in Utheory. I updated my snippet to a (hopefully) compilable example.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 17:28):

Thanks @Li-yao!! Now when I locate distr, I get the location. Also you located distr behind RP and PP, very nice of you.
Unfortunately the example of random list doesn't seem to work with alea anymore. I get:
The term "length l" has type "nat" while it is expected to have type "U.(tord)".
I got the same error with some lemmas that used nat.
Any idea why?

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 17:30):

I see that in Uprop.v:2800 change (tord nat0) in n.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 17:44):

If I put length l outside the brackets, I get:
Error: Syntax error: [term] expected after '/' (in [term])
In ALEA this notation is used a lot, but I don't know what I have to import to make this work.

view this post on Zulip Li-yao (Jun 05 2022 at 17:55):

The notation [1/] x is now [1/]1+ x and lives in the Univ module parameter. And the type error is because of an implicit argument setting that's hidden in the rendered version of RandomList.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 05 2022 at 18:00):

Thanks @Li-yao !! That worked. Sorry for needing so much hand holding, I'm a newbie

view this post on Zulip Li-yao (Jun 05 2022 at 18:01):

No worries, that stuff is not obvious :)

view this post on Zulip Bas Spitters (Jun 06 2022 at 14:16):

@Roland Coeurjoly Did you consider using other libraries for probabilities, like the math-comp one.
@Théo Zimmermann and others would it make sense to make an "alternatives to" on:
https://coq-community.org/awesome-coq/

view this post on Zulip Roland Coeurjoly Lechuga (Jun 06 2022 at 14:30):

@Bas Spitters I see that in the analysis library of math-comp there is support for probabilities, but I don't see much documentation and examples, and with ALEA there are

view this post on Zulip Bas Spitters (Jun 06 2022 at 14:43):

The library is much better maintained. E.g. we're happily using it for our SSProve system.
https://github.com/SSProve/ssprove

What's your overall goal with your formalization?

view this post on Zulip Roland Coeurjoly Lechuga (Jun 06 2022 at 14:47):

I have to prove that a debugging algorithm terminates and returns a buggy node (which represents a function execution). The user evaluates the correctness of a certain node, with possible answers correct or incorrect. I think it is appropriate to model the user as a probability distribution of this 2 possible answers.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 06 2022 at 15:39):

@Bas Spitters do you think that is something that could be achieved using math-comp?

view this post on Zulip Bas Spitters (Jun 06 2022 at 16:48):

I don't see why not. I sounds like a fairly straightforward use of probabilistic programming, which I would imagine can be encoded monadically (like in ALEA)

view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:09):

@Roland Coeurjoly have you looked at https://github.com/affeldt-aist/infotheo and its "flagship" probability theory application: https://github.com/certichain/ceramist

view this post on Zulip Karl Palmskog (Jun 06 2022 at 17:11):

other libraries discussed here: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166

view this post on Zulip Roland Coeurjoly Lechuga (Jun 06 2022 at 17:30):

@Karl Palmskog yes, I read the discussion, and I concluded that ALEA was a good option. But I admit that I am a bit overwhelmed with so many options with various degrees of maintenance. In the last comment in that discussion @Bas Spitters talks about integration. What would that integration work in practice?

view this post on Zulip Notification Bot (Jun 07 2022 at 19:21):

Roland Coeurjoly has marked this topic as resolved.


Last updated: Oct 01 2023 at 18:01 UTC