Add several simple lemmas (mostly about list and map filter).

Some simple lemmas about lists and maps. The lemma map_filter_lookup_eq' generalises map_filter_lookup_eq and can be used to shorten the proof of map_filter_iff.

Thanks for this MR. Overall I think these are useful lemmas, with the exception of insert_union_comm and insert_union_comm', for which I have my doubts (see comments).

Some questions:

• We are getting tons of "extensionality" lemmas for filter, and the names (of both the existing and new lemmas) are not great. Concretely, we have:

  • map_filter_lookup_eq' : (∀ k v, (P1 (k, v) ∧ m1 !! k = Some v) ↔ (P2 (k, v) ∧ m2 !! k = Some v)) → filter P1 m1 = filter P2 m2 (new)
  • map_filter_lookup_eq : (∀ k x, P (k,x) → m1 !! k = Some x ↔ m2 !! k = Some x) → filter P m1 = filter P m2 (existing)
  • map_filter_iff : (∀ x, P1 x ↔ P2 x) → filter P1 m = filter P2 m (existing)

  (And similarly for the versions for lists) It seems like the second one is barely used, do I would be in favor of deleting it and having the first instead. Maybe a better name would be map_filter_strong_ext? Do we have any lemmas that are similar?

• I have doubts about the names map_filter_filter_1 and map_filter_filter_2 since we usually use _1 and _2 for the two directions of a ↔ lemma. Maybe _l and _r would be better? Any opinions?

added 3 commits

• c7f299a5 - 1 commit from branch iris:master
• 04c0a58c - Add several simple lemmas (mostly about list and map filter).
• 06471403 - Apply proposed ammendments to the MR.

Compare with previous version

added 1 commit

• 1c9edd39 - Apply proposed amendments to the MR.

Compare with previous version

added 11 commits

• 1c9edd39...7309dfa2 - 7 commits from branch iris:master
• 929bb71b - Add several simple lemmas (mostly about list and map filter).
• fe1b7b86 - Apply proposed amendments to the MR.
• 7e69d4b8 - Add lemma about [list_to_set] composed with [elements].
• c6d1e8b2 - Remove lemma [list_filter_alt].

Compare with previous version

added 8 commits

• c6d1e8b2...d3feb6b5 - 3 commits from branch iris:master
• 0608ef65 - Add several simple lemmas (mostly about list and map filter).
• 0f49e561 - Apply proposed amendments to the MR.
• dbc36fe6 - Add lemma about [list_to_set] composed with [elements].
• a1fc7de9 - Remove lemma [list_filter_alt].
• 1749dd30 - Perform further amendments.

Compare with previous version

Can you also add a CHANGELOG?

added 1 commit

• b182e533 - CHANGELOG.

Compare with previous version

added 1 commit

• d8badd5e - CHANGELOG.md

Compare with previous version

added 1 commit

• b68a10e9 - CHANGELOG.

Compare with previous version

added 1 commit

• 388382c4 - Remove [map_filter_lookup_eq].

Compare with previous version

added 1 commit

• 10636f91 - Add context to section [map_filter_misc] and shorten some proofs.

Compare with previous version

added 1 commit

• 8220d9a9 - CHANGELOG.

Compare with previous version