diff options
Diffstat (limited to 'src/ModularArithmetic/Pow2BaseProofs.v')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index d95de5bd1..78c6bba0f 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -230,10 +230,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. @@ -245,7 +245,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. @@ -255,7 +255,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; @@ -265,7 +265,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 @@ -278,12 +278,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. @@ -416,14 +416,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. |