diff options
author | Rob Sloan <varomodt@google.com> | 2016-11-09 12:48:01 -0800 |
---|---|---|
committer | Rob Sloan <varomodt@google.com> | 2016-11-09 12:48:01 -0800 |
commit | 9e32f8427ed7b64b8f29f331a6154679d8cc59f8 (patch) | |
tree | eabacf6c3125120aa8d6aa89813c1719dec9ab24 /src/Util/WordUtil.v | |
parent | 759b1b8bd212d953ba1e2da0506bccf1ef616f8c (diff) | |
parent | 363af9e129eda8a05db701e75c3935c23f85ee98 (diff) |
Rebase + remove WordizeUtil dependency from Z/Interpretations
Diffstat (limited to 'src/Util/WordUtil.v')
-rw-r--r-- | src/Util/WordUtil.v | 53 |
1 files changed, 45 insertions, 8 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 4c74fe9b4..f0e6ef335 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,6 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.ZArith.ZArith. +Require Import Coq.NArith.NArith. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Tactics. Require Import Bedrock.Word. @@ -51,6 +52,32 @@ Proof. auto. Qed. +Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N. +Proof. + intros; induction x. + + - simpl; apply N.lt_1_r; intuition. + + - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition. + apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0. + + + intuition; inversion H. + + + apply N.neq_0_lt_0 in IHx; intuition. +Qed. + +Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N. +Proof. + induction n. + + - simpl; intuition. + + - rewrite Nat2N.inj_succ. + rewrite N.pow_succ_r; try apply N_ge_0. + rewrite <- IHn. + simpl; intuition. +Qed. + Lemma Npow2_Zlog2 : forall x n, (Z.log2 (Z.of_N x) < Z.of_nat n)%Z -> (x < Npow2 n)%N. @@ -243,16 +270,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*. Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *) Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances. -Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m := - match n, m return wordsize_eq n m -> word n -> word m with - | O, O => fun _ _ => WO - | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w)) - | _, _ => fun _ _ => ! +Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y + := match x, y with + | O, O => fun _ => eq_refl + | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf)) + | _, _ => fun x => x + end. + +Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl. +Proof. + induction n; [ reflexivity | simpl ]. + rewrite IHn; reflexivity. +Qed. + +Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m := + match correct_wordsize_eq n m pf in _ = y return word n -> word y with + | eq_refl => fun w => w end. -Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *) Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w. -Proof. induction w; simpl; auto using f_equal. Qed. +Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed. Lemma wordToNat_cast_word {n} (w:word n) m pf : wordToNat (@cast_word n m pf w) = wordToNat w. @@ -721,4 +758,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _. Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)), @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO). Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a. -Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file +Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b. |