From 5cfa4af9c6e4d9703e3142c24ae78c7da0ac575f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 4 May 2020 16:13:16 +0100
Subject: Add equality check for value

---
 src/verilog/Value.v   | 36 +++++++++++++++++++++---------------
 src/verilog/Verilog.v |  2 +-
 2 files changed, 22 insertions(+), 16 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 21e59be..4cacab5 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -149,24 +149,30 @@ Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value)
   | _ => None
   end.
 
-Lemma eqvalue {sz : nat} (x y : word sz) : x = y -> (mkvalue sz x = mkvalue sz y).
-Proof. intros. subst. reflexivity. Qed.
 
-Lemma nevalue {sz : nat} (x y : word sz) : x <> y -> (mkvalue sz x <> mkvalue sz y).
-Proof. Admitted.
+Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y.
+Proof.
+  split; intros.
+  subst. reflexivity. inversion H. apply existT_wordToZ in H1.
+  apply wordToZ_inj. assumption.
+Qed.
+
+Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y.
+Proof. apply eqvalue. Qed.
+
+Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y.
+Proof. split; intros; intuition. apply H. apply eqvalue. assumption.
+       apply H. rewrite H0. trivial.
+Qed.
 
-Definition valueEqCheck (sz : nat) (x y : word sz) :
+Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y.
+Proof. apply nevalue. Qed.
+
+Definition valueEq (sz : nat) (x y : word sz) :
   {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} :=
   match weq x y with
-  | left eq => left (eqvalue x y eq)
-  | right ne => right (nevalue x y ne)
-  end.
-
-Definition valueEq (x y : value) (EQ : vsize x = vsize y): {x = y} + {x <> y} :=
-  let unif_y := unify_word (vsize x) (vsize y) (vword y) EQ in
-  match weq (vword x) unif_y with
-  | left _ => left _
-  | right _ => right _
+  | left eq => left (eqvaluef x y eq)
+  | right ne => right (nevaluef x y ne)
   end.
 
 (** Arithmetic operations over [value], interpreting them as signed or unsigned
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index a927eac..756dc12 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
-- 
cgit