aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar jadep <jadep@mit.edu>2019-03-12 15:56:17 -0400
committerGravatar jadephilipoom <jade.philipoom@gmail.com>2019-03-25 06:13:45 -0400
commit44d7932acb4eb48e0c75497747c5e3bd203afc3d (patch)
tree1a0f29d941abc68c6ff8d9fa2f9f807267629576 /src
parentd71fe6f9e283ba7b297da63fa5240c9117acd570 (diff)
remove 2: syntax so I don't break 8.7
Diffstat (limited to 'src')
-rw-r--r--src/Arithmetic.v27
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.