From fa43870237b14e5ec02ceea05655d6617ddc0ba8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Apr 2020 17:35:22 +0200
Subject: [PATCH] Add `NonExpansive` instances for `!!!` on maps and lists.

---
 theories/algebra/gmap.v | 5 ++++-
 theories/algebra/list.v | 3 +++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 01d97b757..3a5cbe52a 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -45,7 +45,10 @@ Global Instance gmapO_leibniz: LeibnizEquiv A → LeibnizEquiv gmapO.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
 Global Instance lookup_ne k : NonExpansive (lookup k : gmap K A → option A).
-Proof. by intros m1 m2. Qed.
+Proof. by intros n m1 m2. Qed.
+Global Instance lookup_total_ne `{!Inhabited A} k :
+  NonExpansive (lookup_total k : gmap K A → A).
+Proof. intros n m1 m2. rewrite !lookup_total_alt. by intros ->. Qed.
 Global Instance partial_alter_ne n :
   Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
          (partial_alter (M:=gmap K A)).
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 492ffe0b3..a6d5d0f92 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -23,6 +23,9 @@ Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
 Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Global Instance list_lookup_total_ne `{!Inhabited A} i :
+  NonExpansive (lookup_total (M:=list A) i).
+Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
 Global Instance list_alter_ne n f i :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
-- 
GitLab