diff options
author | jadep <jadep@mit.edu> | 2019-03-07 15:18:42 -0500 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-03-25 06:13:45 -0400 |
commit | 3e4edb9a9b8cc15bdc02b9005e0b94561645b77b (patch) | |
tree | 765489dd5ce02b3baf141190b1f52e3eb2ffb1fb /src/Arithmetic | |
parent | bbabd295594448f12161075c5d19dd369ed04a53 (diff) |
Get new Barrett proofs to generate Fancy code as before
Diffstat (limited to 'src/Arithmetic')
-rw-r--r-- | src/Arithmetic/BarrettReduction/Generalized.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v index c2885bc77..93aa9452f 100644 --- a/src/Arithmetic/BarrettReduction/Generalized.v +++ b/src/Arithmetic/BarrettReduction/Generalized.v @@ -218,6 +218,15 @@ Section barrett. autorewrite with push_Zmul zsimplify zstrip_div. auto with lia. Qed. + + Theorem barrett_reduction_small_strong + : a mod n = if r <? n then r else r-n. + Proof using a a_good a_nonneg a_small b base_good epsilon k k_big_enough k_good m m_good n n_good n_large n_pos n_reasonable offset offset_nonneg q r. + pose proof r_small_strong. pose proof qn_small. + destruct (r <? n) eqn:Hr; try rewrite Hr; Z.ltb_to_lt; try lia. + { symmetry; apply (Zmod_unique a n q); subst r; lia. } + { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. } + Qed. End StrongerBounds. End barrett_algorithm. End barrett. |