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
1 file
+ 0
9
Compare changes
  • Side-by-side
  • Inline
+ 0
9
@@ -119,15 +119,6 @@ Section basic_lemmas.
@@ -119,15 +119,6 @@ Section basic_lemmas.
Lemma elem_of_multiplicity x X : x X 0 < multiplicity x X.
Lemma elem_of_multiplicity x X : x X 0 < multiplicity x X.
Proof. done. Qed.
Proof. done. Qed.
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
Proof.
split.
- intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
- intros x y.
rewrite elem_of_multiplicity, multiplicity_singleton'.
destruct (decide (x = y)); intuition lia.
- intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
Qed.
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
Loading