Add more proofs and remove Admitted

2 files changed, 51 insertions, 16 deletions

diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index cac2c02..7db800b 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -26,6 +26,11 @@ Module AssocMap := PositiveMap.
 Module AssocMapExt.
   Import AssocMap.
 
+  Hint Resolve elements_3w : assocmap.
+  Hint Resolve elements_correct : assocmap.
+  Hint Resolve gss : assocmap.
+  Hint Resolve gso : assocmap.
+
   Section Operations.
 
     Variable elt : Type.
@@ -36,16 +41,40 @@ Module AssocMapExt.
       | Some v => v
       end.
 
-    Definition merge (m1 m2 : t elt) : t elt :=
-      fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1).
+    Definition merge (am bm : t elt) : t elt :=
+      fold_right (fun p a => add (fst p) (snd p) a) bm (elements am).
 
-    Lemma merge_add_assoc2 :
-      forall am am' r v,
-        merge (add r v am) am' = add r v (merge am am').
+    Lemma add_assoc :
+      forall k v l bm,
+      List.In (k, v) l ->
+      SetoidList.NoDupA (@eq_key elt) l ->
+      @find elt k (fold_right (fun p a => add (fst p) (snd p) a) bm l) = Some v.
     Proof.
-      induction am; intros.
-      unfold merge. simpl. unfold fold_right. simpl. Search MapsTo.
-      Abort.
+      Hint Resolve SetoidList.InA_alt : assocmap.
+      Hint Extern 1 (exists _, _) => apply list_in_map_inv : assocmap.
+
+      induction l; intros.
+      - contradiction.
+      - destruct a as [k' v'].
+        destruct (peq k k').
+        + inversion H. inversion H1. inversion H0. subst.
+          simpl. auto with assocmap.
+
+          subst. inversion H0. subst. apply in_map with (f := fst) in H1. simpl in *.
+          unfold not in H4. exfalso. apply H4. apply SetoidList.InA_alt.
+          auto with assocmap.
+
+        + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption.
+          apply IHl. contradiction. contradiction.
+          simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption.
+    Qed.
+    Hint Resolve add_assoc : assocmap.
+
+    Lemma merge_add :
+      forall k v am bm,
+      find k am = Some v ->
+      find k (merge am bm) = Some v.
+    Proof. unfold merge. auto with assocmap. Qed.
 
     Lemma merge_base :
       forall am,
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 0ce0bc5..34cb0d2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -85,10 +85,11 @@ Definition intToValue (i : Integers.int) : value :=
 Definition valueToInt (i : value) : Integers.int :=
   Int.repr (valueToZ i).
 
-Definition valToValue (v : Values.val) :=
+Definition valToValue (v : Values.val) : option value :=
   match v with
-  | Values.Vint i => intToValue i
-  | _ => ZToValue 32 0%Z
+  | Values.Vint i => Some (intToValue i)
+  | Values.Vundef => Some (ZToValue 32 0%Z)
+  | _ => None
   end.
 
 (** Convert a [value] to a [bool], so that choices can be made based on the
@@ -295,17 +296,22 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
-Search Z positive.
-
-Search "wordToZ".
+Lemma valueToZ_ZToValue :
+  forall n z,
+  (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
+  valueToZ (ZToValue (S n) z) = z.
+Proof.
+  unfold valueToZ, ZToValue. simpl.
+  auto using wordToZ_ZToWord.
+Qed.
 
 Lemma uvalueToZ_ZToValue :
   forall n z,
   (0 <= z < 2 ^ Z.of_nat n)%Z ->
   uvalueToZ (ZToValue n z) = z.
 Proof.
-  intros. unfold uvalueToZ, ZToValue. simpl.
-  apply uwordToZ_ZToWord. apply H.
+  unfold uvalueToZ, ZToValue. simpl.
+  auto using uwordToZ_ZToWord.
 Qed.
 
 Lemma valueToPos_posToValueAuto :