From 74ac24f8dc099cc558d3b03b2f9303c89048f519 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 6 May 2020 11:49:32 +0100
Subject: Add changes to value

---
 src/verilog/Value.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 61f2652..8a0716d 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -186,13 +186,20 @@ Definition valueeqb (x y : value) : bool :=
   | right _ => false
   end.
 
+Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2).
+
+Theorem value_projZ_eqb_true :
+  forall v1 v2,
+  v1 = v2 -> value_projZ_eqb v1 v2 = true.
+Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed.
+
 Theorem valueeqb_true_iff :
   forall v1 v2,
   valueeqb v1 v2 = true <-> v1 = v2.
 Proof.
   split; intros.
-  unfold valueeqb in H. destruct (value_eq_size v1 v2).
-  Admitted.
+  unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?.
+  - destruct v1, v2. simpl in H.
 
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
 depending on the operation.
-- 
cgit