Skip to content
Snippets Groups Projects

Add `set_fold_union_strong` and similarly for map

Merged Robbert Krebbers requested to merge robbert/set_fold_union into master

This discussion at Mattermost nerdsniped me to add the lemma set_fold_union and the stronger lemma set_fold_union_strong that only requires idempotence/associativity/commutativity for the elements in the sets.

Interestingly, the already existing "disjoint" versions of the lemma can be derived.

The proofs are pretty long/tricky, so I tried to add some comments what's going on.

Merge request reports

Merge request pipeline #106870 passed

Merge request pipeline passed for 8bfd5a08

Approval is optional

Merged by Robbert KrebbersRobbert Krebbers 7 months ago (Sep 10, 2024 6:08pm UTC)

Merge details

  • Changes merged into master with a1a12e00.
  • Deleted the source branch.
  • Auto-merge enabled

Pipeline #106871 passed

Pipeline passed for a1a12e00 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung
  • added 1 commit

    • 4f656cac - Apply 1 suggestion(s) to 1 file(s)

    Compare with previous version

  • I noticed there's an inconsistency in naming between the fold lemmas for maps and sets.

    1. For maps we use no suffix for the "strong" version, and _L for the = version. See e.g., map_fold_insert and map_fold_insert_L.
    2. For sets we use suffix _strong for the "strong" version, and no suffix for the = version. See e.g., set_fold_disj_union_strong and set_fold_disj_union.

    I would be in favor of using the convention for sets also for maps.

    Also it appears lemmas for fold + (disjoint)union are missing for maps.

  • What makes the strong versions 'strong'? _L is usually about Leibniz equality and strong is often about only showing facts for actual elements of the set/list/map, so those sound like very different situations?

  • Oh in this case we have a version that is general over the relation and gives "element of" facts, and a version specifically for eq. That doesn't sound like the _L situation though? _L is about vs =, not about general relation vs specific relation.

  • Indeed, so then we seem to agree on:

    I would be in favor of using the convention for sets also for maps.

    The names for the list lemmas are also not great. So how about I open a new MR where we can bikeshed about renamings?

  • Yeah the set version is definitely better than the map version.

    Don't we sometimes use _eq for the = version?

  • The only example I can find is foldr_cons_permute_eq, and that's an instance of "The names for the list lemmas are also not great" :smile:

    • Resolved by Robbert Krebbers

      how about I open a new MR where we can bikeshed about renamings?

      Or an issue? I am not sure we have consensus yet so don't spend time adjusting all the names quite yet.^^

      I think for distinguishing general relation vs = I would prefer names ending in _gen(eral) vs _eq, or something like that.

      We do have gen_proper lemmas in Iris for a similar situation.

      Edited by Ralf Jung
  • Robbert Krebbers added 533 commits

    added 533 commits

    Compare with previous version

  • added 2 commits

    • 01dca152 - Add lemma `foldr_idemp`.
    • f75160fe - Add lemmas `set_fold_union_strong` and `set_fold_union`.

    Compare with previous version

  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers mentioned in issue #215

    mentioned in issue #215

  • added 1 commit

    Compare with previous version

  • I fixed all remaining problems and added a CHANGELOG.

    I think this is ready to go.

  • Robbert Krebbers mentioned in merge request !573 (merged)

    mentioned in merge request !573 (merged)

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading