Merge branch 'robbert/cancelable' into 'master'

`Cancelable` instances for all elements of option/gmap

See merge request FP/iris-coq!127

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.

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.