Skip to content
Snippets Groups Projects

Draft: Drop misleading gmultiset_simple_set instance

Closed Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:drop-gmultiset_simple_set into master
2 unresolved threads

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.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • However, the lemmas should be restated in terms of gmultiset, since they do hold, and they hold on sensible instances.

    Without sugar, this is an instance for:

    A: Type
    EqDecision0: @RelDecision A A (@eq A)
    H: @Countable A EqDecision0
    ————————————————————————————————————————————————————————————————————————————————
    @SemiSet A (@gmultiset A EqDecision0 H) (@gmultiset_elem_of A EqDecision0 H)
      (@gmultiset_empty A EqDecision0 H) (@gmultiset_singleton A EqDecision0 H)
      (@gmultiset_union A EqDecision0 H)

    That is:

    1/3
     x : A, x  
    2/3
     x y : A, x  {[y]}  x = y
    3/3
     (X Y : gmultiset A) (x : A), x  X  Y  x  X  x  Y

    or

    1/3
    forall x : A,
    not
      (@elem_of A (@gmultiset A EqDecision0 H)
         (@gmultiset_elem_of A EqDecision0 H) x
         (@empty (@gmultiset A EqDecision0 H) (@gmultiset_empty A EqDecision0 H)))
    2/3
    forall x y : A,
    iff
      (@elem_of A (@gmultiset A EqDecision0 H)
         (@gmultiset_elem_of A EqDecision0 H) x
         (@singleton A (@gmultiset A EqDecision0 H)
            (@gmultiset_singleton A EqDecision0 H) y)) 
      (@eq A x y)
    3/3
    forall (X Y : @gmultiset A EqDecision0 H) (x : A),
    iff
      (@elem_of A (@gmultiset A EqDecision0 H)
         (@gmultiset_elem_of A EqDecision0 H) x
         (@union (@gmultiset A EqDecision0 H) (@gmultiset_union A EqDecision0 H)
            X Y))
      (or
         (@elem_of A (@gmultiset A EqDecision0 H)
            (@gmultiset_elem_of A EqDecision0 H) x X)
         (@elem_of A (@gmultiset A EqDecision0 H)
            (@gmultiset_elem_of A EqDecision0 H) x Y))
  • Ralf Jung
    Ralf Jung @jung started a thread on the diff
119 119 Lemma elem_of_multiplicity x X : x X 0 < multiplicity x X.
120 120 Proof. done. Qed.
121 121
122 Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
123 Proof.
124 split.
125 - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
126 - intros x y.
127 rewrite elem_of_multiplicity, multiplicity_singleton'.
128 destruct (decide (x = y)); intuition lia.
129 - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
130 Qed.
  • Ah, so this way we have two "subseteq" instances, I see.

    Maybe add a comment explaining that this instance deliberately does not exist?

  • Please register or sign in to reply
  • @robbertkrebbers I also recall us discussing the Union and DisjUnion instances... what was the argument again for gmultiset even having a Union instance? It is very confusing, I just recently saw someone using it when really they meant disj-union.

    In contrast, Difference works as one would expect for multisets.

  • Hm, fair... I guess it is symmetric with intersection.

    • Testing Iris, big_opMS_None breaks because it relies on set_solver which of course breaks, and multiset_solver fails as well.

    • While somebody (not me) could replicate the needed infrastructure for multisets, I suspect conditioning set_subseteq on some "tagging" typeclass (with instances for everything sensible but gmultiset) might be a better way forward?

    • For the record, that's the only breakage in Iris, but it confirms my feeling that this is not the right fix.

      And since I don't want to "own" the issue and stop progress, I'd like to close this MR. Feel free to continue discussing here or link to a thread.

    • For the record, here is the failure:

      $ COQPATH=livelibs make -j10
      COQDEP VFILES
      COQC theories/algebra/cmra_big_op.v
      File "./theories/algebra/cmra_big_op.v", line 33, characters 28-38:
      Error: No matching clauses for match.
      
      Command exited with non-zero status 1
      theories/algebra/cmra_big_op (real: 1.83, user: 1.32, sys: 0.27, mem: 482344 ko)
      make[2]: *** [theories/algebra/cmra_big_op.vo] Error 1
      make[1]: *** [all] Error 2
      make: *** [all] Error 2
    • Please register or sign in to reply
  • mentioned in issue #87 (closed)

  • Please register or sign in to reply
    Loading