From bb2262ee7cf7d83cc73d6f33095d143b0ac1b002 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2022 09:31:05 +0200
Subject: [PATCH] Add lemma `lookup_total_preimage`.
---
theories/fin_maps.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 33533c8c..29738bea 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3355,6 +3355,14 @@ Section preimage.
+ apply set_choose_L in HXne as [j ?].
apply (lookup_preimage_None_1 _ _ j) in HX'. naive_solver.
Qed.
+
+ Lemma lookup_total_preimage m x i :
+ i ∈ map_preimage m !!! x ↔ m !! i = Some x.
+ Proof.
+ rewrite lookup_total_alt. destruct (map_preimage m !! x) as [X|] eqn:HX.
+ - by apply lookup_preimage_Some.
+ - rewrite lookup_preimage_None in HX. set_solver.
+ Qed.
End preimage.
(** * Tactics *)
--
GitLab