From f6733c0048eacc911feff5277fed12fb544c7299 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 Feb 2016 13:46:07 -0500 Subject: Factor out some bedrock dependencies into WordUtil Also move a definition about words, with a TODO about location, into WordUtil. --- src/Util/WordUtil.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 src/Util/WordUtil.v (limited to 'src/Util/WordUtil.v') diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v new file mode 100644 index 000000000..49de971ef --- /dev/null +++ b/src/Util/WordUtil.v @@ -0,0 +1,27 @@ +Require Import NPeano. +Require Import ZArith.ZArith. +Require Import Bedrock.Word. + +Local Open Scope nat_scope. + +Lemma pow2_id : forall n, pow2 n = 2 ^ n. +Proof. + induction n; intros; simpl; auto. +Qed. + +Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)). +Proof. + induction n; intros; auto. + simpl pow2. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite untimes2. + rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega). + rewrite <- IHn. + auto. +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 + end)); abstract omega. Defined. -- cgit v1.2.3