From a82770a13960d214a76265620096d0f266ca00cd Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Fri, 29 Apr 2016 15:22:57 -0400
Subject: Proved decode_point_eq in Ed25519 (comparing encodings is equivalent
 to comparing points).

---
 src/Util/WordUtil.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Util/WordUtil.v')

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index d655d046d..6a8831b14 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -46,6 +46,15 @@ Proof.
   rewrite pow2_id; assumption.
 Qed.
 
+Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
+Proof.
+  split; intros.
+  + intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
+  + case_eq (weqb x y); intros weqb_xy; auto.
+    apply weqb_true_iff in weqb_xy.
+    congruence.
+Qed.
+
 Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w
-- 
cgit v1.2.3