From 37762bb834f77154782c1903fcbb5a24f5dce88c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 23 Feb 2019 14:12:32 +0100 Subject: [PATCH] Bit of refactoring for multiset singleton. --- theories/gmultiset.v | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/theories/gmultiset.v b/theories/gmultiset.v index be9c491..7b2e6dc 100644 --- a/theories/gmultiset.v +++ b/theories/gmultiset.v @@ -83,6 +83,13 @@ 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. @@ -117,10 +124,9 @@ Global Instance gmultiset_simple_set : SemiSet A (gmultiset A). Proof. split. - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia. - - intros x y. destruct (decide (x = y)) as [->|]. - + rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia. - + rewrite elem_of_multiplicity, multiplicity_singleton_ne by done. - by split; auto with 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}). @@ -411,9 +417,8 @@ Proof. rewrite (comm_L (⊎)). apply gmultiset_disj_union_subset_l. Qed. Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X. Proof. rewrite elem_of_multiplicity. split. - - intros Hx y; destruct (decide (x = y)) as [->|]. - + rewrite multiplicity_singleton; lia. - + rewrite multiplicity_singleton_ne by done; lia. + - intros Hx y. rewrite multiplicity_singleton'. + destruct (decide (y = x)); naive_solver lia. - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia. Qed. -- 2.26.2