From 0c360ec297c42d73c1090958d061447c2bfbe31b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 28 Jun 2020 23:48:06 +0100
Subject: Fix proof again with Verilog semantics changes

---
 src/verilog/Value.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src/verilog')

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 52a87e3..e7b2362 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -345,6 +345,18 @@ Proof.
   simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
 Qed.
 
+Lemma valueToPos_posToValue :
+  forall p, valueToPos (posToValueAuto p) = p.
+Proof.
+  intros. unfold valueToPos, posToValueAuto.
+  rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
+  split. apply Zle_0_pos.
+
+  assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.
+  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
+  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
+Qed.
+
 Lemma valueToInt_intToValue :
   forall v,
   valueToInt (intToValue v) = v.
-- 
cgit