Commit 474be0c3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Comment about partial inverse.

parent 5de3c7f7
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment