From bbd4cc11aa335eb4e831c75755effca8c5782e40 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 23 Oct 2016 14:52:05 -0400 Subject: Fill in some word util admitted lemmas --- src/Util/WordUtil.v | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'src/Util/WordUtil.v') 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. -- cgit v1.2.3