get rid of axiom and uninstantiated operator in `Birthday`

[oskgo]

I'd also like to add exists_max to Distr.ec instead but the file does not pass the check on my computer, most likely because I don't have CVC4 installed (M1 Mac).

I've also made the theory abstract due to the uninstantiated T parameter. This is needed because the modules cannot take type parameters.

Thanks to @Cimylog for finding this.

[oskgo]

Pinging @chdoc for review.

[fdupress]

Thanks, both.

Is the final lemma stated in a way that could either 1) make use of the new pr_max (instead of picking an element of max weight); 2) locally quantify over an upper-bound on the guessing probability?

More generally, I think this is one of the oldest libraries we wrote, and we'd be very happy to see it change more drastically in ways that better support actual usage. We should merge this independently of that.

[fdupress]

@oskgo can you also give a quick outline of the proof and the arguments underlying it?

First thought was "This is fine." Second thought was "Hang on, this wouldn't work for min." Third thought was "It has to involve the fact that the sum is bounded.'

Is there something in there that could or should be pushed to the theory of series and summability?

[chdoc]

Third thought was "It has to involve the fact that the sum is bounded.'

It does. The way I exploit it is through the following lemma:

lemma mu_pos_fin (d : 'a distr) eps :
  0%r < eps => is_finite (fun x => eps <= mu1 d x).

[oskgo]

@chdoc I'll switch to using the appropriate lemmas. 🙃

I also managed to make my smt solvers work properly again by setting XDG_CONFIG_HOME and running easycrypt why3config.

[chdoc]

I think that if you want to refactor Distr that should be done as a separate PR.

[oskgo]

@chdoc Should be good now.

[oskgo]

I'm only moving things around so I can group the p_max lemmas with my mode operator and the associated lemmas. There are no internal changes to any of the lemmas or proofs in Distr.

Personally I don't think it makes much sense to postpone the reordering, but I can put my operator somewhere towards the end instead if you want this PR to preserve the order of the lemmas in Distr.

[chdoc]

I'm only moving things around so I can group the p_max lemmas with my mode operator and the associated lemmas. There are no internal changes to any of the lemmas or proofs in Distr.

Point in case: I actually missed the new operator when I looked at the diff.

Personally I don't think it makes much sense to postpone the reordering, but I can put my operator somewhere towards the end instead if you want this PR to preserve the order of the lemmas in Distr.

I think it would be good if the refactoring was its own commit. However, the policy is usually to squash merge. @fdupress is rebase merging also an option?

[fdupress]

Rebase merge is fine if it makes sense and the history is clean: my recent commit to the CI config was rebase merged because it did 3 different things that could not easily be split into 3 PRs because of the need to preserve ordering.

[fdupress]

That being said, after taking the whole conversation's context in, if everything is fine except for the fact that the commits could be split, then let's keep things as they are: messing about with history for the sake of history only is not yet so high a priority that we should spend our contributors' good will on it.

[oskgo]

I didn't see the conversation until i changed the history. I'll make a refactoring PR once this one is merged (if I remember).

I'm ready for review.

[fdupress]

@oskgo Please rebase and merge when ready. (And ideally ASAP, to prevent drift.)

[oskgo]

@fdupress I don't have write access, so I can't merge, but I'll do the rebase.