From fa00f5df77c667ea4b2b43fe2303d0703f57dc26 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Sep 2023 17:55:37 +0200
Subject: [PATCH] add lemma lookup_insert_eq

---
 stdpp/fin_maps.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 596b3dbf..3eb4f8e0 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -528,6 +528,9 @@ Lemma lookup_insert_rev {A}  (m : M A) i x y : <[i:=x]>m !! i = Some y → x = y
 Proof. rewrite lookup_insert. congruence. Qed.
 Lemma lookup_insert_ne {A} (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
 Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+Lemma lookup_insert_eq {A} (m : M A) i j x :
+  <[i:=x]>m !! j = if decide (i = j) then Some x else m !! j.
+Proof. case_decide; simplify_eq; eauto using lookup_insert, lookup_insert_ne. Qed.
 Lemma lookup_total_insert_ne `{!Inhabited A} (m : M A) i j x :
   i ≠ j → <[i:=x]>m !!! j = m !!! j.
 Proof. intros. by rewrite lookup_total_alt, lookup_insert_ne. Qed.
-- 
GitLab