Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement. (!526) · Merge requests · Iris / stdpp

Robbert Krebbers requested to merge robbert/eq_lemmas into ci/refactor_staging Oct 14, 2023

This has been discussed in !507 (closed). This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.

While performing the refactoring, I also added some missing lemmas. They are also described in the CHANGELOG.

I tested the sed script on iris, iris-examples, lambdarust, Actris, Iron, GPFSL. No manual fixes were needed.

Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.

Merge request reports