diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-06 11:49:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-06 11:49:32 +0100 |
commit | 74ac24f8dc099cc558d3b03b2f9303c89048f519 (patch) | |
tree | 35f830a82c1348d8f3c79ad1fbbc721f801bc4f0 /src/verilog/Value.v | |
parent | d530dc044242efdd4c5fafe13456cd05ac65beee (diff) | |
download | vericert-kvx-74ac24f8dc099cc558d3b03b2f9303c89048f519.tar.gz vericert-kvx-74ac24f8dc099cc558d3b03b2f9303c89048f519.zip |
Add changes to value
Diffstat (limited to 'src/verilog/Value.v')
-rw-r--r-- | src/verilog/Value.v | 11 |
1 files 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. |