From 44d7932acb4eb48e0c75497747c5e3bd203afc3d Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 15:56:17 -0400 Subject: remove 2: syntax so I don't break 8.7 --- src/Arithmetic.v | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'src') 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. -- cgit v1.2.3