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
  • !192

Draft: Drop misleading gmultiset_simple_set instance

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:drop-gmultiset_simple_set into master Oct 10, 2020
  • Overview 9
  • Commits 1
  • Pipelines 0
  • Changes 1

The problem is that elem_of_subseteq_singleton applies to multiset goals, but uses the wrong instance.

[...] when my goal is a multiset elem-of, then apply gmultiset_elem_of_singleton_subseteq. and apply elem_of_subseteq_singleton. result in different goals that print exactly the same (also btw note the inconsistent lemma name)

Based on a suggestion by Robbert (which I might have misunderstood); but I'm not sure this is the right fix.

This instance appears to not be used, and it allows applying lemmas like elem_of_subseteq_singleton which are inappropriate for gmultiset, as they use the set_subseteq instance for SubsetEq, instead of gmultiset_subseteq : SubsetEq (gmultiset A).

However, the lemmas should be restated in terms of gmultiset, since they do hold, and they hold on sensible instances.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: drop-gmultiset_simple_set