diff options
-rw-r--r-- | src/BaseSystem.v | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 2 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 2 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParams.v | 4 |
6 files changed, 4 insertions, 7 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v index f3a1a0fdb..627550440 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -85,6 +85,7 @@ Section BaseSystem. End BaseSystem. +(* Example : polynomial base system *) Section PolynomialBaseCoefs. Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true). (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *) 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 }. |