From 7da2e219c6c1eb6288f10a7da756d51140f8da60 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2017 20:34:01 -0400 Subject: Fix ZToWord, add wring_eq_ext, speed up some proofs --- Bedrock/Word.v | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'Bedrock') diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 016903a7f..09bfc036b 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -818,9 +818,12 @@ Theorem wmult_plus_distr : forall sz (x y z : word sz), (x ^+ y) ^* z = (x ^* z) rewrite (mult_comm (wordToNat x + wordToNat y)). rewrite <- (mult_assoc (wordToNat z)). auto with arith. - generalize dependent (wordToNat x * wordToNat z). - generalize dependent (wordToNat y * wordToNat z). - intros. + generalize dependent (pow2 sz); intros. + repeat match goal with + | [ |- context[natToWord ?sz (?f ?x ?y)] ] => generalize dependent (f x y); intros + | [ H : context[natToWord ?sz (?f ?x ?y)] |- _ ] => generalize dependent (f x y); intros + | [ H : wordToNat (natToWord _ _) = _ |- _ ] => clear H + end. omega. Qed. @@ -859,6 +862,7 @@ Theorem wminus_inv : forall sz (x : word sz), x ^+ ^~ x = wzero sz. rewrite drop_sub; auto with arith. apply natToWord_pow2. generalize (wordToNat_bound x). + match goal with Heq : wordToNat (natToWord _ _) = _ |- _ => clear Heq end. omega. Qed. @@ -868,6 +872,11 @@ Definition wring (sz : nat) : ring_theory (wzero sz) (wone sz) (@wplus sz) (@wmu (@wmult_unit _) (@wmult_comm _) (@wmult_assoc _) (@wmult_plus_distr _) (@wminus_def _) (@wminus_inv _). +Lemma wring_eq_ext (sz : nat) : ring_eq_ext (@wplus sz) (@wmult sz) (@wneg sz) (@eq _). +Proof. + constructor; repeat intro; subst; reflexivity. +Qed. + Theorem weqb_sound : forall sz (x y : word sz), weqb x y = true -> x = y. Proof. eapply weqb_true_iff. @@ -1017,10 +1026,10 @@ Definition wordToZ sz (w : word sz) : Z := Definition ZToWord sz (v : Z) : word sz := if (v