diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
commit | 0ae5f6871b29d20f48b5df6dab663b5a44162d01 (patch) | |
tree | 33b11090af2555a91a593f9b919edf83c71557cd /src/ModularArithmetic/ExtendedBaseVector.v | |
parent | a0bdb14300aa57eed684992a23a57fd319ef97c0 (diff) |
remove trailing whitespace from src/
Diffstat (limited to 'src/ModularArithmetic/ExtendedBaseVector.v')
-rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 2e65df9bd..9ed7d065e 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -22,19 +22,19 @@ Section ExtendedBaseVector. * * (x \dot base) * (y \dot base) = (z \dot ext_base) * - * Then we can separate z into its first and second halves: + * Then we can separate z into its first and second halves: * * (z \dot ext_base) = (z1 \dot base) + (2 ^ k) * (z2 \dot base) * * Now, if we want to reduce the product modulo 2 ^ k - c: - * + * * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + (2 ^ k) * (z2 \dot base) mod (2^k-c) * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + c * (z2 \dot base) mod (2^k-c) * * This sum may be short enough to express using base; if not, we can reduce again. *) Definition ext_base := base ++ (map (Z.mul (2^k)) base). - + Lemma ext_base_positive : forall b, In b ext_base -> b > 0. Proof. unfold ext_base. intros b In_b_base. @@ -76,14 +76,14 @@ Section ExtendedBaseVector. intuition. Qed. - Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> + Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> nth_default 0 (map (Z.mul (2 ^ k)) base) n = (2 ^ k) * (nth_default 0 base n). Proof. intros. erewrite map_nth_default; auto. Qed. - + Lemma base_good_over_boundary : forall (i : nat) (l : (i < length base)%nat) |