Commit 425c0d18 authored by Robbert Krebbers's avatar Robbert Krebbers

Lemma for `x ∈ _ ⊎ _` on multisets.

parent 5eabf109
Pipeline #14886 passed with stage
in 7 minutes and 20 seconds
...@@ -126,12 +126,14 @@ Qed. ...@@ -126,12 +126,14 @@ 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.
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.
Global Instance set_unfold_gmultiset_disj_union x X Y P Q : Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
SetUnfold (x X) P SetUnfold (x Y) Q SetUnfold (x X Y) (P Q). SetUnfold (x X) P SetUnfold (x Y) Q SetUnfold (x X Y) (P Q).
Proof. Proof.
intros ??; constructor. intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
rewrite <-(set_unfold (x X) P), <-(set_unfold (x Y) Q). by rewrite <-(set_unfold (x X) P), <-(set_unfold (x Y) Q).
rewrite !elem_of_multiplicity, multiplicity_disj_union. lia.
Qed. Qed.
(* Algebraic laws *) (* Algebraic laws *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment