Add some _1, _2 lemmas for map_filter

As discussed with @robbertkrebbers

assigned to @msammler

unassigned @msammler

I think the not_elem_of_dom and lookup_union_None lemmas are no-brainers and could be added asap.

The filter lemmas are a bit more of a headache since we need to make sure they are consistent with those for set/list.

Could you maybe split up the MR?

added 30 commits

• 861b0283...b99e79cf - 29 commits from branch master
• 8a4b52b7 - Add some _1, _2 lemmas

Compare with previous version

mentioned in merge request !405 (merged)

added 1 commit

• 18c543b3 - Add some _1, _2 lemmas

Compare with previous version

changed title from Add some _1, _2 lemmas to Add some _1, _2 lemmas for map_filter

Status: needs figuring out the names for the new lemmas and making sure they are consistent with sets and lists. @robbertkrebbers says he has some half-finished work somewhere he'll try to dig out.

added S-waiting-for-review label

removed S-waiting-for-review label

added S-waiting-for-author label

mentioned in merge request !582 (merged)

added 537 commits

• 18c543b3...d6ba38c3 - 536 commits from branch master
• a825d7aa - Add some _1, _2 lemmas

Compare with previous version

added 123 commits

• a825d7aa...e3a6f3ef - 122 commits from branch master
• df5ac4a9 - Add some _1, _2 lemmas

Compare with previous version

added 1 commit

• ce64df0e - Add _1, _2 lemmas for map_empty_filter

Compare with previous version

added 1 commit

• ba934995 - Add _1, _2 lemmas for map_empty_filter

Compare with previous version

resolved all threads

removed S-waiting-for-author label

added S-waiting-for-review label

I added a changelog for this MR. Is there anything else that needs to be done for this?

Okay should be good to go then. :) @robbertkrebbers can you take a final look?

added 3 commits

• ba934995...ada66bd2 - 2 commits from branch master
• 5a5578b4 - Add _1, _2 lemmas for map_empty_filter

Compare with previous version

mentioned in commit 96ef0cd6

merged

Thanks!

@iris-users This is a breaking change:

• Rename map_filter_empty_iff to map_empty_filter

mentioned in merge request !584 (merged)