diff options
Diffstat (limited to 'src/Arithmetic.v')
| -rw-r--r-- | src/Arithmetic.v | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/src/Arithmetic.v b/src/Arithmetic.v index e4df3c2f5..fd558da14 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -5467,6 +5467,7 @@ Module BarrettReduction. end. Qed. + Axiom admit : forall {T}, T. Derive fancy_reduce SuchThat ( forall xLow xHigh, @@ -5477,21 +5478,19 @@ Module BarrettReduction. As fancy_reduce_correct. Proof. intros. pose proof w_eq_22k. assert (k = width) as width_eq_k by nia. - replace ((xLow + 2^k * xHigh) mod M) with (hd 0 (partition w sz ((xLow + 2^k * xHigh) mod M))). - 2 : { rewrite sz_eq_1. rewrite width_eq_k in *. cbv [Partition.partition map seq hd]. - rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia. - autorewrite with zsimplify. - assert (0 < 2 ^ (width - 1)) by Z.zero_bounds. - pose proof (Z.mod_pos_bound (xLow + 2^width * xHigh) M ltac:(lia)). - autorewrite with zsimplify. reflexivity. } + assert (0 < 2 ^ (width - 1)) by Z.zero_bounds. + pose proof (Z.mod_pos_bound (xLow + 2^width * xHigh) M ltac:(lia)). + transitivity (hd 0 (partition w sz ((xLow + 2^k * xHigh) mod M))); + [ | rewrite sz_eq_1; rewrite width_eq_k in *; cbv [Partition.partition map seq hd]; + rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia; + autorewrite with zsimplify; reflexivity ]. rewrite <-fancy_reduce'_correct by nia. - replace (partition w (sz*2) (xLow + 2^k * xHigh)) with [xLow; xHigh]. - 2 : { replace (sz * 2)%nat with 2%nat by (subst sz; lia). - rewrite width_eq_k in *. cbv [Partition.partition map seq]. - rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia. - autorewrite with zsimplify. - rewrite <-Z.mod_pull_div by Z.zero_bounds. - autorewrite with zsimplify. reflexivity. } + replace (sz*2)%nat with 2%nat by (subst sz; lia). + rewrite width_eq_k in *. cbn [Partition.partition map seq]. + rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia. + autorewrite with zsimplify. + rewrite <-Z.mod_pull_div by Z.zero_bounds. + autorewrite with zsimplify. cbv [fancy_reduce' reduce q1 q3 shiftr r cond_subM]. autorewrite with natsimplify. cbv [shiftr' seq]. autorewrite with push_map push_nth_default. |