diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-01 14:49:17 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-01 14:49:17 +0100 |
| commit | a4c5420b851d64c8b6612d1e4c7da2aef29c5b65 (patch) | |
| tree | 1f68565477aeaff8437104fbed8ce52f33d1a81b /src/hls/AssocMap.v | |
| parent | d83c0e1c96c01cee3c8a1c30aca3feca75f4b4da (diff) | |
| download | vericert-a4c5420b851d64c8b6612d1e4c7da2aef29c5b65.tar.gz vericert-a4c5420b851d64c8b6612d1e4c7da2aef29c5b65.zip | |
Fixing store transformation
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. |