Skip to content

GitLab

  • Menu
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 70
    • Issues 70
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 6
    • Merge requests 6
  • 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
  • !281

Various setoids lemmas for maps, lists, and option

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/setoid into master Jun 15, 2021
  • Overview 10
  • Commits 7
  • Pipelines 7
  • Changes 4

This MR adds various setoid lemmas.

Primarily: it's often useful to turn a setoid equality into a Leibniz equality. For boring elements like None, nil, and empty we have ma ≡ None ↔ ma = None, l ≡ [] ↔ l = [], and m ≡ ∅ ↔ m = ∅. For other functions, this is a bit more complicated, but there are useful results nonetheless. For example:

Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
Lemma app_equiv_eq l k1 k2 :
  l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
Lemma map_union_equiv_eq (m1 m2a m2b : M A) :
  m1 ≡ m2a ∪ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∪ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.

This MR adds such lemmas for all map operations, some lists operations.

For Some we had like 4 variants of the lemma. I removed all of those, and created a new lemma equiv_Some that follows the scheme for the other operations.


Concrete changes

Option:

  • Add Proper instances for union, union_with, intersection_with, and difference_with.
  • Rename equiv_None → None_equiv_eq.
  • Replace equiv_Some_inv_l, equiv_Some_inv_r, equiv_Some_inv_l', and equiv_Some_inv_r' by new lemma Some_equiv_eq that follows the pattern of other ≡-inversion lemmas: it uses a ↔ and puts the arguments of ≡ and = in consistent order.

List:

  • Add ≡-inversion lemmas nil_equiv_eq, cons_equiv_eq, list_singleton_equiv_eq, and app_equiv_eq.
  • Add lemmas Permutation_equiv and equiv_Permutation.

Maps:

  • Add map_filter_proper
  • Rename map_equiv_empty → map_empty_equiv_eq.
  • Add ≡-inversion lemmas insert_equiv_eq, delete_equiv_eq, map_union_equiv_eq, etc.
Edited Jun 17, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: robbert/setoid