Skip to content

Various tweaks to lists, maps, sets

Robbert Krebbers requested to merge robbert/list_map_set_tweaks into master

While reviewing !442 (merged) and !441 (merged) I ran into a bunch of stuff that should be improved:

  • Add subset_proper.
  • Add list_eq_prefix_length and list_eq_suffix_length. The version for prefix is also part of !441 (merged), but the version for suffix was missing there.
  • Add set_equiv_subseteq_size and set_eq_subseteq_size. Similar to the prior lemmas, but now for set equality. These are not part of !441 (merged) and !442 (merged).
  • Add dom_subseteq_size, dom_subset_size, map_eq_subseteq_dom. The last lemma is part of !442 (merged), but the version in this MR is stronger since it requires Set_ instead of FinSet)
  • Add map_eq_subseteq_size, map_subseteq_size, map_subset_size. These lemmas are also part of !442 (merged), but the statement and naming are made consistent with similar lemmas for sets, and the proof have been shortened.
  • Add Permutation_submseteq_length to replace Permutation_alt, submseteq_Permutation_length_le and submseteq_Permutation_length_eq. This makes the statement and naming consistent with the new lemmas for prefix/suffix/sets/maps
  • Simplify proofs of map induction principles; remove map_to_list_length.
Edited by Robbert Krebbers

Merge request reports