blob: 17d04c60a9ab317e87dcc32cdf7d3661a2f4cefe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.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.
|
