diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 16:44:57 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 16:44:57 -0700 |
| commit | 2a14406a3d0ce41241471dbcb7cbd60fe2a66c59 (patch) | |
| tree | c67b2012a2afa95da8efb56a4611d9618f2d1e97 /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | 9b6a08343fd418296b069ead6fc4e879f8af0e7c (diff) | |
ext_base: now defined in terms of ext_limb_widths
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 7 |
1 files changed, 4 insertions, 3 deletions
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. |