Draft: Drop misleading gmultiset_simple_set instance
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.
andapply 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
Activity
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))
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. @robbertkrebbers I also recall us discussing the
Union
andDisjUnion
instances... what was the argument again for gmultiset even having aUnion
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.Union on multisets is usually defined as the max. See e.g., https://en.wikipedia.org/wiki/Multiset#Basic_properties_and_operations
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
mentioned in issue #87 (closed)