[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!

[strub]

I asked Claude to play the game and to fix the comments.

[fdupress]

In passing, and while doing my own pass (because I can't pay for Claude), I also noticed that the first non-module parameter to total_prob should be its after its second. In left-to-right rewriting, the distribution and additional input can be inferred, but the range cannot. I'll stack on a commit correcting that.

[oskgo]

Looks good to me.

Thank you for the contribution!

@fdupress Merging is blocked on your change requests (which all seem to have been addressed).

addressed