diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-23 14:52:05 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-23 14:52:05 -0400 |
commit | bbd4cc11aa335eb4e831c75755effca8c5782e40 (patch) | |
tree | 85a2da8176244035477a4088488e69b1415f8036 /src/Util | |
parent | 108f003608e841612216774ee76bc715e6bbd6c8 (diff) |
Fill in some word util admitted lemmas
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/WordUtil.v | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index f2ceb047f..f73d9fccc 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -137,10 +137,25 @@ Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) : Admitted. Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a). -Admitted. +Proof. + intro a; induction a. + { reflexivity. } + { simpl; intros; rewrite IHa; clear IHa. + rewrite (shatter_word w); simpl. + change (2^a + (2^a + 0)) with (2 * 2^a). + rewrite (mul_comm 2 (2^a)). + assert (2^a <> 0) by auto with arith. + destruct (whd w); try rewrite S_mod; try rewrite mul_mod_distr_r; omega. } +Qed. Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a). -Admitted. +Proof. + unfold wfirstn. + intros; rewrite wordToNat_split1. + match goal with |- appcontext[match ?x with _ => _ end] => generalize x end. + intro H'; destruct H'. + reflexivity. +Qed. Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y. Proof. |