From 649c6e792404adbcd3954c21895b6f33684c6a5e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Jul 2019 14:27:00 +0200
Subject: [PATCH] Stronger local update for multisets that entails the old
 ones.

---
 theories/algebra/gmultiset.v | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index a9acacd07..576918daa 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -61,19 +61,22 @@ Section gmultiset.
   Lemma gmultiset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X ⊎ X', Y ⊎ X').
+  Lemma gmultiset_local_update X Y X' Y' : X ⊎ Y' = X' ⊎ Y → (X,Y) ~l~> (X', Y').
   Proof.
-    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite !gmultiset_op_disj_union.
-    by rewrite -!assoc (comm _ Z' X').
+    intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
+    split; first done. apply leibniz_equiv_iff, (inj (⊎ Y)).
+    rewrite -HXY !gmultiset_op_disj_union.
+    by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
   Qed.
 
+  Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X ⊎ X', Y ⊎ X').
+  Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
+
   Lemma gmultiset_local_update_dealloc X Y X' :
     X' ⊆ X → X' ⊆ Y → (X,Y) ~l~> (X ∖ X', Y ∖ X').
   Proof.
     intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
-    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
-    split. done. rewrite !gmultiset_op_disj_union=> x.
+    apply gmultiset_local_update. apply gmultiset_eq=> x.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
   Qed.
-- 
GitLab