fsbigop.v review

[zstone1]

I've done a review of the fsbigop.v file. Looks pretty reasonable. There are a couple mechanical things, and then a couple more general questions: @affeldt-aist, not sure who else should be tagged on this.

small changes

1. fsbig_supp takes an unused argument D
2. We're missing fsbig_split. We have fsum_split, but a more general version would be nice.
3. In the definition of mkcond, is there any value in using the patch function instead of using the conditional directly?
4. I'm pretty sure full_fsbigID could have a simpler proof using fsbig_split. I took 20 minutes to attempt it, and got stuck trying to convert between various kinds of BigOps. Then I gave up.
5. Are all these deprecated flags just trying to make up for not having private methods, or is there actually a plan to delete these lemmas?

some generalizations

When P is infinite, but F is finitely supported in P,

\big[op/idx]_(i \in P) F i

is doing something interesting, and this is adding clear value. But there are a few lemmas like fsum_split and exchange_fsum that take finite_set P as an assumption. I'd recommend adding a definition like Definition support P f := P '&' f @^-1' [set~ idx]. That will help factor things a bit. And a hint for finite_set P -> finite_set (support P f) would generalize those lemmas accordingly.

How is this related to the other bigops?

Is part of the goal here to unite all the measure theory stuff under a single definition of BigOp? Having to navigate Fset, seq, set, finitely_supported, ect bigop definitions all at once sounds pretty difficult. So I'm kinda hopeful that this could be used in many instances (Except perhaps large union/intersections?).

[CohenCyril]

small changes

1. fsbig_supp takes an unused argument D

:+1:

2. We're missing fsbig_split. We have fsum_split, but a more general version would be nice.

:+1:

3. In the definition of mkcond, is there any value in using the patch function instead of using the conditional directly?

Apparently there is... since @affeldt-aist shortened the code.

4. I'm pretty sure full_fsbigID could have a simpler proof using fsbig_split. I took 20 minutes to attempt it, and got stuck trying to convert between various kinds of BigOps. Then I gave up.

maybe!

5. Are all these deprecated flags just trying to make up for not having private methods, or is there actually a plan to delete these lemmas?

Actually, I they are supposed to be subsumed by a combination of fsbig_widen and their non-deprecated alternative. So I hope they are indeed useless but I'm not 100% sure.

some generalizations

When P is infinite, but F is finitely supported in P,

\big[op/idx]_(i \in P) F i

is doing something interesting, and this is adding clear value. But there are a few lemmas like fsum_split and exchange_fsum that take finite_set P as an assumption. I'd recommend adding a definition like Definition support P f := P '&' f @^-1' [set~ idx]. That will help factor things a bit. And a hint for finite_set P -> finite_set (support P f) would generalize those lemmas accordingly.

As I tried to explain in 5., I put the finite_set P restriction on purpose, since replacing P by support P f can be done using fsbig_widen (right to left). But maybe you are right and your definition + hint would actually work even better!

How is this related to the other bigops?

Is part of the goal here to unite all the measure theory stuff under a single definition of BigOp? Having to navigate Fset, seq, set, finitely_supported, ect bigop definitions all at once sounds pretty difficult. So I'm kinda hopeful that this could be used in many instances (Except perhaps large union/intersections?).

I think this diversity is both an asset and a struggle. I think the way out is more documentation on what is rewritable to what.

[CohenCyril]

and thanks for the review

[affeldt-aist]

Comments partially addressed in PR #572 .