diff options
Diffstat (limited to 'src/hls/AssocMap.v')
| -rw-r--r-- | src/hls/AssocMap.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 18b1bc0..4941b0e 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -304,3 +304,23 @@ Proof. unfold AssocMapExt.merge_atom. now rewrite !H. Qed. + +Lemma merge_left_gso : + forall A ars ars' d (v: A) r, + d <> r -> + (AssocMapExt.merge _ (ars # d <- v) ars') ! r = (AssocMapExt.merge _ ars ars') ! r. +Proof. + unfold AssocMapExt.merge; intros. + rewrite ! AssocMap.gcombine by auto. + now rewrite AssocMap.gso by auto. +Qed. + +Lemma merge_right_gso : + forall A ars ars' d (v: A) r, + d <> r -> + (AssocMapExt.merge _ ars (ars' # d <- v)) ! r = (AssocMapExt.merge _ ars ars') ! r. +Proof. + unfold AssocMapExt.merge; intros. + rewrite ! AssocMap.gcombine by auto. + now rewrite AssocMap.gso by auto. +Qed. |