From 333b306421d204e69deb1308352e31ffe53d2287 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 20 May 2020 10:50:37 +0100 Subject: Add theorems about merge --- src/verilog/AssocMap.v | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'src/verilog') 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. -- cgit