Library stdpp.gmultiset
From stdpp Require Export countable.
From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import gmap.
From stdpp Require Import options.
Multisets gmultiset A are represented as maps from A to natural numbers,
which represent the multiplicity. To ensure we have canonical representations,
the multiplicity is a positive. Therefore, gmultiset_car !! x = None means
x has multiplicity 0 and gmultiset_car !! x = Some 1 means x has
multiplicity 1.
Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A positive }.
Global Arguments GMultiSet {_ _ _} _ : assert.
Global Arguments gmultiset_car {_ _ _} _ : assert.
Global Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined.
Global Program Instance gmultiset_countable `{Countable A} :
Countable (gmultiset A) := {|
encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
|}.
Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
Section definitions.
Context `{Countable A}.
Definition multiplicity (x : A) (X : gmultiset A) : nat :=
match gmultiset_car X !! x with Some n ⇒ Pos.to_nat n | None ⇒ 0 end.
Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
0 < multiplicity x X.
Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x,
multiplicity x X ≤ multiplicity x Y.
Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, ∀ x,
multiplicity x X = multiplicity x Y.
Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
let (X) := X in '(x,n) ← map_to_list X; replicate (Pos.to_nat n) x.
Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
Global Instance gmultiset_singleton : SingletonMS A (gmultiset A) := λ x,
GMultiSet {[ x := 1%positive ]}.
Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
let (X) := X in let (Y) := Y in
GMultiSet $ union_with (λ x y, Some (x `max` y)%positive) X Y.
Global Instance gmultiset_intersection : Intersection (gmultiset A) := λ X Y,
let (X) := X in let (Y) := Y in
GMultiSet $ intersection_with (λ x y, Some (x `min` y)%positive) X Y.
Often called the "sum"
Global Instance gmultiset_disj_union : DisjUnion (gmultiset A) := λ X Y,
let (X) := X in let (Y) := Y in
GMultiSet $ union_with (λ x y, Some (x + y)%positive) X Y.
Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
let (X) := X in let (Y) := Y in
GMultiSet $ difference_with (λ x y,
guard (y < x)%positive; Some (x - y)%positive) X Y.
Global Instance gmultiset_scalar_mul : ScalarMul nat (gmultiset A) := λ n X,
let (X) := X in GMultiSet $
match n with 0 ⇒ ∅ | _ ⇒ fmap (λ m, m × Pos.of_nat n)%positive X end.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom X.
End definitions.
Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
Section basic_lemmas.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Lemma gmultiset_eq X Y : X = Y ↔ ∀ x, multiplicity x X = multiplicity x Y.
Proof.
split; [by intros ->|intros HXY].
destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x.
specialize (HXY x); unfold multiplicity in *; simpl in ×.
repeat case_match; naive_solver lia.
Qed.
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
Global Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
Lemma multiplicity_empty x : multiplicity x ∅ = 0.
Proof. done. Qed.
Lemma multiplicity_singleton x : multiplicity x {[+ x +]} = 1.
Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[+ y +]} = 0.
Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
Lemma multiplicity_singleton' x y :
multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
Proof.
destruct (decide _) as [->|].
- by rewrite multiplicity_singleton.
- by rewrite multiplicity_singleton_ne.
Qed.
Lemma multiplicity_union X Y x :
multiplicity x (X ∪ Y) = multiplicity x X `max` multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_intersection X Y x :
multiplicity x (X ∩ Y) = multiplicity x X `min` multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_disj_union X Y x :
multiplicity x (X ⊎ Y) = multiplicity x X + multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_difference X Y x :
multiplicity x (X ∖ Y) = multiplicity x X - multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_difference_with.
destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Qed.
Lemma multiplicity_scalar_mul n X x :
multiplicity x (n *: X) = n × multiplicity x X.
Proof.
destruct X as [X]; unfold multiplicity; simpl. destruct n as [|n]; [done|].
rewrite lookup_fmap. destruct (X !! _); simpl; lia.
Qed.
Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
Proof. done. Qed.
Lemma gmultiset_elem_of_empty x : x ∈@{gmultiset A} ∅ ↔ False.
Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
Lemma gmultiset_elem_of_singleton x y : x ∈@{gmultiset A} {[+ y +]} ↔ x = y.
Proof.
rewrite elem_of_multiplicity, multiplicity_singleton'.
case_decide; naive_solver lia.
Qed.
Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_union. lia. Qed.
Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
Lemma gmultiset_elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_intersection. lia. Qed.
Lemma gmultiset_elem_of_scalar_mul n X x : x ∈ n *: X ↔ n ≠ 0 ∧ x ∈ X.
Proof. rewrite !elem_of_multiplicity, multiplicity_scalar_mul. lia. Qed.
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
End basic_lemmas.
let (X) := X in let (Y) := Y in
GMultiSet $ union_with (λ x y, Some (x + y)%positive) X Y.
Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
let (X) := X in let (Y) := Y in
GMultiSet $ difference_with (λ x y,
guard (y < x)%positive; Some (x - y)%positive) X Y.
Global Instance gmultiset_scalar_mul : ScalarMul nat (gmultiset A) := λ n X,
let (X) := X in GMultiSet $
match n with 0 ⇒ ∅ | _ ⇒ fmap (λ m, m × Pos.of_nat n)%positive X end.
Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
let (X) := X in dom X.
End definitions.
Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
Section basic_lemmas.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Lemma gmultiset_eq X Y : X = Y ↔ ∀ x, multiplicity x X = multiplicity x Y.
Proof.
split; [by intros ->|intros HXY].
destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x.
specialize (HXY x); unfold multiplicity in *; simpl in ×.
repeat case_match; naive_solver lia.
Qed.
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
Global Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
Lemma multiplicity_empty x : multiplicity x ∅ = 0.
Proof. done. Qed.
Lemma multiplicity_singleton x : multiplicity x {[+ x +]} = 1.
Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[+ y +]} = 0.
Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
Lemma multiplicity_singleton' x y :
multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
Proof.
destruct (decide _) as [->|].
- by rewrite multiplicity_singleton.
- by rewrite multiplicity_singleton_ne.
Qed.
Lemma multiplicity_union X Y x :
multiplicity x (X ∪ Y) = multiplicity x X `max` multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_intersection X Y x :
multiplicity x (X ∩ Y) = multiplicity x X `min` multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_disj_union X Y x :
multiplicity x (X ⊎ Y) = multiplicity x X + multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Qed.
Lemma multiplicity_difference X Y x :
multiplicity x (X ∖ Y) = multiplicity x X - multiplicity x Y.
Proof.
destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
rewrite lookup_difference_with.
destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Qed.
Lemma multiplicity_scalar_mul n X x :
multiplicity x (n *: X) = n × multiplicity x X.
Proof.
destruct X as [X]; unfold multiplicity; simpl. destruct n as [|n]; [done|].
rewrite lookup_fmap. destruct (X !! _); simpl; lia.
Qed.
Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
Proof. done. Qed.
Lemma gmultiset_elem_of_empty x : x ∈@{gmultiset A} ∅ ↔ False.
Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
Lemma gmultiset_elem_of_singleton x y : x ∈@{gmultiset A} {[+ y +]} ↔ x = y.
Proof.
rewrite elem_of_multiplicity, multiplicity_singleton'.
case_decide; naive_solver lia.
Qed.
Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_union. lia. Qed.
Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
Lemma gmultiset_elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
Proof. rewrite !elem_of_multiplicity, multiplicity_intersection. lia. Qed.
Lemma gmultiset_elem_of_scalar_mul n X x : x ∈ n *: X ↔ n ≠ 0 ∧ x ∈ X.
Proof. rewrite !elem_of_multiplicity, multiplicity_scalar_mul. lia. Qed.
Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
End basic_lemmas.
A solver for multisets
We define a tactic multiset_solver that solves goals involving multisets. The strategy of this tactic is as follows:- If the goal or some hypothesis contains multiplicity y X it adds the hypothesis H y.
- If P contains a multiset singleton {[ y ]} it adds the hypothesis H y. This is needed, for example, to prove ¬ ({[ x ]} ⊆ ∅), which is turned into hypothesis H : ∀ y, multiplicity y {[ x ]} ≤ 0 and goal False. The only way to make progress is to instantiate H with the singleton appearing in H, so variable x.
- First, we try to turn these occurencess into 1 or 0 if either x = y or x ≠ y can be proved using done, respectively.
- Second, we try to turn these occurences into a fresh z ≤ 1 if y does not occur elsewhere in the hypotheses or goal.
- Finally, we make a case distinction between x = y or x ≠ y. This step is done last so as to avoid needless exponential blow-ups.
Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
{ multiset_unfold : multiplicity x X = n }.
Global Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
Global Hint Mode MultisetUnfold + + + - + - : typeclass_instances.
Section multiset_unfold.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Global Instance multiset_unfold_default x X :
MultisetUnfold x X (multiplicity x X) | 1000.
Proof. done. Qed.
Global Instance multiset_unfold_empty x : MultisetUnfold x ∅ 0.
Proof. constructor. by rewrite multiplicity_empty. Qed.
Global Instance multiset_unfold_singleton x :
MultisetUnfold x {[+ x +]} 1.
Proof. constructor. by rewrite multiplicity_singleton. Qed.
Global Instance multiset_unfold_union x X Y n m :
MultisetUnfold x X n → MultisetUnfold x Y m →
MultisetUnfold x (X ∪ Y) (n `max` m).
Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_union, HX, HY. Qed.
Global Instance multiset_unfold_intersection x X Y n m :
MultisetUnfold x X n → MultisetUnfold x Y m →
MultisetUnfold x (X ∩ Y) (n `min` m).
Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_intersection, HX, HY. Qed.
Global Instance multiset_unfold_disj_union x X Y n m :
MultisetUnfold x X n → MultisetUnfold x Y m →
MultisetUnfold x (X ⊎ Y) (n + m).
Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_disj_union, HX, HY. Qed.
Global Instance multiset_unfold_difference x X Y n m :
MultisetUnfold x X n → MultisetUnfold x Y m →
MultisetUnfold x (X ∖ Y) (n - m).
Proof. intros [HX] [HY]; constructor. by rewrite multiplicity_difference, HX, HY. Qed.
Global Instance multiset_unfold_scalar_mul x m X n :
MultisetUnfold x X n →
MultisetUnfold x (m *: X) (m × n).
Proof. intros [HX]; constructor. by rewrite multiplicity_scalar_mul, HX. Qed.
Global Instance set_unfold_multiset_equiv X Y f g :
(∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
SetUnfold (X ≡ Y) (∀ x, f x = g x) | 0.
Proof.
constructor. apply forall_proper; intros x.
by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).
Qed.
Global Instance set_unfold_multiset_eq X Y f g :
(∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
SetUnfold (X = Y) (∀ x, f x = g x) | 0.
Proof. constructor. unfold_leibniz. by apply set_unfold_multiset_equiv. Qed.
Global Instance set_unfold_multiset_subseteq X Y f g :
(∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
SetUnfold (X ⊆ Y) (∀ x, f x ≤ g x) | 0.
Proof.
constructor. apply forall_proper; intros x.
by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).
Qed.
Global Instance set_unfold_multiset_subset X Y f g :
(∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
SetUnfold (X ⊂ Y) ((∀ x, f x ≤ g x) ∧ (¬∀ x, g x ≤ f x)) | 0.
Proof.
constructor. unfold strict. f_equiv.
- by apply set_unfold_multiset_subseteq.
- f_equiv. by apply set_unfold_multiset_subseteq.
Qed.
Global Instance set_unfold_multiset_elem_of X x n :
MultisetUnfold x X n → SetUnfoldElemOf x X (0 < n) | 100.
Proof. constructor. by rewrite <-(multiset_unfold x X n). Qed.
Global Instance set_unfold_gmultiset_empty x :
SetUnfoldElemOf x (∅ : gmultiset A) False.
Proof. constructor. apply gmultiset_elem_of_empty. Qed.
Global Instance set_unfold_gmultiset_singleton x y :
SetUnfoldElemOf x ({[+ y +]} : gmultiset A) (x = y).
Proof. constructor; apply gmultiset_elem_of_singleton. Qed.
Global Instance set_unfold_gmultiset_union x X Y P Q :
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ∪ Y) (P ∨ Q).
Proof.
intros ??; constructor. by rewrite gmultiset_elem_of_union,
(set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q).
Proof.
intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_gmultiset_intersection x X Y P Q :
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ∩ Y) (P ∧ Q).
Proof.
intros ??; constructor. rewrite gmultiset_elem_of_intersection.
by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
End multiset_unfold.
Step 3: instantiate hypotheses
Ltac multiset_instantiate :=
repeat match goal with
| H : (∀ x : ?A, @?P x) |- _ ⇒
let e := mk_evar A in
lazymatch constr:(P e) with
| context [ {[+ ?y +]} ] ⇒ unify y e; learn_hyp (H y)
end
| H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ ⇒ learn_hyp (H y)
| H : (∀ x : ?A, _) |- context [multiplicity ?y _] ⇒ learn_hyp (H y)
end.
repeat match goal with
| H : (∀ x : ?A, @?P x) |- _ ⇒
let e := mk_evar A in
lazymatch constr:(P e) with
| context [ {[+ ?y +]} ] ⇒ unify y e; learn_hyp (H y)
end
| H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ ⇒ learn_hyp (H y)
| H : (∀ x : ?A, _) |- context [multiplicity ?y _] ⇒ learn_hyp (H y)
end.
Step 4: simplify singletons This lemma results in information loss if there are other occurences of
y in the goal. In the tactic multiset_simplify_singletons we use clear y
to ensure we do not use the lemma if it leads to information loss.
Local Lemma multiplicity_singleton_forget `{Countable A} x y :
∃ n, multiplicity (A:=A) x {[+ y +]} = n ∧ n ≤ 1.
Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.
Ltac multiset_simplify_singletons :=
repeat match goal with
| H : context [multiplicity ?x {[+ ?y +]}] |- _ ⇒
first
[progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne in H by done
|destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
|rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
| |- context [multiplicity ?x {[+ ?y +]}] ⇒
first
[progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne by done
|destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
|rewrite multiplicity_singleton'; destruct (decide (x = y)); simplify_eq/=]
end.
∃ n, multiplicity (A:=A) x {[+ y +]} = n ∧ n ≤ 1.
Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.
Ltac multiset_simplify_singletons :=
repeat match goal with
| H : context [multiplicity ?x {[+ ?y +]}] |- _ ⇒
first
[progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne in H by done
|destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
|rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
| |- context [multiplicity ?x {[+ ?y +]}] ⇒
first
[progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne by done
|destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
|rewrite multiplicity_singleton'; destruct (decide (x = y)); simplify_eq/=]
end.
Putting it all together Similar to set_solver and naive_solver, multiset_solver has a by
parameter whose default is eauto.
Tactic Notation "multiset_solver" "by" tactic3(tac) :=
set_solver by (multiset_instantiate;
multiset_simplify_singletons;
solve [fast_done|lia|tac]).
Tactic Notation "multiset_solver" := multiset_solver by eauto.
Section more_lemmas.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
set_solver by (multiset_instantiate;
multiset_simplify_singletons;
solve [fast_done|lia|tac]).
Tactic Notation "multiset_solver" := multiset_solver by eauto.
Section more_lemmas.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
For union
Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) (∪).
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) (∪).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A}) ∅ (∪).
Proof. unfold LeftId. multiset_solver. Qed.
Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A}) ∅ (∪).
Proof. unfold RightId. multiset_solver. Qed.
Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) (∪).
Proof. unfold IdemP. multiset_solver. Qed.
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) (∪).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A}) ∅ (∪).
Proof. unfold LeftId. multiset_solver. Qed.
Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A}) ∅ (∪).
Proof. unfold RightId. multiset_solver. Qed.
Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) (∪).
Proof. unfold IdemP. multiset_solver. Qed.
For intersection
Global Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) (∩).
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) (∩).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold LeftAbsorb. multiset_solver. Qed.
Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold RightAbsorb. multiset_solver. Qed.
Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) (∩).
Proof. unfold IdemP. multiset_solver. Qed.
Lemma gmultiset_union_intersection_l X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_union_intersection_r X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_intersection_union_l X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_intersection_union_r X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
Proof. multiset_solver. Qed.
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) (∩).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold LeftAbsorb. multiset_solver. Qed.
Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A}) ∅ (∩).
Proof. unfold RightAbsorb. multiset_solver. Qed.
Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) (∩).
Proof. unfold IdemP. multiset_solver. Qed.
Lemma gmultiset_union_intersection_l X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_union_intersection_r X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_intersection_union_l X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_intersection_union_r X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
Proof. multiset_solver. Qed.
For disjoint union (aka sum)
Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) (⊎).
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) (⊎).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold LeftId. multiset_solver. Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold RightId. multiset_solver. Qed.
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.).
Proof. unfold Inj. multiset_solver. Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
Proof. unfold Inj. multiset_solver. Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_intersection_r X Y Z : (X ∩ Y) ⊎ Z = (X ⊎ Z) ∩ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_union_l X Y Z : X ⊎ (Y ∪ Z) = (X ⊎ Y) ∪ (X ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Proof. unfold Comm. multiset_solver. Qed.
Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) (⊎).
Proof. unfold Assoc. multiset_solver. Qed.
Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold LeftId. multiset_solver. Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
Proof. unfold RightId. multiset_solver. Qed.
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.).
Proof. unfold Inj. multiset_solver. Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
Proof. unfold Inj. multiset_solver. Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_intersection_r X Y Z : (X ∩ Y) ⊎ Z = (X ⊎ Z) ∩ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_union_l X Y Z : X ⊎ (Y ∪ Z) = (X ⊎ Y) ∪ (X ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Element of operation
Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
Proof. multiset_solver. Qed.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
Proof. multiset_solver. Qed.
Misc
Global Instance gmultiset_singleton_inj : Inj (=) (=@{gmultiset A}) singletonMS.
Proof.
intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
case_decide; [done|lia].
Qed.
Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Proof.
intros x1 x2 Hx. rewrite gmultiset_eq in Hx. specialize (Hx x1).
rewrite multiplicity_singleton, multiplicity_singleton' in Hx.
case_decide; [done|lia].
Qed.
Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Scalar
Lemma gmultiset_scalar_mul_0 X : 0 *: X = ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_S_l n X : S n *: X = X ⊎ (n *: X).
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_S_r n X : S n *: X = (n *: X) ⊎ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_1 X : 1 *: X = X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_2 X : 2 *: X = X ⊎ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_empty n : n *: ∅ =@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_disj_union n X Y :
n *: (X ⊎ Y) =@{gmultiset A} (n *: X) ⊎ (n *: Y).
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_union n X Y :
n *: (X ∪ Y) =@{gmultiset A} (n *: X) ∪ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_max_distr_l. Qed.
Lemma gmultiset_scalar_mul_intersection n X Y :
n *: (X ∩ Y) =@{gmultiset A} (n *: X) ∩ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_min_distr_l. Qed.
Lemma gmultiset_scalar_mul_difference n X Y :
n *: (X ∖ Y) =@{gmultiset A} (n *: X) ∖ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_sub_distr_l. Qed.
Lemma gmultiset_scalar_mul_inj_ne_0 n X1 X2 :
n ≠ 0 → n *: X1 = n *: X2 → X1 = X2.
Proof. set_unfold. intros ? HX x. apply (Nat.mul_reg_l _ _ n); auto. Qed.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_S_l n X : S n *: X = X ⊎ (n *: X).
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_S_r n X : S n *: X = (n *: X) ⊎ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_1 X : 1 *: X = X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_2 X : 2 *: X = X ⊎ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_empty n : n *: ∅ =@{gmultiset A} ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_disj_union n X Y :
n *: (X ⊎ Y) =@{gmultiset A} (n *: X) ⊎ (n *: Y).
Proof. multiset_solver. Qed.
Lemma gmultiset_scalar_mul_union n X Y :
n *: (X ∪ Y) =@{gmultiset A} (n *: X) ∪ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_max_distr_l. Qed.
Lemma gmultiset_scalar_mul_intersection n X Y :
n *: (X ∩ Y) =@{gmultiset A} (n *: X) ∩ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_min_distr_l. Qed.
Lemma gmultiset_scalar_mul_difference n X Y :
n *: (X ∖ Y) =@{gmultiset A} (n *: X) ∖ (n *: Y).
Proof. set_unfold. intros x; by rewrite Nat.mul_sub_distr_l. Qed.
Lemma gmultiset_scalar_mul_inj_ne_0 n X1 X2 :
n ≠ 0 → n *: X1 = n *: X2 → X1 = X2.
Proof. set_unfold. intros ? HX x. apply (Nat.mul_reg_l _ _ n); auto. Qed.
Specialized to S n so that type class search can find it.
Global Instance gmultiset_scalar_mul_inj_S n :
Inj (=) (=@{gmultiset A}) (S n *:.).
Proof. intros x1 x2. apply gmultiset_scalar_mul_inj_ne_0. lia. Qed.
Inj (=) (=@{gmultiset A}) (S n *:.).
Proof. intros x1 x2. apply gmultiset_scalar_mul_inj_ne_0. lia. Qed.
Conversion from lists
Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} ∅.
Proof. done. Qed.
Lemma list_to_set_disj_cons x l :
list_to_set_disj (x :: l) =@{gmultiset A} {[+ x +]} ⊎ list_to_set_disj l.
Proof. done. Qed.
Lemma list_to_set_disj_app l1 l2 :
list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2.
Proof. induction l1; multiset_solver. Qed.
Lemma elem_of_list_to_set_disj x l :
x ∈@{gmultiset A} list_to_set_disj l ↔ x ∈ l.
Proof. induction l; set_solver. Qed.
Global Instance list_to_set_disj_perm :
Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof. induction 1; multiset_solver. Qed.
Proof. done. Qed.
Lemma list_to_set_disj_cons x l :
list_to_set_disj (x :: l) =@{gmultiset A} {[+ x +]} ⊎ list_to_set_disj l.
Proof. done. Qed.
Lemma list_to_set_disj_app l1 l2 :
list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2.
Proof. induction l1; multiset_solver. Qed.
Lemma elem_of_list_to_set_disj x l :
x ∈@{gmultiset A} list_to_set_disj l ↔ x ∈ l.
Proof. induction l; set_solver. Qed.
Global Instance list_to_set_disj_perm :
Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
Proof. induction 1; multiset_solver. Qed.
Properties of the elements operation
Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = [].
Proof.
unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
Qed.
Lemma gmultiset_elements_empty_iff X : elements X = [] ↔ X = ∅.
Proof.
split; [|intros ->; by rewrite gmultiset_elements_empty].
destruct X as [X]; unfold elements, gmultiset_elements; simpl.
intros; apply (f_equal GMultiSet).
destruct (map_to_list X) as [|[x p]] eqn:?; simpl in ×.
- by apply map_to_list_empty_iff.
- pose proof (Pos2Nat.is_pos p). destruct (Pos.to_nat); naive_solver lia.
Qed.
Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
Proof. apply gmultiset_elements_empty_iff. Qed.
Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
Proof.
unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
Qed.
Lemma gmultiset_elements_disj_union X Y :
elements (X ⊎ Y) ≡ₚ elements X ++ elements Y.
Proof.
destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements.
set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
{ by rewrite (left_id_L _ _ Y), map_to_list_empty. }
destruct (Y !! x) as [n'|] eqn:HY.
- rewrite <-(insert_delete Y x n') by done.
erewrite <-insert_union_with by done.
rewrite !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
rewrite (assoc_L _). f_equiv.
rewrite (comm _); simpl. by rewrite Pos2Nat.inj_add, replicate_add.
- rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?HX, ?HY).
by rewrite <-(assoc_L (++)), <-IH.
Qed.
Lemma gmultiset_elements_scalar_mul n X :
elements (n *: X) ≡ₚ mjoin (replicate n (elements X)).
Proof.
induction n as [|n IH]; simpl.
- by rewrite gmultiset_scalar_mul_0, gmultiset_elements_empty.
- by rewrite gmultiset_scalar_mul_S_l, gmultiset_elements_disj_union, IH.
Qed.
Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X.
Proof.
destruct X as [X]. unfold elements, gmultiset_elements.
set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
rewrite elem_of_list_bind. split.
- intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
- intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
∃ (x,n); split; [|by apply elem_of_map_to_list].
apply elem_of_replicate; auto with lia.
Qed.
Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
Proof.
unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
Qed.
Lemma gmultiset_elements_empty_iff X : elements X = [] ↔ X = ∅.
Proof.
split; [|intros ->; by rewrite gmultiset_elements_empty].
destruct X as [X]; unfold elements, gmultiset_elements; simpl.
intros; apply (f_equal GMultiSet).
destruct (map_to_list X) as [|[x p]] eqn:?; simpl in ×.
- by apply map_to_list_empty_iff.
- pose proof (Pos2Nat.is_pos p). destruct (Pos.to_nat); naive_solver lia.
Qed.
Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
Proof. apply gmultiset_elements_empty_iff. Qed.
Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
Proof.
unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
Qed.
Lemma gmultiset_elements_disj_union X Y :
elements (X ⊎ Y) ≡ₚ elements X ++ elements Y.
Proof.
destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements.
set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
revert Y; induction X as [|x n X HX IH] using map_ind; intros Y.
{ by rewrite (left_id_L _ _ Y), map_to_list_empty. }
destruct (Y !! x) as [n'|] eqn:HY.
- rewrite <-(insert_delete Y x n') by done.
erewrite <-insert_union_with by done.
rewrite !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
rewrite (assoc_L _). f_equiv.
rewrite (comm _); simpl. by rewrite Pos2Nat.inj_add, replicate_add.
- rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?HX, ?HY).
by rewrite <-(assoc_L (++)), <-IH.
Qed.
Lemma gmultiset_elements_scalar_mul n X :
elements (n *: X) ≡ₚ mjoin (replicate n (elements X)).
Proof.
induction n as [|n IH]; simpl.
- by rewrite gmultiset_scalar_mul_0, gmultiset_elements_empty.
- by rewrite gmultiset_scalar_mul_S_l, gmultiset_elements_disj_union, IH.
Qed.
Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X.
Proof.
destruct X as [X]. unfold elements, gmultiset_elements.
set (f xn := let '(x, n) := xn in replicate (Pos.to_nat n) x); simpl.
unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl.
rewrite elem_of_list_bind. split.
- intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia.
- intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
∃ (x,n); split; [|by apply elem_of_map_to_list].
apply elem_of_replicate; auto with lia.
Qed.
Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
Proof.
unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
destruct (X !! x); naive_solver lia.
Qed.
Properties of the set_fold operation
Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) :
set_fold f b (∅ : gmultiset A) = b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed.
Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
set_fold f b ({[+ a +]} : gmultiset A) = f a b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y :
Comm (=) f →
Assoc (=) f →
set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y.
Proof.
intros Hcomm Hassoc. unfold set_fold; simpl.
by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)).
Qed.
Lemma gmultiset_set_fold_scalar_mul (f : A → A → A) (b : A) n X :
Comm (=) f →
Assoc (=) f →
set_fold f b (n *: X) = Nat.iter n (flip (set_fold f) X) b.
Proof.
intros Hcomm Hassoc. induction n as [|n IH]; simpl.
- by rewrite gmultiset_scalar_mul_0, gmultiset_set_fold_empty.
- rewrite gmultiset_scalar_mul_S_r.
by rewrite (gmultiset_set_fold_disj_union _ _ _ _ _ _), IH.
Qed.
set_fold f b (∅ : gmultiset A) = b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed.
Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
set_fold f b ({[+ a +]} : gmultiset A) = f a b.
Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y :
Comm (=) f →
Assoc (=) f →
set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y.
Proof.
intros Hcomm Hassoc. unfold set_fold; simpl.
by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)).
Qed.
Lemma gmultiset_set_fold_scalar_mul (f : A → A → A) (b : A) n X :
Comm (=) f →
Assoc (=) f →
set_fold f b (n *: X) = Nat.iter n (flip (set_fold f) X) b.
Proof.
intros Hcomm Hassoc. induction n as [|n IH]; simpl.
- by rewrite gmultiset_scalar_mul_0, gmultiset_set_fold_empty.
- rewrite gmultiset_scalar_mul_S_r.
by rewrite (gmultiset_set_fold_disj_union _ _ _ _ _ _), IH.
Qed.
Properties of the size operation
Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
Proof. done. Qed.
Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
Qed.
Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
Proof. apply gmultiset_size_empty_iff. Qed.
Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
Proof. by rewrite gmultiset_size_empty_iff. Qed.
Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- by apply gmultiset_elements_empty_iff.
- ∃ x. rewrite <-gmultiset_elem_of_elements, HX. by left.
Qed.
Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed.
Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
Proof.
intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|].
contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
Qed.
Lemma gmultiset_size_singleton x : size ({[+ x +]} : gmultiset A) = 1.
Proof.
unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
Qed.
Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite gmultiset_elements_disj_union, app_length.
Qed.
Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n × size X.
Proof.
induction n as [|n IH].
- by rewrite gmultiset_scalar_mul_0, gmultiset_size_empty.
- rewrite gmultiset_scalar_mul_S_l, gmultiset_size_disj_union, IH. lia.
Qed.
Proof. done. Qed.
Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
Qed.
Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
Proof. apply gmultiset_size_empty_iff. Qed.
Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
Proof. by rewrite gmultiset_size_empty_iff. Qed.
Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- by apply gmultiset_elements_empty_iff.
- ∃ x. rewrite <-gmultiset_elem_of_elements, HX. by left.
Qed.
Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed.
Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
Proof.
intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|].
contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
Qed.
Lemma gmultiset_size_singleton x : size ({[+ x +]} : gmultiset A) = 1.
Proof.
unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
Qed.
Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
Proof.
unfold size, gmultiset_size; simpl.
by rewrite gmultiset_elements_disj_union, app_length.
Qed.
Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n × size X.
Proof.
induction n as [|n IH].
- by rewrite gmultiset_scalar_mul_0, gmultiset_size_empty.
- rewrite gmultiset_scalar_mul_S_l, gmultiset_size_disj_union, IH. lia.
Qed.
Order stuff
Global Instance gmultiset_po : PartialOrder (⊆@{gmultiset A}).
Proof. repeat split; repeat intro; multiset_solver. Qed.
Local Lemma gmultiset_subseteq_alt X Y :
X ⊆ Y ↔
map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
Proof.
apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation Pos.le
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
by rewrite gmultiset_subseteq_alt.
Defined.
Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_subseteq_l X Y : X ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_subseteq_r X Y : Y ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ⊎ Y1 ⊆ X2 ⊎ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ⊎ Y1 ⊆ X ⊎ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ⊎ Y ⊆ X2 ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y.
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
Lemma gmultiset_disj_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_singleton_subseteq x y :
{[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
Proof. multiset_solver. Qed.
Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_difference' x Y :
x ∈ Y → Y = {[+ x +]} ⊎ Y ∖ {[+ x +]}.
Proof. multiset_solver. Qed.
Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
Proof.
intros HX%gmultiset_disj_union_difference.
rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
Qed.
Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_diag X : X ∖ X = ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_disj_union_r X Y Z : X ∖ Y = (X ⊎ Z) ∖ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_disj_union_l X Y Z : X ∖ Y = (Z ⊎ X) ∖ (Z ⊎ Y).
Proof. multiset_solver. Qed.
Proof. repeat split; repeat intro; multiset_solver. Qed.
Local Lemma gmultiset_subseteq_alt X Y :
X ⊆ Y ↔
map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
Proof.
apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation Pos.le
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
by rewrite gmultiset_subseteq_alt.
Defined.
Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_subseteq_l X Y : X ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_subseteq_r X Y : Y ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ⊎ Y1 ⊆ X2 ⊎ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ⊎ Y1 ⊆ X ⊎ Y2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ⊎ Y ⊆ X2 ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y.
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
Lemma gmultiset_disj_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_singleton_subseteq x y :
{[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
Proof. multiset_solver. Qed.
Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X.
Proof. multiset_solver. Qed.
Lemma gmultiset_disj_union_difference' x Y :
x ∈ Y → Y = {[+ x +]} ⊎ Y ∖ {[+ x +]}.
Proof. multiset_solver. Qed.
Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
Proof.
intros HX%gmultiset_disj_union_difference.
rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
Qed.
Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_diag X : X ∖ X = ∅.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y.
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_disj_union_r X Y Z : X ∖ Y = (X ⊎ Z) ∖ (Y ⊎ Z).
Proof. multiset_solver. Qed.
Lemma gmultiset_difference_disj_union_l X Y Z : X ∖ Y = (Z ⊎ X) ∖ (Z ⊎ Y).
Proof. multiset_solver. Qed.
Mononicity
Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
Proof.
intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
by apply submseteq_inserts_r.
Qed.
Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y.
Proof.
intros HXY. assert (size (Y ∖ X) ≠ 0).
{ by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
rewrite (gmultiset_disj_union_difference X Y),
gmultiset_size_disj_union by auto using gmultiset_subset_subseteq. lia.
Qed.
Proof.
intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
by apply submseteq_inserts_r.
Qed.
Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y.
Proof.
intros HXY. assert (size (Y ∖ X) ≠ 0).
{ by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
rewrite (gmultiset_disj_union_difference X Y),
gmultiset_size_disj_union by auto using gmultiset_subset_subseteq. lia.
Qed.
Well-foundedness
Lemma gmultiset_wf : wf (⊂@{gmultiset A}).
Proof.
apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Lemma gmultiset_ind (P : gmultiset A → Prop) :
P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
Proof.
intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
rewrite (gmultiset_disj_union_difference' x X) by done.
apply Hinsert, IH; multiset_solver.
Qed.
End more_lemmas.
Proof.
apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Lemma gmultiset_ind (P : gmultiset A → Prop) :
P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
Proof.
intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
rewrite (gmultiset_disj_union_difference' x X) by done.
apply Hinsert, IH; multiset_solver.
Qed.
End more_lemmas.