Skip to content

Simplify proofs of `gmap` local update lemmas.

Robbert Krebbers requested to merge robbert/gmap_local_updates into master

Inspired by !948 (merged) this MR adds:

Lemma gmap_local_update m1 m2 m1' m2' :
  (∀ i, (m1 !! i, m2 !! i) ~l~> (m1' !! i, m2' !! i)) →
  (m1, m2) ~l~> (m1', m2').

This addresses a todo from 2017:

TODO: Investigate whether we can use these in proving the very similar local updates on finmaps.

Merge request reports