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

Review changes
Download
Patches
Plain diff

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

robbert/map_filter_True_False into master

Overview 6
Commits 2
Pipelines 4
Changes 2

All threads resolved!

Merged Robbert Krebbers requested to merge robbert/map_filter_True_False into master 3 years ago

Overview 6
Commits 2
Pipelines 4
Changes -

All threads resolved!

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).