Skip to content

Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`

Robbert Krebbers requested to merge robbert/list_fmap_lemmas into ci/refactor_staging
  • Rename lemmas elem_of_list_X into list_elem_of_X to be consistent with the list_lookup_X lemmas. Some lemmas contained other inconsistencies (e.g., _1 and _2 swapped), see CHANGELOG for details.
  • Change the order of the conjunction in list_lookup_fmap_Some. The new version is (f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x, which makes it consistent with list_elem_of_fmap and the corresponding lemmas for sets and maps. To be continued in other MR, insert link
  • Rename list_alter_fmap → list_fmap_alter and remove list_alter_fmap_mono which was a monomorphic duplicate.

With the exception of the list_elem_of_fmap change, all changes in this MR can be applied by sed. It would be best to merge it together with !526 (merged) so we only have to run a giant sed script once on reverse dependencies.

Edited by Robbert Krebbers

Merge request reports