Add theorems about merge

1 files changed, 12 insertions, 2 deletions

diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index e550072..bd61c8e 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -30,14 +30,24 @@ Module AssocMapExt.
 
     Variable elt : Type.
 
-    Definition merge : t elt -> t elt -> t elt := fold (@add elt).
-
     Definition find_default (a : elt) (k : reg) (m : t elt) : elt :=
       match find k m with
       | None => a
       | Some v => v
       end.
 
+    Definition merge : t elt -> t elt -> t elt := fold (@add elt).
+
+    Lemma merge_add_assoc :
+      forall am am' r v x,
+        find x (merge (add r v am) am') = find x (add r v (merge am am')).
+    Admitted.
+
+    Lemma merge_base :
+      forall am,
+        merge (empty elt) am = am.
+    Proof. intros. unfold merge. apply fold_1. Qed.
+
   End Operations.
 
 End AssocMapExt.