diff options
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 1a7b3316e..49b1875ce 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -32,7 +32,7 @@ Section PseudoMersenneBaseParamProofs. unfold value in *. congruence. Qed. - + 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 -> @@ -45,7 +45,7 @@ Section PseudoMersenneBaseParamProofs. case_eq i; intros; subst. + subst; apply nth_error_first in nth_err_w. apply nth_error_first in nth_err_b; subst. - apply map_nth_error. + apply map_nth_error. case_eq l; intros; subst; [simpl in *; omega | ]. unfold base_from_limb_widths; fold base_from_limb_widths. reflexivity. @@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs. apply nth_error_first in H. subst; eauto. Qed. - + Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> sum_firstn l (S i) = x + sum_firstn l i. @@ -89,6 +89,13 @@ Section PseudoMersenneBaseParamProofs. - rewrite IHl by auto; ring. Qed. + Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. + Proof. + intros. + apply Z.lt_le_incl. + auto using limb_widths_pos. + Qed. + Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. Proof. unfold sum_firstn; intros. @@ -110,7 +117,7 @@ Section PseudoMersenneBaseParamProofs. induction i; intros. + unfold base, 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. specialize (IHi lt_i_length). rewrite base_length in lt_i_length. @@ -131,7 +138,7 @@ Section PseudoMersenneBaseParamProofs. apply limb_widths_nonneg. 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). Proof. @@ -171,7 +178,7 @@ Section PseudoMersenneBaseParamProofs. + rewrite base_length in *; apply limb_widths_match_modulus; assumption. Qed. - Lemma base_succ : forall i, ((S i) < length base)%nat -> + 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. @@ -219,7 +226,7 @@ Section PseudoMersenneBaseParamProofs. Proof. unfold base; case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity]. Qed. - + Lemma base_good : forall i j : nat, (i + j < length base)%nat -> let b := nth_default 0 base in |