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?
Locate distr
will tell you how to qualify it/what modules to import.
Probas.v
only defines a module functor, which gets instantiated in Prog.v
, so maybe try Require Import Prog
.
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
@Li-yao thanks! I have imported all of the modules in ALEA, I do locate distr and I get:
No object of basename distr
Yes, I get the sources from coq-community
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.
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.
I get:
Error: "Universe" is not a module type.
Is universe also something I have to import? I tried to no avail
Universe
lives in Utheory
. I updated my snippet to a (hopefully) compilable example.
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?
I see that in Uprop.v:2800 change (tord nat0) in n.
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.
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
.
Include Univ.
after the Module
line (Import
should also work but the ALEA sources all use Include
for some reason)[1/](length l)
to [1/]1+ (length l)
Set Implicit Arguments.
Thanks @Li-yao !! That worked. Sorry for needing so much hand holding, I'm a newbie
No worries, that stuff is not obvious :)
@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/
@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
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?
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.
@Bas Spitters do you think that is something that could be achieved using math-comp?
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)
@Roland Coeurjoly have you looked at https://github.com/affeldt-aist/infotheo and its "flagship" probability theory application: https://github.com/certichain/ceramist
other libraries discussed here: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166
@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?
Roland Coeurjoly has marked this topic as resolved.
Last updated: Oct 01 2023 at 18:01 UTC