From 2a14406a3d0ce41241471dbcb7cbd60fe2a66c59 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 16:44:57 -0700 Subject: ext_base: now defined in terms of ext_limb_widths --- src/ModularArithmetic/ExtendedBaseVector.v | 34 ++++++++++++++++++++----- src/ModularArithmetic/ModularBaseSystemOpt.v | 7 ++--- src/ModularArithmetic/ModularBaseSystemProofs.v | 4 +-- 3 files changed, 34 insertions(+), 11 deletions(-) diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index ddf787d21..0afd6b484 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -7,12 +7,13 @@ Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.BaseSystemProofs. Require Crypto.BaseSystem. Local Open Scope Z_scope. Section ExtendedBaseVector. Context `{prm : PseudoMersenneBaseParams}. - Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). (* 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: @@ -37,11 +38,19 @@ Section ExtendedBaseVector. * * This sum may be short enough to express using base; if not, we can reduce again. *) - Definition ext_base := base ++ (map (Z.mul (2^k)) base). + Definition ext_limb_widths := limb_widths ++ limb_widths. + Definition ext_base := base_from_limb_widths ext_limb_widths. + Lemma ext_base_alt : ext_base = base ++ (map (Z.mul (2^k)) base). + Proof. + unfold ext_base, ext_limb_widths. + rewrite base_from_limb_widths_app by auto using limb_widths_pos, Z.lt_le_incl. + rewrite two_p_equiv. + reflexivity. + Qed. Lemma ext_base_positive : forall b, In b ext_base -> b > 0. Proof. - unfold ext_base. intros b In_b_base. + rewrite ext_base_alt. intros b In_b_base. rewrite in_app_iff in In_b_base. destruct In_b_base as [In_b_base | In_b_extbase]. + eapply BaseSystem.base_positive. @@ -68,7 +77,7 @@ Section ExtendedBaseVector. Lemma b0_1 : forall x, nth_default x ext_base 0 = 1. Proof. - intros. unfold ext_base. + intros. rewrite ext_base_alt. rewrite nth_default_app. assert (0 < length base)%nat by (apply base_length_nonzero). destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega. @@ -120,7 +129,7 @@ Section ExtendedBaseVector. Proof. intros. subst b. subst r. - unfold ext_base in *. + rewrite ext_base_alt in *. rewrite app_length in H; rewrite map_length in H. repeat rewrite nth_default_app. repeat break_if; try omega. @@ -157,8 +166,21 @@ Section ExtendedBaseVector. Lemma extended_base_length: length ext_base = (length base + length base)%nat. Proof. - unfold ext_base; rewrite app_length; rewrite map_length; auto. + rewrite ext_base_alt, app_length, map_length; auto. + Qed. + + Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), + (length us <= length base)%nat + -> firstn (length us) base = firstn (length us) ext_base. + Proof. + rewrite ext_base_alt; intros. + rewrite firstn_app_inleft; auto; omega. Qed. + + Lemma decode_short : forall (us : BaseSystem.digits), + (length us <= length base)%nat -> + BaseSystem.decode base us = BaseSystem.decode ext_base us. + Proof. auto using decode_short_initial, firstn_us_base_ext_base. Qed. End ExtendedBaseVector. Hint Rewrite @extended_base_length : distr_length. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d7e6f1c65..696f10438 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -376,7 +376,7 @@ Section Multiplication. cbv [mul_bi'_step]. opt_step. { reflexivity. } - { cbv [crosscoef ext_base]. + { cbv [crosscoef]. change Z.div with Z_div_opt. change Z.mul with Z_mul_opt at 2. change @nth_default with @nth_default_opt. @@ -405,7 +405,7 @@ Section Multiplication. rewrite <- IHvsr; clear IHvsr. unfold mul_bi'_opt, mul_bi'_opt_step. apply f_equal2; [ | reflexivity ]. - cbv [crosscoef ext_base]. + cbv [crosscoef]. change Z.div with Z_div_opt. change Z.mul with Z_mul_opt at 2. change @nth_default with @nth_default_opt. @@ -477,7 +477,8 @@ Section Multiplication. Definition mul_opt_sig (us vs : digits) : { b : digits | b = mul us vs }. Proof. eexists. - cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. + cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros reduce]. + rewrite ext_base_alt. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. rewrite Z.map_shiftl by apply k_nonneg. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 227a3e77f..5d1becc00 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -132,7 +132,7 @@ Section PseudoMersenneProofs. (length us <= length base)%nat -> firstn (length us) base = firstn (length us) ext_base. Proof. - unfold ext_base; intros. + rewrite ext_base_alt; intros. rewrite firstn_app_inleft; auto; omega. Qed. Local Hint Immediate firstn_us_base_ext_base. @@ -184,7 +184,7 @@ Section PseudoMersenneProofs. Proof. intros. unfold BaseSystem.decode; rewrite <- mul_each_rep. - unfold ext_base. + rewrite ext_base_alt. replace (map (Z.mul (2 ^ k)) base) with (BaseSystem.mul_each (2 ^ k) base) by auto. rewrite base_mul_app. rewrite <- mul_each_rep; auto. -- cgit v1.2.3