Generalize `map_filter_insert` so that it covers both the True and False case.
All threads resolved!
All threads resolved!
Compare changes
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.