From 474be0c3302a1f1be2ff0db2bfecb06477949e56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 May 2021 19:14:13 +0200
Subject: [PATCH] Comment about partial inverse.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 34bf85b6..8c9f5ffb 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2561,6 +2561,9 @@ Section kmap.
     setoid_rewrite eq_None_not_Some.
     rewrite lookup_kmap_is_Some. naive_solver.
   Qed.
+  (** Note that to state a lemma [map_kmap f m !! j = ...] we need to have a
+  partial inverse [f_inv] of [f] (which one cannot define constructively). Then
+  we could write [map_kmap f m !! j = (i ← f_inv j; m !! i)] *)
   Lemma lookup_kmap {A} (m : M1 A) (i : K1) :
     kmap f m !! (f i) = m !! i.
   Proof. apply option_eq. setoid_rewrite lookup_kmap_Some. naive_solver. Qed.
-- 
GitLab