From 7227cf283f167dc13686ae5e46c9750f48ae2f36 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Sep 2016 16:22:59 +0200
Subject: [PATCH] Looking up into a gmap is a homomorphism.

---
 algebra/gmap.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/gmap.v b/algebra/gmap.v
index 5d658ea52..aa08442b1 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -195,6 +195,10 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
 
+Global Instance lookup_cmra_homomorphism :
+  UCMRAHomomorphism (lookup i : gmap K A → option A).
+Proof. split. split. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
+
 Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
 
-- 
GitLab