Add `NonExpansive` instances for `!!!` on maps and lists.

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)).

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) := _.