Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.

This has been discussed in !507 (closed). This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.

While performing the refactoring, I also added some missing lemmas. They are also described in the CHANGELOG.

I tested the sed script on iris, iris-examples, lambdarust, Actris, Iron, GPFSL. No manual fixes were needed.

mentioned in merge request !507 (closed)

added 1 commit

• 0a181ec0 - CHANGELOG.

Compare with previous version

added 9 commits

• 0a181ec0...c4ea1778 - 4 commits from branch master
• 2437efa0 - `_eq` lemmas for maps.
• 50ad574c - Follow same scheme for other map lemmas.
• b0b80560 - Follow same scheme for `multiplicity_singleton`.
• 6f0564e5 - Follow same scheme for list lemmas.
• 8900568d - CHANGELOG.

Compare with previous version

mentioned in merge request !530 (merged)

mentioned in merge request !531 (merged)

added 16 commits

• 8900568d...32edabf7 - 11 commits from branch master
• ec2d6bdd - `_eq` lemmas for maps.
• 9462e1d2 - Follow same scheme for other map lemmas.
• 43c7fc90 - Follow same scheme for `multiplicity_singleton`.
• 6ab49eb3 - Follow same scheme for list lemmas.
• 6c418c2d - CHANGELOG.

Compare with previous version

Wow that's a huge PR. Thanks a lot for taking care of this! I reviewed mostly the changelog, since the actual diff is a bit too much...

added 1 commit

• cc29fff2 - Improvements to CHANGELOG.

Compare with previous version

added 6 commits

• b7eaaf91 - Follow same scheme for other map lemmas.
• f85c45f4 - Follow same scheme for `multiplicity_singleton`.
• 211ee09d - Follow same scheme for list lemmas.
• f0787262 - CHANGELOG.
• 23b17486 - Improvements to CHANGELOG.
• 59b232a3 - Improvements to CHANGELOG.

Compare with previous version

mentioned in merge request !532

changed target branch from master to ci/refactor_staging

I changed this MR to be merged in the the "refactor" staging branch (see !532). Aside from the CHANGELOG discussion, I think this one is good to go.

resolved all threads

added 2 commits

• 509990a7 - Improvements to CHANGELOG.
• 9672c3da - Improvements to CHANGELOG.

Compare with previous version