From 3e77e2b40ca90ae4184700a05f886b3998c94ab4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2016 12:58:18 +0200
Subject: [PATCH] Insert and singleton maps are non-empty.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9abe5b0..0c5fb47 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -475,6 +475,10 @@ Proof.
 Qed.
 Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}.
 Proof. done. Qed.
+Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅.
+Proof.
+  intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi.
+Qed.
 
 (** ** Properties of the singleton maps *)
 Lemma lookup_singleton_Some {A} i j (x y : A) :
@@ -510,6 +514,8 @@ Proof.
   intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
     rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
 Qed.
+Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ ∅.
+Proof. apply insert_non_empty. Qed.
 
 (** ** Properties of the map operations *)
 Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ = ∅.
-- 
GitLab