From a037beca47152901155bf5c10f05dab22f856125 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 12 Mar 2021 18:08:07 +0000
Subject: Prove top-level theorem with admitted theorems

---
 src/hls/AssocMap.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/hls/AssocMap.v')

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 1d1b77f..98eda9c 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -97,6 +97,17 @@ Module AssocMapExt.
     Qed.
     Hint Resolve merge_correct_2 : assocmap.
 
+    Lemma merge_correct_3 :
+      forall am bm k,
+      get k am = None ->
+      get k bm = None ->
+      get k (merge am bm) = None.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_3 : assocmap.
+
     Definition merge_fold (am bm : t A) : t A :=
       fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).
 
-- 
cgit