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`

.

- Add
`Include Univ.`

after the`Module`

line (`Import`

should also work but the ALEA sources all use`Include`

for some reason) - Change
`[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