diff options
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 22 | ||||
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 16 |
2 files changed, 19 insertions, 19 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index ed9b58ccc..a7d7da800 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -158,10 +158,10 @@ Section BitwiseDecodeEncode. Local Hint Resolve limb_widths_nonneg. Local Notation "w[ i ]" := (nth_default 0 limb_widths i). Local Notation base := (base_from_limb_widths limb_widths). - Local Notation max := (upper_bound limb_widths). + Local Notation upper_bound := (upper_bound limb_widths). Lemma encode'_spec : forall x i, (i <= length base)%nat -> - encode' limb_widths x i = BaseSystem.encode' base x max i. + encode' limb_widths x i = BaseSystem.encode' base x upper_bound i. Proof. induction i; intros. + rewrite encode'_zero. reflexivity. @@ -173,7 +173,7 @@ Section BitwiseDecodeEncode. - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity. - repeat f_equal; try solve [rewrite nth_default_base by (omega || auto); reflexivity]. rewrite nth_default_out_of_bounds by omega. - unfold upper_bound. + unfold Pow2Base.upper_bound. rewrite <-base_from_limb_widths_length by auto. congruence. Qed. @@ -183,7 +183,7 @@ Section BitwiseDecodeEncode. intros; apply nth_default_preserves_properties; auto; omega. Qed. Hint Resolve nth_default_limb_widths_nonneg. - Lemma base_upper_bound_compatible : @base_max_succ_divide base max. + Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound. Proof. unfold base_max_succ_divide; intros i lt_Si_length. rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length; @@ -193,7 +193,7 @@ Section BitwiseDecodeEncode. rewrite Z.pow_add_r; auto using sum_firstn_limb_widths_nonneg. apply Z.divide_factor_r. + rewrite nth_default_out_of_bounds by omega. - unfold upper_bound. + unfold Pow2Base.upper_bound. replace (length limb_widths) with (S (pred (length limb_widths))) by (rewrite base_from_limb_widths_length in H by auto; omega). replace i with (pred (length limb_widths)) by @@ -206,12 +206,12 @@ Section BitwiseDecodeEncode. Hint Resolve base_upper_bound_compatible. Lemma encodeZ_spec : forall x, - BaseSystem.decode base (encodeZ limb_widths x) = x mod max. + BaseSystem.decode base (encodeZ limb_widths x) = x mod upper_bound. Proof. intros. assert (length base = length limb_widths) by auto using base_from_limb_widths_length. unfold encodeZ; rewrite encode'_spec by omega. - rewrite BaseSystemProofs.encode'_spec; unfold upper_bound; try zero_bounds; + rewrite BaseSystemProofs.encode'_spec; unfold Pow2Base.upper_bound; try zero_bounds; auto using sum_firstn_limb_widths_nonneg. rewrite nth_default_out_of_bounds by omega. reflexivity. @@ -344,14 +344,14 @@ End BitwiseDecodeEncode. Section Conversion. Context {limb_widthsA} (limb_widthsA_nonneg : forall w, In w limb_widthsA -> 0 <= w) {limb_widthsB} (limb_widthsB_nonneg : forall w, In w limb_widthsB -> 0 <= w). - Local Notation "{baseA}" := (base_from_limb_widths limb_widthsA). - Local Notation "{baseB}" := (base_from_limb_widths limb_widthsB). - Context (bvB : BaseSystem.BaseVector {baseB}). + Local Notation baseA := (base_from_limb_widths limb_widthsA). + Local Notation baseB := (base_from_limb_widths limb_widthsB). + Context (bvB : BaseSystem.BaseVector baseB). Definition convert xs := @encodeZ limb_widthsB (@decode_bitwise limb_widthsA xs). Lemma convert_spec : forall xs, @bounded limb_widthsA xs -> length xs = length limb_widthsA -> - BaseSystem.decode {baseA} xs mod (@upper_bound limb_widthsB) = BaseSystem.decode {baseB} (convert xs). + BaseSystem.decode baseA xs mod (@upper_bound limb_widthsB) = BaseSystem.decode baseB (convert xs). Proof. unfold convert; intros. rewrite encodeZ_spec, decode_bitwise_spec by auto. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index e0a194c3b..50ef9df00 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -11,7 +11,7 @@ Local Open Scope Z_scope. Section PseudoMersenneBaseParamProofs. Context `{prm : PseudoMersenneBaseParams}. - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof. @@ -29,9 +29,9 @@ Section PseudoMersenneBaseParamProofs. (i < length limb_widths)%nat -> (j < length limb_widths)%nat -> (i+j >= length limb_widths)%nat-> - let b := nth_default 0 {base} in - let r := (b i * b j) / (2^k * b (i+j-length {base})%nat) in - b i * b j = r * (2^k * b (i+j-length {base})%nat). + let b := nth_default 0 base in + let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in + b i * b j = r * (2^k * b (i+j-length base)%nat). Proof. intros. rewrite (Z.mul_comm r). @@ -53,8 +53,8 @@ Section PseudoMersenneBaseParamProofs. Qed. Lemma base_good : forall i j : nat, - (i + j < length {base})%nat -> - let b := nth_default 0 {base} in + (i + j < length base)%nat -> + let b := nth_default 0 base in let r := b i * b j / b (i + j)%nat in b i * b j = r * b (i + j)%nat. Proof. @@ -70,12 +70,12 @@ Section PseudoMersenneBaseParamProofs. rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg. Qed. - Lemma base_length : length {base} = length limb_widths. + Lemma base_length : length base = length limb_widths. Proof. auto using base_from_limb_widths_length. Qed. - Global Instance bv : BaseSystem.BaseVector {base} := { + Global Instance bv : BaseSystem.BaseVector base := { base_positive := base_positive limb_widths_nonneg; b0_1 := fun x => b0_1 x limb_widths_nonnil; base_good := base_good |