From 9c268bd4677af50677c2f9e9f57ae77cdb9454f9 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 18 Jul 2016 13:17:43 -0400 Subject: changed base notation --- src/ModularArithmetic/Pow2BaseProofs.v | 72 +++++++++++----------- .../PseudoMersenneBaseParamProofs.v | 16 ++--- 2 files changed, 44 insertions(+), 44 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 7538781c0..e06df9328 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -8,9 +8,9 @@ Local Open Scope Z_scope. Section Pow2BaseProofs. Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). - Lemma base_from_limb_widths_length : length {base} = length limb_widths. + Lemma base_from_limb_widths_length : length base = length limb_widths. Proof. induction limb_widths; try reflexivity. simpl; rewrite map_length. @@ -28,10 +28,10 @@ Section Pow2BaseProofs. eapply In_firstn; eauto. Qed. Hint Resolve sum_firstn_limb_widths_nonneg. - Lemma base_from_limb_widths_step : forall i b w, (S i < length {base})%nat -> - nth_error {base} i = Some b -> + Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat -> + nth_error base i = Some b -> nth_error limb_widths i = Some w -> - nth_error {base} (S i) = Some (two_p w * b). + nth_error base (S i) = Some (two_p w * b). Proof. induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b; unfold base_from_limb_widths in *; fold base_from_limb_widths in *; @@ -54,13 +54,13 @@ Section Pow2BaseProofs. Qed. - Lemma nth_error_base : forall i, (i < length {base})%nat -> - nth_error {base} i = Some (two_p (sum_firstn limb_widths i)). + Lemma nth_error_base : forall i, (i < length base)%nat -> + nth_error base i = Some (two_p (sum_firstn limb_widths i)). Proof. induction i; intros. + unfold sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity. intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega. - + assert (i < length {base})%nat as lt_i_length by omega. + + assert (i < length base)%nat as lt_i_length by omega. specialize (IHi lt_i_length). rewrite base_from_limb_widths_length in lt_i_length. destruct (nth_error_length_exists_value _ _ lt_i_length) as [w nth_err_w]. @@ -80,8 +80,8 @@ Section Pow2BaseProofs. eapply nth_error_value_In; eauto. Qed. - Lemma nth_default_base : forall d i, (i < length {base})%nat -> - nth_default d {base} i = 2 ^ (sum_firstn limb_widths i). + Lemma nth_default_base : forall d i, (i < length base)%nat -> + nth_default d base i = 2 ^ (sum_firstn limb_widths i). Proof. intros ? ? i_lt_length. destruct (nth_error_length_exists_value _ _ i_lt_length) as [x nth_err_x]. @@ -92,8 +92,8 @@ Section Pow2BaseProofs. congruence. Qed. - Lemma base_succ : forall i, ((S i) < length {base})%nat -> - nth_default 0 {base} (S i) mod nth_default 0 {base} i = 0. + Lemma base_succ : forall i, ((S i) < length base)%nat -> + nth_default 0 base (S i) mod nth_default 0 base i = 0. Proof. intros. repeat rewrite nth_default_base by omega. @@ -105,7 +105,7 @@ Section Pow2BaseProofs. apply limb_widths_nonneg. rewrite lw_eq. apply in_eq. - + assert (i < length {base})%nat as i_lt_length by omega. + + assert (i < length base)%nat as i_lt_length by omega. rewrite base_from_limb_widths_length in *. apply nth_error_length_exists_value in i_lt_length. destruct i_lt_length as [x nth_err_x]. @@ -115,7 +115,7 @@ Section Pow2BaseProofs. omega. Qed. - Lemma nth_error_subst : forall i b, nth_error {base} i = Some b -> + Lemma nth_error_subst : forall i b, nth_error base i = Some b -> b = 2 ^ (sum_firstn limb_widths i). Proof. intros i b nth_err_b. @@ -125,7 +125,7 @@ Section Pow2BaseProofs. congruence. Qed. - Lemma base_positive : forall b : Z, In b {base} -> b > 0. + Lemma base_positive : forall b : Z, In b base -> b > 0. Proof. intros b In_b_base. apply In_nth_error_value in In_b_base. @@ -136,7 +136,7 @@ Section Pow2BaseProofs. apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg. Qed. - Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x {base} 0 = 1. + Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x base 0 = 1. Proof. case_eq limb_widths; intros; [congruence | reflexivity]. Qed. @@ -154,23 +154,23 @@ Section BitwiseDecodeEncode. (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). 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 base := (base_from_limb_widths 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. + Lemma encode'_spec : forall x i, (i <= length base)%nat -> + encode' limb_widths x i = BaseSystem.encode' base x upper_bound i. Proof. induction i; intros. + rewrite encode'_zero. reflexivity. + rewrite encode'_succ, <-IHi by omega. simpl; do 2 f_equal. rewrite Z.land_ones, Z.shiftr_div_pow2 by auto using sum_firstn_limb_widths_nonneg. - match goal with H : (S _ <= length {base})%nat |- _ => + match goal with H : (S _ <= length base)%nat |- _ => apply le_lt_or_eq in H; destruct H end. - 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. @@ -180,7 +180,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; @@ -190,7 +190,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 @@ -203,12 +203,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. + 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. @@ -316,7 +316,7 @@ Section BitwiseDecodeEncode. Lemma decode_bitwise'_spec : forall us i, (i <= length limb_widths)%nat -> bounded limb_widths us -> length us = length limb_widths -> decode_bitwise' limb_widths us i (partial_decode us i (length us - i)) = - BaseSystem.decode {base} us. + BaseSystem.decode base us. Proof. induction i; intros. + rewrite partial_decode_intermediate by auto. @@ -328,7 +328,7 @@ Section BitwiseDecodeEncode. Lemma decode_bitwise_spec : forall us, bounded limb_widths us -> length us = length limb_widths -> - decode_bitwise limb_widths us = BaseSystem.decode {base} us. + decode_bitwise limb_widths us = BaseSystem.decode base us. Proof. unfold decode_bitwise; intros. replace 0 with (partial_decode us (length us) (length us - length us)) by @@ -341,14 +341,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. @@ -361,7 +361,7 @@ Section UniformBase. Context {width : Z} (limb_width_pos : 0 < width). Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil) (limb_widths_uniform : forall w, In w limb_widths -> w = width). - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat -> (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)). @@ -409,7 +409,7 @@ Section UniformBase. Qed. Lemma decode_tl_base_shift : forall us, (length us < length limb_widths)%nat -> - BaseSystem.decode (tl {base}) us = BaseSystem.decode {base} us << width. + BaseSystem.decode (tl base) us = BaseSystem.decode base us << width. Proof. intros ? Hlength. edestruct (destruct_repeat limb_widths) as [? | [tl_lw [Heq_lw tl_lw_uniform]]]; @@ -422,7 +422,7 @@ Section UniformBase. Qed. Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat -> - BaseSystem.decode {base} (u0 :: us) = u0 + ((BaseSystem.decode {base} us) << width). + BaseSystem.decode base (u0 :: us) = u0 + ((BaseSystem.decode base us) << width). Proof. intros. rewrite <-decode_tl_base_shift by (simpl in *; omega). 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 -- cgit v1.2.3