[theories/modules] law of total probability

[alleystoughton]

Add module-based law of total probability for distributions with finite support.
Put it in theories/modules as it uses event partitioning.

[alleystoughton]

I don't understand why the EC library checking failed.

[alleystoughton]

I made the distribution a parameter to the procedure of the Rand module, instead of a theory parameter, and force pushed.

[alleystoughton]

I don't understand why the EC library checking failed.

I see, it's because I checked it with Alt-Ergo. Will fix this.

[alleystoughton]

I don't understand why the EC library checking failed.

It checked for me with Z3 (4.15.4) and CVC5 (1.3.2). Fixed to check with just Z3.

[fdupress]

Using make check before committing or pushing to the EC repo (but after moving your file to the EC working directory) should make use of the easycrypt.project we serve, which should ensure that the CI reproduces successes (barring regressions in SMT solvers, which are mostly rare now that we do not use Alt-Ergo).

I'll do a proper review + local edits when it's not a bank holiday, but wanted to guide your workflow to avoid you having to figure out why CI is failing in the future!

[oskgo]

This might be easier to use if supp was computed as to_seq (support dt'), requiring is_finite (support dt'), instead of taking it as an argument.

I suppose the existing variant is simpler if you already have a supp that might be distinct from to_seq (support dt'). Maybe it makes sense to have both variants? For the existing variant it might be better to move supp to the front of the argument list since this cannot be inferred from the LHS in rewrites. If the intention is to rewrite in the other direction where supp can be inferred it might make sense to swap the sides of the equality.

[alleystoughton]

Thanks for the suggestion. I'd missed that there was this operator.

[alleystoughton]

That worked out nicely, at least as easy to use.