diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:53 +0100 |
| commit | bb8a935f9143e65102a3a498a96dd13a3b8a4801 (patch) | |
| tree | 61549541968cc88b000275e18b37259bb365afe3 /src/verilog/AssocMap.v | |
| parent | d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b (diff) | |
| download | vericert-kvx-bb8a935f9143e65102a3a498a96dd13a3b8a4801.tar.gz vericert-kvx-bb8a935f9143e65102a3a498a96dd13a3b8a4801.zip | |
Add HTLgen
Diffstat (limited to 'src/verilog/AssocMap.v')
| -rw-r--r-- | src/verilog/AssocMap.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 9caa2d1..cac2c02 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -43,15 +43,14 @@ Module AssocMapExt. forall am am' r v, merge (add r v am) am' = add r v (merge am am'). Proof. - intros. - unfold merge. - Search fold_right. - apply SetoidList.fold_right_add2. + induction am; intros. + unfold merge. simpl. unfold fold_right. simpl. Search MapsTo. + Abort. Lemma merge_base : forall am, merge (empty elt) am = am. - Proof. intros. unfold merge. apply fold_1. Qed. + Proof. auto. Qed. End Operations. |