Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`

• Rename lemmas elem_of_list_X into list_elem_of_X to be consistent with the list_lookup_X lemmas. Some lemmas contained other inconsistencies (e.g., _1 and _2 swapped), see CHANGELOG for details.
• Change the order of the conjunction in list_lookup_fmap_Some. The new version is (f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x, which makes it consistent with list_elem_of_fmap and the corresponding lemmas for sets and maps. To be continued in other MR, insert link
• Rename list_alter_fmap → list_fmap_alter and remove list_alter_fmap_mono which was a monomorphic duplicate.

With the exception of the list_elem_of_fmap change, all changes in this MR can be applied by sed. It would be best to merge it together with !526 (merged) so we only have to run a giant sed script once on reverse dependencies.

This MR revealed another inconsistency, we use elem_of_list_X and list_lookup_X.

I prefer the latter scheme. Since we are performing massive renamings (as in this MR and !526 (merged)), and this can be fixed by sed, this might be the time to fix that.

added 1 commit

• b152571c - Also fix `elem_of_list` → `list_elem_of` inconsistency.

Compare with previous version

added 1 commit

• 83bf38cb - Also fix `elem_of_list` → `list_elem_of` inconsistency.

Compare with previous version

changed the description

I have adjusted the MR to take the prior comment into account. It turns out to be not just replacing elem_of_list_X with list_lookup_X. You have to exclude somethings such as elem_of_list_to_set and elem_of_list_to_set_disj.

changed title from Make lookup and elem_of lemmas for list consistent with those for map and set. to Fix inconsistencies in lookup and elem_of lemmas for list

added 1 commit

• bcc8e36e - Rename `list_alter_fmap` → `list_fmap_alter`, remove `list_alter_fmap_mono`.

Compare with previous version

changed the description

added 1 commit

• e8928020 - Fix bug in CHANGELOG.

Compare with previous version

changed the description

There was a bug in the MR description and CHANGELOG, I said that list_elem_of_fmap changed, but it is list_lookup_fmap_Some that changed.

added 1 commit

• fea65407 - Fix typo in CHANGELOG.

Compare with previous version

mentioned in merge request !532

mentioned in merge request iris!1008

added 12 commits

• fea65407...b7eaaf91 - 2 earlier commits
• f85c45f4 - Follow same scheme for `multiplicity_singleton`.
• 211ee09d - Follow same scheme for list lemmas.
• 0a52e84c - CHANGELOG.
• fead4470 - Merge branch 'robbert/eq_lemmas' into 'ci/refactor_staging'
• d9a6e55e - Make `lookup` and `elem_of` lemmas for `list` consistent with those for map and set.
• 44d3349c - CHANGELOG.
• 1235cdaa - Also fix `elem_of_list` → `list_elem_of` inconsistency.
• 4aa3ffdf - Rename `list_alter_fmap` → `list_fmap_alter`, remove `list_alter_fmap_mono`.
• d875d10f - Fix bug in CHANGELOG.
• f6820a98 - Rename `list_elem_of_fmap_2_alt` → `list_elem_of_fmap_2'`.

Compare with previous version

changed the description