From acd8180a1626ca35c19de7d797dd80e1e22f5799 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 21 Oct 2016 16:47:20 -0400 Subject: Add word64eqb_Zeqb --- src/Util/WordUtil.v | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'src/Util/WordUtil.v') 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. -- cgit v1.2.3