Add word64eqb_Zeqb

1 files changed, 18 insertions, 1 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index a89d02364..f2ceb047f 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -140,4 +140,21 @@ Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w)
 Admitted.
 
 Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
-Admitted.
\ No newline at end of file
+Admitted.
+
+Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y.
+Proof.
+  match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end;
+    repeat match goal with
+           | _ => reflexivity
+           | _ => progress unfold not in *
+           | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
+           | [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq
+           | [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H
+           | [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H
+           | [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H
+           | [ H : ?x = false |- _ ] => progress rewrite <- H; clear H
+           | _ => congruence
+           | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst
+           end.
+Qed.