diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-07-31 11:36:57 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-31 11:36:57 +0100 |
| commit | 13cd1c16d36402318150615475de85ac3b2cff52 (patch) | |
| tree | f5b4c8c3ac2854e28666eeb4ef653344af5efa31 /src/hls/AssocMap.v | |
| parent | 502e49e2f8c95b40cd0761cbb69c863904169f8b (diff) | |
| download | vericert-13cd1c16d36402318150615475de85ac3b2cff52.tar.gz vericert-13cd1c16d36402318150615475de85ac3b2cff52.zip | |
Remove RTLParFu and fix DMemorygen.v
Diffstat (limited to 'src/hls/AssocMap.v')
| -rw-r--r-- | src/hls/AssocMap.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 0c9242c..18b1bc0 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -256,3 +256,51 @@ Lemma find_get_assocmap : assoc ! r = Some v -> assoc # r = v. Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. + +Lemma merge_get_default : + forall ars ars' r x, + ars ! r = Some x -> + (AssocMapExt.merge _ ars ars') # r = x. +Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. +Qed. + +Lemma merge_get_default2 : + forall ars ars' r, + ars ! r = None -> + (AssocMapExt.merge _ ars ars') # r = ars' # r. +Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. +Qed. + +Lemma merge_get_default3 : + forall A ars ars' r, + ars ! r = None -> + (AssocMapExt.merge A ars ars') ! r = ars' ! r. +Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. +Qed. + +Lemma merge_get_default4 : + forall A ars ars' r x, + ars ! r = Some x -> + (AssocMapExt.merge A ars ars') ! r = Some x. +Proof. + unfold AssocMapExt.merge; intros. + unfold "#", AssocMapExt.get_default. + rewrite AssocMap.gcombine by auto. + unfold AssocMapExt.merge_atom. + now rewrite !H. +Qed. |