Roland Coeurjoly Lechuga (Jun 05 2022 at 16:22): 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?
Li-yao (Jun 05 2022 at 16:32):Locate distr will tell you how to qualify it/what modules to import.
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.
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
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
Roland Coeurjoly Lechuga (Jun 05 2022 at 16:48):Yes, I get the sources from coq-community
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.
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.
I get:
Error: "Universe" is not a module type.
Is universe also something I have to import? I tried to no avail
Li-yao (Jun 05 2022 at 17:15):Universe lives in Utheory. I updated my snippet to a (hopefully) compilable example.
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?
Roland Coeurjoly Lechuga (Jun 05 2022 at 17:30):I see that in Uprop.v:2800 change (tord nat0) in n.
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.
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.
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. 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
Li-yao (Jun 05 2022 at 18:01):No worries, that stuff is not obvious :)
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/
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
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?
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.
Roland Coeurjoly Lechuga (Jun 06 2022 at 15:39):@Bas Spitters do you think that is something that could be achieved using math-comp?
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)
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
Karl Palmskog (Jun 06 2022 at 17:11):other libraries discussed here: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166
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?
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