diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-12 18:08:07 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-12 18:08:07 +0000 |
| commit | a037beca47152901155bf5c10f05dab22f856125 (patch) | |
| tree | 81f00a95729bf644709dab8a82f4222dd4ad1ab5 /src/hls/AssocMap.v | |
| parent | 1df82be06ecda0e75b48159f525020dd08e7b00b (diff) | |
| download | vericert-a037beca47152901155bf5c10f05dab22f856125.tar.gz vericert-a037beca47152901155bf5c10f05dab22f856125.zip | |
Prove top-level theorem with admitted theorems
Diffstat (limited to 'src/hls/AssocMap.v')
| -rw-r--r-- | src/hls/AssocMap.v | 11 |
1 files changed, 11 insertions, 0 deletions
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). |