From d792677e84a79021d75162a840377dd45efb796c Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sun, 20 Mar 2016 17:09:44 -0400 Subject: made BaseVector instance global --- src/ModularArithmetic/ExtendedBaseVector.v | 1 - src/ModularArithmetic/ModularBaseSystem.v | 1 - src/ModularArithmetic/ModularBaseSystemProofs.v | 2 -- src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 2 +- src/ModularArithmetic/PseudoMersenneBaseParams.v | 4 ++-- 5 files changed, 3 insertions(+), 7 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 746791d8d..2e65df9bd 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -9,7 +9,6 @@ Local Open Scope Z_scope. Section ExtendedBaseVector. Context `{prm : PseudoMersenneBaseParams}. - Existing Instance bv. (* This section defines a new BaseVector that has double the length of the BaseVector * used to construct [params]. The coefficients of the new vector are as follows: diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index d121e9d5c..2bfcdcf0b 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -7,7 +7,6 @@ Local Open Scope Z_scope. Section PseudoMersenneBase. Context `{prm :PseudoMersenneBaseParams}. - Existing Instance bv. Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 524c2da27..7efccbade 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -9,7 +9,6 @@ Local Open Scope Z_scope. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. - Existing Instance bv. Local Hint Unfold decode. Local Notation "u '~=' x" := (rep u x) (at level 70). @@ -251,7 +250,6 @@ End PseudoMersenneProofs. Section CarryProofs. Context `{prm : PseudoMersenneBaseParams}. - Existing Instance bv. Local Notation "u '~=' x" := (rep u x) (at level 70). Hint Unfold log_cap. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 847b8e85f..93e6bc1f0 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -268,7 +268,7 @@ Section PseudoMersenneBaseParamProofs. rewrite <- base_length; assumption. Qed. - Instance bv : BaseSystem.BaseVector base := { + Global Instance bv : BaseSystem.BaseVector base := { base_positive := base_positive; b0_1 := b0_1; base_good := base_good diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v index 122cac0ab..09f4bc68e 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParams.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v @@ -14,6 +14,7 @@ Class PseudoMersenneBaseParams (modulus : Z) := { sum_firstn limb_widths i + sum_firstn limb_widths j; k : Z; c : Z; + k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k; modulus_pseudomersenne : modulus = 2^k - c; prime_modulus : Znumtheory.prime modulus; limb_widths_match_modulus : forall i j, @@ -21,6 +22,5 @@ Class PseudoMersenneBaseParams (modulus : Z) := { (j < length limb_widths)%nat -> (i + j >= length limb_widths)%nat -> let w_sum := sum_firstn limb_widths in - k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j; - k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k + k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j }. -- cgit v1.2.3