diff options
Diffstat (limited to 'src/Assembly/WordizeUtil.v')
-rw-r--r-- | src/Assembly/WordizeUtil.v | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v index d0b563368..d4a9409e2 100644 --- a/src/Assembly/WordizeUtil.v +++ b/src/Assembly/WordizeUtil.v @@ -806,6 +806,57 @@ Section TopLevel. apply wordize_plus; assumption. Qed. + Lemma wordize_sub: forall {n} (x y: word n) low0 high0 low1 high1, + (low0 <= wordToN x)%N -> (wordToN x <= high0)%N + -> (low1 <= wordToN y)%N -> (wordToN y <= high1)%N + -> (&x >= &y)%N -> (& (x ^- y) <= high0 - low1)%N. + Proof. + intros. + + destruct (Nge_dec 0%N (&y)). { + unfold wminus, wneg. + replace (& y) with 0%N in * by nomega. + replace low1 with 0%N by (symmetry; apply N.le_0_r; assumption). + replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N + by (rewrite wordToN_zero; nomega). + rewrite <- Npow2_ignore. + rewrite wplus_comm. + rewrite wplus_unit. + replace (high0 - 0)%N with high0 by nomega; assumption. + } + + assert (& x - & y < Npow2 n)%N. { + transitivity (wordToN x); + try apply word_size_bound; + apply N.sub_lt; + [apply N.ge_le|]; assumption. + } + + assert (& x - & y + & y < Npow2 n)%N. { + replace (& x - & y + & y)%N + with (wordToN x) by nomega; + apply word_size_bound. + } + + assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. { + apply NToWord_equal. + rewrite <- wordize_plus; rewrite wordToN_NToWord; try assumption. + nomega. + } + + rewrite Hv. + unfold wminus. + rewrite <- wplus_assoc. + rewrite wminus_inv. + rewrite wplus_comm. + rewrite wplus_unit. + rewrite wordToN_NToWord; try assumption. + + transitivity (high0 - & y)%N; + [apply N.sub_le_mono_r | apply N.sub_le_mono_l]; + assumption. + Qed. + Lemma wordize_mult: forall {n} (x y: word n), (&x * &y < Npow2 n)%N -> (&x * &y)%N = &(x ^* y). |