diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-20 10:50:37 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-20 10:50:37 +0100 |
commit | 333b306421d204e69deb1308352e31ffe53d2287 (patch) | |
tree | 1cafc892ee4fc60b87f998b3d9d46422d287298a /src/verilog/AssocMap.v | |
parent | b688e8bbf82e694cf62c11a117b67706d39f8459 (diff) | |
download | vericert-333b306421d204e69deb1308352e31ffe53d2287.tar.gz vericert-333b306421d204e69deb1308352e31ffe53d2287.zip |
Add theorems about merge
Diffstat (limited to 'src/verilog/AssocMap.v')
-rw-r--r-- | src/verilog/AssocMap.v | 14 |
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. |