Draft: Prepare MathComp pull request

This is in preparation of a pull request to MathComp to push generic lemmas upstream (I only went through util/nat.v anf util/sum.v for now). Merge plan:

• do a pull request on MathComp with the lemmas tagged TODO: PR MathComp
• when this PR is merged, adapt the current merge request and change the TODO comments into something like "will be in MathComp 1.15"
• merge the current merge request
• once MathComp 1.15 (or 2.0) is released and becomes the minimal version in Prosa, remove the tagged lemmas

Is there a volunteer to open the upstream pull request? I could certainly do it but I don't feel the most legitimate, not being an actual Prosa author. Note that I probably already made most of the work here by rewriting the proofs in a more MathComp style, so the procces should be reasonnably light. It's also a great opportunity to learn more about MathComp and how to write short and robust proof scripts with ssreflect.

This is great, thank you for starting the upstreaming effort!

I'll definitely want to get involved, but this week is already crazy busy, so I will probably not have much time (if any) to look into it.

added 9 commits

• 7641911e - Simplify proof of leq_sum_sub_uniq
• e6a17e68 - Simplify proof of {l,}eq_sum_seq
• aed5029d - Simplify proof of leq_sum_seq_pred
• b4fdd06f - Simplify proof of sumnB_nat
• a47fe1ab - Remove sum_seq_cond_gt0P
• 032aaedd - Simplify proof of sum_majorant_eqn
• 4d105fba - Remove sum0
• ab13c461 - Simplify proof of sum_of_ones
• 8d972f8a - Add MathComp to wordlist

Compare with previous version

No hurry

added 75 commits

• 8d972f8a...903e5476 - 52 commits from branch master
• aaf26118 - Remove subn_abba
• 6e4b5858 - Remove leq_addk
• 7b5bba61 - Prepare subdnD for MathComp PR
• c7b575f8 - Prepare leq_subRL_impl for MathComp PR
• a4974927 - Remove exists_or_not_add_mul_cases
• fb2b1e65 - Remove add_mul_diff
• 2d797ef5 - Rewrite 2 proofs in more ssreflect style
• 05a1776f - Generalize and simplify proof of sum_nat_eq0_nat
• d82e0f7c - Simplify sum_nat_gt0
• ee2c273f - Simplify proof of sum_notin_rem_eqn
• 2dc1570d - Simplify proof of sum_majorant_constant
• 35bd290d - Simplify proof of sum_pred_diff
• e8c95eb7 - Simplify proof of leq_sum_sub_uniq
• 538efe84 - Simplify proof of {l,}eq_sum_seq
• 9ce6f031 - Simplify proof of leq_sum_seq_pred
• f3cdfa98 - Simplify proof of sumnB_nat
• 5eb590c1 - Remove sum_seq_cond_gt0P
• c34d979d - Simplify proof of sum_majorant_eqn
• f2eedb8a - Remove sum0
• 18725a02 - Simplify proof of sum_of_ones
• 515ce07b - Add MathComp to wordlist
• b04df195 - protect TODO comments from spell checker
• 82bcf9b7 - fixup! Simplify sum_nat_gt0

Compare with previous version

No progress yet, but at least rebased. Recent changes in master caused a lot of merge conflicts.

I'm thinking of splitting this in two: (1) the cleanups and simplifications (without the MathComp TODOs), which could be merged rather soon to avoid further merge conflicts, and (2) the MathComp TODOs, which will probably take a bit longer to be resolved piece by piece.

Makes sense but it would probably be less work to just merge as it is (with the TODOs) and open an issue mentioning the TODOs to remember doing the upstreaming.

added 24 commits

• f925eeee - 1 commit from branch master
• 7a480edc - Remove subn_abba
• 8af3d009 - Remove leq_addk
• fff04c64 - Prepare subdnD for MathComp PR
• 5cb56cc4 - Prepare leq_subRL_impl for MathComp PR
• b9395c3a - Remove exists_or_not_add_mul_cases
• 2dabf450 - Remove add_mul_diff
• cad22b99 - Rewrite 2 proofs in more ssreflect style
• a55307be - Generalize and simplify proof of sum_nat_eq0_nat
• ef4bd179 - Simplify sum_nat_gt0
• 74f273c8 - Simplify proof of sum_notin_rem_eqn
• 0dd8bad8 - Simplify proof of sum_majorant_constant
• 56b9d030 - Simplify proof of sum_pred_diff
• cb30fb84 - Simplify proof of leq_sum_sub_uniq
• 4a2b9b9c - Simplify proof of {l,}eq_sum_seq
• 53afe9c9 - Simplify proof of leq_sum_seq_pred
• 3b9e2722 - Simplify proof of sumnB_nat
• 810ce289 - Remove sum_seq_cond_gt0P
• e46ff62f - Simplify proof of sum_majorant_eqn
• 8ea28803 - Remove sum0
• 3b988754 - Simplify proof of sum_of_ones
• a7d7f715 - Add MathComp to wordlist
• 93c1fb11 - protect TODO comments from spell checker
• 0790aede - fixup! Simplify sum_nat_gt0

Compare with previous version

added 29 commits

• bd554522 - Prepare subdnD for MathComp PR
• 697b6f71 - Prepare leq_subRL_impl for MathComp PR
• 59eb9c42 - Remove exists_or_not_add_mul_cases
• f61b1a30 - Remove add_mul_diff
• 57ac071c - Rewrite 2 proofs in more ssreflect style
• 69f472d4 - Generalize and simplify proof of sum_nat_eq0_nat
• 73d872d4 - Simplify sum_nat_gt0
• fd9362c4 - Simplify proof of sum_notin_rem_eqn
• e236b083 - Simplify proof of sum_majorant_constant
• 9789d90a - Simplify proof of sum_pred_diff
• 6d9ee6a7 - Simplify proof of leq_sum_sub_uniq
• 62777423 - Simplify proof of {l,}eq_sum_seq
• 29069c21 - Simplify proof of leq_sum_seq_pred
• 9351f653 - Simplify proof of sumnB_nat
• 7271808c - Remove sum_seq_cond_gt0P
• 15625c34 - Simplify proof of sum_majorant_eqn
• 4d40b3fb - Remove sum0
• 7946968b - Simplify proof of sum_of_ones
• 8bbb6f11 - MathComp PR TODO for sum_nat_gt0
• 2630da77 - MathComp PR TODO for subdnD
• 3e962af5 - MathComp PR TODO for leq_subRL_impl
• 491cd96f - MathComp PR TODO for sum_nat_eq0_nat
• 6dfe06ca - MathComp PR TODO for leq_sum_sub_uniq
• 1efd97fe - MathComp PR TODO for {l,}eq_sum_seq
• 08036d9f - MathComp PR TODO for leq_sum_seq_pred
• 78e5cb99 - MathComp PR TODO for sumnB_nat
• 4f1ee93e - MathComp PR TODO for sum_majorant_eqn
• ff2ac49c - Add MathComp to wordlist
• 16861a25 - protect TODO comments from spell checker

Compare with previous version

added 38 commits

• 16861a25...e3567e95 - 5 commits from branch master
• eda66272 - Remove subn_abba
• b782b2d7 - Remove leq_addk
• e1ad15ce - Prepare subdnD for MathComp PR
• 87094d03 - Prepare leq_subRL_impl for MathComp PR
• 72371646 - Remove exists_or_not_add_mul_cases
• feb7687b - Remove add_mul_diff
• 0164ff70 - Rewrite 2 proofs in more ssreflect style
• c2605125 - Generalize and simplify proof of sum_nat_eq0_nat
• 85ebd23d - Simplify sum_nat_gt0
• 60766ce5 - Simplify proof of sum_notin_rem_eqn
• c5210959 - Simplify proof of sum_majorant_constant
• c6819041 - Simplify proof of sum_pred_diff
• a695ccc9 - Simplify proof of leq_sum_sub_uniq
• 45e93b6f - Simplify proof of {l,}eq_sum_seq
• 955c7026 - Simplify proof of leq_sum_seq_pred
• d77587e2 - Simplify proof of sumnB_nat
• 2641b7b4 - Remove sum_seq_cond_gt0P
• 4ce91a2b - Simplify proof of sum_majorant_eqn
• aed41d5c - Remove sum0
• 8d0b8ab3 - Simplify proof of sum_of_ones
• cdfd02d5 - MathComp PR TODO for sum_nat_gt0
• c9ccf986 - MathComp PR TODO for subdnD
• 0c582dcc - MathComp PR TODO for leq_subRL_impl
• 21318ce5 - MathComp PR TODO for sum_nat_eq0_nat
• 057ba2ab - MathComp PR TODO for leq_sum_sub_uniq
• e23ee870 - MathComp PR TODO for {l,}eq_sum_seq
• 617c6a43 - MathComp PR TODO for leq_sum_seq_pred
• af1e9ae6 - MathComp PR TODO for sumnB_nat
• 2fe23236 - MathComp PR TODO for sum_majorant_eqn
• 939ad007 - Add MathComp to wordlist
• a3d020b2 - protect TODO comments from spell checker
• 3ae37941 - fixup! Simplify proof of sumnB_nat
• 00ad6c52 - fixup! Generalize and simplify proof of sum_nat_eq0_nat

Compare with previous version

added 24 commits

• 6ee9ee93 - Generalize and simplify proof of sum_nat_eq0_nat
• 55ff5fb4 - Simplify sum_nat_gt0
• 6a0ec068 - Simplify proof of sum_notin_rem_eqn
• d8bbb500 - Simplify proof of sum_majorant_constant
• b35a6b06 - Simplify proof of sum_pred_diff
• 121ae84c - Simplify proof of leq_sum_sub_uniq
• 66e63c02 - Simplify proof of {l,}eq_sum_seq
• fb84f2c4 - Simplify proof of leq_sum_seq_pred
• 68f80fbb - Simplify proof of sumnB_nat
• 1b4a03df - Remove sum_seq_cond_gt0P
• 8e2d2828 - Simplify proof of sum_majorant_eqn
• 80717b54 - Remove sum0
• 2f13c730 - Simplify proof of sum_of_ones
• e5b9c057 - MathComp PR TODO for sum_nat_gt0
• 3daa51b9 - MathComp PR TODO for subdnD
• e637b96a - MathComp PR TODO for leq_subRL_impl
• 645dace8 - MathComp PR TODO for sum_nat_eq0_nat
• 52affb8f - MathComp PR TODO for leq_sum_sub_uniq
• 0dacc14a - MathComp PR TODO for {l,}eq_sum_seq
• c2bbcab3 - MathComp PR TODO for leq_sum_seq_pred
• 1a0ef2df - MathComp PR TODO for sumnB_nat
• cb7cbe00 - MathComp PR TODO for sum_majorant_eqn
• ec303bf5 - Add MathComp to wordlist
• 85d21e4b - protect TODO comments from spell checker

Compare with previous version

mentioned in merge request !212 (merged)

You are right, that would be easier and less work, but I'd like to keep the spec "clean", including the util module (I know, I know...). So I'll tweak the cleanups a bit in !212 (merged) and then when rebasing on top of master this MR will consist primarily of the TODOs. (Which we still might want to turn into an issue at some point.)

Well, you are the one doing the painful work, so I certainly won't complain.

Note however that this is not following the "merge plan" offered in this merge request description.

Rebasing this MR has been difficult, because it tends to result in broken proofs elsewhere as the codebase evolves. For example, some of the lemmas removed in this MR were used in new code just recently merged. So I thought it would reduce work in the longterm to get this in sooner, so that new code is aware of these changes.

added 31 commits

• bb76b8bd - Prepare subdnD for MathComp PR
• 010ef216 - Prepare leq_subRL_impl for MathComp PR
• 0e8d85e0 - Remove exists_or_not_add_mul_cases
• 8ff12f1c - Remove add_mul_diff
• 162e01f4 - Rewrite 2 proofs in more ssreflect style
• 4a9a0cfc - Generalize and simplify proof of sum_nat_eq0_nat
• 594d4da6 - Simplify sum_nat_gt0
• 2d72fd86 - Simplify proof of sum_notin_rem_eqn
• e1d58324 - Simplify proof of sum_majorant_constant
• 9a537fa3 - Simplify proof of sum_pred_diff
• fb9eb1f3 - Simplify proof of leq_sum_sub_uniq
• 1c1a8bf9 - Simplify proof of {l,}eq_sum_seq
• d15b1e83 - Simplify proof of leq_sum_seq_pred
• a9431bf0 - Simplify proof of sumnB_nat
• fd7baf22 - Remove sum_seq_cond_gt0P
• e6205fed - Simplify proof of sum_majorant_eqn
• 9e195050 - Remove sum0
• fb3e19b5 - Simplify proof of sum_of_ones
• 45391d62 - reorganize `util.sum` and add some comments
• f5330204 - Revert "reorganize `util.sum` and add some comments"
• 0e6dfbea - MathComp PR TODO for sum_nat_gt0
• 7a99883c - MathComp PR TODO for subdnD
• 6736af64 - MathComp PR TODO for leq_subRL_impl
• a0f29a8c - MathComp PR TODO for sum_nat_eq0_nat
• d4ffcb2e - MathComp PR TODO for leq_sum_sub_uniq
• 2c984c85 - MathComp PR TODO for {l,}eq_sum_seq
• 17bf3ec3 - MathComp PR TODO for leq_sum_seq_pred
• 19a728c2 - MathComp PR TODO for sumnB_nat
• b0e014c0 - MathComp PR TODO for sum_majorant_eqn
• 8fd87880 - Add MathComp to wordlist
• 6ddac08b - protect TODO comments from spell checker

Compare with previous version

The changes to the lemmas have been merged as !212 (merged). This MR remains open to track the open TODOs and to (eventually) accumulate further changes as the TODOs are tackled one by one.

Thanks.

as the TODOs are tackled one by one

I don't think there is any need to do them one by one, a single pull request on mathcomp with all lemmas would probably do the job (there are less than 10 of them and they are quite related).

added 31 commits

• 6ddac08b...3607c290 - 19 commits from branch master
• 8c448fd5 - Revert "reorganize `util.sum` and add some comments"
• d3fc3cdf - MathComp PR TODO for sum_nat_gt0
• 8a313de6 - MathComp PR TODO for subdnD
• 7c056588 - MathComp PR TODO for leq_subRL_impl
• ba835f65 - MathComp PR TODO for sum_nat_eq0_nat
• edca8425 - MathComp PR TODO for leq_sum_sub_uniq
• f278ef2c - MathComp PR TODO for {l,}eq_sum_seq
• f22aed5a - MathComp PR TODO for leq_sum_seq_pred
• 7e60956e - MathComp PR TODO for sumnB_nat
• ff226079 - MathComp PR TODO for sum_majorant_eqn
• 84d23d0d - Add MathComp to wordlist
• ef78aad2 - protect TODO comments from spell checker

Compare with previous version

added 23 commits

• ef78aad2...998f7526 - 11 commits from branch master
• 34c438f1 - Revert "reorganize `util.sum` and add some comments"
• c64f2315 - MathComp PR TODO for sum_nat_gt0
• a67debe6 - MathComp PR TODO for subdnD
• 182f0e2c - MathComp PR TODO for leq_subRL_impl
• d72d71f7 - MathComp PR TODO for sum_nat_eq0_nat
• 54d7fcd9 - MathComp PR TODO for leq_sum_sub_uniq
• 60f49991 - MathComp PR TODO for {l,}eq_sum_seq
• 3404d2f5 - MathComp PR TODO for leq_sum_seq_pred
• 735cf74f - MathComp PR TODO for sumnB_nat
• d0c389c6 - MathComp PR TODO for sum_majorant_eqn
• 165a18f2 - Add MathComp to wordlist
• 4d5282fa - protect TODO comments from spell checker

Compare with previous version