Generalize `map_filter_insert` so that it covers both the True and False case.

The new lemma is

Lemma map_filter_insert m i x :
  filter P (<[i:=x]> m)
  = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).

We need the delete because there might be another entry with key i in m.

In addition there are the lemmas:

Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
  P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
  ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).

I use the _True and _False suffixes similar to decide_True and decide_False.

See discussion in !245 (335bc4d6, comment 72118) for the discussion that led to this MR.

added 1 commit

• 2bedde94 - CHANGELOG.

Compare with previous version

mentioned in merge request !245 (merged)

changed the description

added 2 commits

• 3182c252 - Weaken premise of `map_filter_delete_False` and make it consistent with `map_filter_insert_False'`.
• 0557c750 - CHANGELOG.

Compare with previous version

added 2 commits

• 8e5ae5c2 - Generalize `map_filter_insert` so that it covers both the True and False case.
• b40765e8 - CHANGELOG.

Compare with previous version

changed the description

LGTM!

resolved all threads

mentioned in commit 8168d813

merged

@iris-users:

• Add generalized lemma map_filter_insert that covers both the True and False case. Rename old map_filter_insert → map_filter_insert_True and map_filter_insert_not_delete → map_filter_insert_False.
• Weaken premise of map_filter_delete_not to make it consistent with map_filter_insert_not'.