From 19aae59ad3806d286e6d3a07038da77ba99c29fd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Nov 2018 20:15:34 +0100
Subject: [PATCH] Prove that `fmap` on `option` and `gmap` is monotone.

---
 theories/algebra/cmra.v | 8 ++++++++
 theories/algebra/gmap.v | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 115ba5c50..b4aaea2c9 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1430,6 +1430,14 @@ Section option_prod.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
 End option_prod.
 
+Lemma option_fmap_mono {A B : cmraT} (f : A → B) ma mb :
+  Proper ((≡) ==> (≡)) f →
+  (∀ a b, a ≼ b → f a ≼ f b) →
+  ma ≼ mb → f <$> ma ≼ f <$> mb.
+Proof.
+  intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
+Qed.
+
 Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
   CmraMorphism (fmap f : option A → option B).
 Proof.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 592303372..1ae544dbc 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -474,6 +474,14 @@ Proof.
   apply (delete_local_update_cancelable m _ i (Some x));
     [done|by rewrite lookup_singleton].
 Qed.
+
+Lemma gmap_fmap_mono {B : ucmraT} (f : A → B) m1 m2 :
+  Proper ((≡) ==> (≡)) f →
+  (∀ x y, x ≼ y → f x ≼ f y) → m1 ≼ m2 → fmap f m1 ≼ fmap f m2.
+Proof.
+  intros ??. rewrite !lookup_included=> Hm i.
+  rewrite !lookup_fmap. by apply option_fmap_mono.
+Qed.
 End properties.
 
 Section unital_properties.
-- 
GitLab