From b79eb4fed002997f56ec132f2015075c55895fe8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Mar 2018 19:54:36 +0100
Subject: [PATCH] `Cancelable` instances for gmap/option.

---
 theories/algebra/cmra.v | 4 ++++
 theories/algebra/gmap.v | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d0f5cffdd..115ba5c50 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1395,6 +1395,10 @@ Section option.
       by eapply (cmra_validN_le n); last lia.
     - done.
   Qed.
+
+  Global Instance option_cancelable (ma : option A) :
+    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
+  Proof. destruct ma; apply _. Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 5df537032..592303372 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -288,6 +288,12 @@ Proof.
   - by rewrite lookup_singleton_ne // !(left_id None _).
 Qed.
 
+Global Instance gmap_cancelable (m : gmap K A) :
+  (∀ x : A, IdFree x) → (∀ x : A, Cancelable x) → Cancelable m.
+Proof.
+  intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
+Qed.
+
 Lemma insert_op m1 m2 i x y :
   <[i:=x â‹… y]>(m1 â‹… m2) =  <[i:=x]>m1 â‹… <[i:=y]>m2.
 Proof. by rewrite (insert_merge (â‹…) m1 m2 i (x â‹… y) x y). Qed.
-- 
GitLab