Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 16
    • Merge requests 16
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !310

Generalize `map_filter_insert` so that it covers both the True and False case.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/map_filter_True_False into master Jul 27, 2021
  • Overview 6
  • Commits 2
  • Pipelines 4
  • Changes 2

The new lemma is

Lemma map_filter_insert m i x :
  filter P (<[i:=x]> m)
  = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).

We need the delete because there might be another entry with key i in m.

In addition there are the lemmas:

Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
  P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
  ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).

I use the _True and _False suffixes similar to decide_True and decide_False.

See discussion in !245 (335bc4d6, comment 72118) for the discussion that led to this MR.

Edited Jul 28, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/map_filter_True_False