From 13c7d213de3c1773ba740f8d6b4b97fd2b57bc57 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 13 Oct 2017 17:38:47 +0200
Subject: [PATCH] Add lemma lookup_gmap_uncurry_empty

---
 theories/gmap.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/gmap.v b/theories/gmap.v
index 874fff96..72ff8b6b 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -168,6 +168,19 @@ Section curry_uncurry.
     - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence.
   Qed.
 
+  Lemma lookup_gmap_uncurry_None (m : gmap (K1 * K2) A) i :
+    gmap_uncurry m !! i = None ↔ (∀ j, m !! (i, j) = None).
+  Proof.
+    apply (map_fold_ind (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None)));
+      [done|].
+    clear m; intros [i' j'] x m12 mr Hij' IH.
+    destruct (decide (i = i')) as [->|].
+    - split; [by rewrite lookup_partial_alter|].
+      intros Hi. specialize (Hi j'). by rewrite lookup_insert in Hi.
+    - rewrite lookup_partial_alter_ne, IH; [|done]. apply forall_proper.
+      intros j. rewrite lookup_insert_ne; [done|congruence].
+  Qed.
+
   Lemma gmap_curry_uncurry (m : gmap (K1 * K2) A) :
     gmap_curry (gmap_uncurry m) = m.
   Proof.
-- 
GitLab