From 31e8abdd050a4cfe180c15895e1e6594ab6f38c6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 14:27:03 +0200
Subject: [PATCH] add insert_map_seq_0
---
theories/fin_maps.v | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ab01036c..a6211d3e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2966,7 +2966,7 @@ Proof.
Qed.
End theorems.
-(** ** The seq operation *)
+(** ** The [map_seq] operation *)
Section map_seq.
Context `{FinMap nat M} {A : Type}.
Implicit Types x : A.
@@ -3054,6 +3054,16 @@ Section map_seq.
{ by rewrite fmap_empty. }
by rewrite fmap_insert, IH.
Qed.
+
+ Lemma insert_map_seq_0 (xs : list A) i x:
+ i < length xs →
+ <[i:=x]> (map_seq (M:=M A) 0 xs) = map_seq 0 (<[i:=x]> xs).
+ Proof.
+ intros ?. apply map_eq. intros j. rewrite lookup_map_seq_0.
+ destruct (decide (i = j)) as [->|Hne].
+ - rewrite lookup_insert, list_lookup_insert; done.
+ - rewrite lookup_insert_ne, lookup_map_seq_0, list_lookup_insert_ne; done.
+ Qed.
End map_seq.
Section kmap.
--
GitLab