Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`
Compare changes
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.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
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.