From b225ccb1829ee0722a0130f91c0a914cd934652b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 5 Feb 2019 21:45:14 +0100
Subject: [PATCH] Monadic bind & join for `option` are non-expansive.

---
 theories/algebra/ofe.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d83c2b333..536fbbc6c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -959,6 +959,13 @@ Arguments optionC : clear implicits.
 Instance option_fmap_ne {A B : ofeT} n:
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
+Instance option_mbind_ne {A B : ofeT} n:
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind option _ A B).
+Proof. destruct 2; simpl; auto. Qed.
+Instance option_mjoin_ne {A : ofeT} n:
+  Proper (dist n ==> dist n) (@mjoin option _ A).
+Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
+
 Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
   CofeMor (fmap f : optionC A → optionC B).
 Instance optionC_map_ne A B : NonExpansive (@optionC_map A B).
-- 
GitLab