From 2927fef17d9c4670cb01d95b7098bc87608c49a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Apr 2021 12:05:39 +0200
Subject: [PATCH] Add lemma `map_seq_ne`.
---
iris/algebra/gmap.v | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 2f74ff9c5..d5ed50970 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,5 +1,5 @@
From stdpp Require Export list gmap.
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export list cmra.
From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
@@ -97,6 +97,13 @@ Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
End ofe.
+Global Instance map_seq_ne {A : ofe} start :
+ NonExpansive (map_seq (M:=gmap nat A) start).
+Proof.
+ intros n l1 l2 Hl. revert start.
+ induction Hl; intros; simpl; repeat (done || f_equiv).
+Qed.
+
Global Arguments gmapO _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
--
GitLab