diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-21 16:47:20 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-21 16:47:20 -0400 |
commit | acd8180a1626ca35c19de7d797dd80e1e22f5799 (patch) | |
tree | 23cdc75f10c55a61a754ec1ef6a9a61709d18bc9 /src/Util | |
parent | 448e38eac815b0dce1b59d11011a65d1898deeaa (diff) |
Add word64eqb_Zeqb
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/WordUtil.v | 19 |
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. |