From 3d553078d8150b6a95ce7c932ff9d39d241b44f8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 19:44:54 +0100
Subject: [PATCH] prove non-step-indexed fin_map validity lemmas

---
 algebra/fin_maps.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 6f19ff730..531010863 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -192,6 +192,13 @@ Proof.
   by move=>/(_ i); simplify_map_equality.
 Qed.
 
+Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x.
+Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed.
+Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
+Proof. intros ?? n j; apply map_insert_validN; auto. Qed.
+Lemma map_singleton_valid i x : ✓ ({[ i ↦ x ]} : gmap K A) ↔ ✓ x.
+Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed.
+
 Lemma map_insert_op_None m1 m2 i x :
   m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
-- 
GitLab