diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-04 20:03:10 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-04 20:03:10 +0100 |
| commit | b71b75aa7f9e4db0575b01cf25b7ad6dd88abff4 (patch) | |
| tree | aa68fd9ad6cf8562991d1aded1548c93a4d9b7c1 /src/verilog/AssocMap.v | |
| parent | 971b35fd4af24cfffc462df13f8c5b9be982858e (diff) | |
| download | vericert-b71b75aa7f9e4db0575b01cf25b7ad6dd88abff4.tar.gz vericert-b71b75aa7f9e4db0575b01cf25b7ad6dd88abff4.zip | |
Finished main proof with small assumptions
Diffstat (limited to 'src/verilog/AssocMap.v')
| -rw-r--r-- | src/verilog/AssocMap.v | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 88b13a6..5d531d5 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -202,9 +202,16 @@ Ltac unfold_merge := unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); rewrite AssocMapExt.merge_base_1. -Module AssocMapNotation. - Notation "a ! b" := (AssocMap.get b a) (at level 1). - Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). - Notation "a # b" := (find_assocmap 32 b a) (at level 1). - Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). -End AssocMapNotation. +Declare Scope assocmap. +Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. +Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. +Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. +Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. +Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. + +Local Open Scope assocmap. +Lemma find_get_assocmap : + forall assoc r v, + assoc ! r = Some v -> + assoc # r = v. +Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. |