From 1aac61c43770099e09fc5ba6be0ec6f377fddbce Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 23 Sep 2016 12:58:18 +0200 Subject: [PATCH] Insert and singleton maps are non-empty. --- prelude/fin_maps.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v index 69c1f1c8..475777ff 100644 --- a/prelude/fin_maps.v +++ b/prelude/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