1 files changed, 17 insertions, 0 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 8dbc6b2..784f455 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -25,6 +25,7 @@ Require Import vericert.hls.ValueInt.
 Definition reg := positive.
 
 Module AssocMap := Maps.PTree.
+Module AssocMap_Properties := Maps.PTree_Properties.
 
 Module AssocMapExt.
   Import AssocMap.
@@ -243,3 +244,19 @@ Lemma find_get_assocmap :
   assoc ! r = Some v ->
   assoc # r = v.
 Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
+
+Lemma fso : forall m v k1 k2, k1 <> k2 -> (m # k1 <- v) # k2 = m # k2.
+Proof.
+  unfold "_ # _".
+  unfold AssocMapExt.get_default.
+  intros.
+  destruct_match; rewrite AssocMap.gso in Heqo by auto; rewrite Heqo; auto.
+Qed.
+
+Lemma fss : forall m v k, (m # k <- v) # k = v.
+Proof.
+  unfold "_ # _".
+  unfold AssocMapExt.get_default.
+  intros.
+  destruct_match; rewrite AssocMap.gss in Heqo by auto; inv Heqo; crush.
+Qed.