From cd83b336eb9aaf035eaea4c43789198e119d43c0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 Nov 2020 15:51:07 +0100
Subject: [PATCH] comment to explain what happens in big_opM_singletons
---
theories/algebra/gmap.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 13208c8d1..04ecf90e5 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -598,6 +598,11 @@ Qed.
Lemma big_opM_singletons m :
([^op map] k ↦ x ∈ m, {[ k := x ]}) = m.
Proof.
+ (* We are breaking the big_opM abstraction here. The reason is that [map_ind]
+ is too weak: we need an induction principle that visits all the keys in the
+ right order, namely the order in which they appear in map_to_list. Here,
+ we achieve this by unfolding [big_opM] and doing induction over that list
+ instead. *)
rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.
--
GitLab