From a58a68cf5bb4d634683b091a8e35b5829a2e90bd Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 16 Sep 2018 19:27:27 -0400 Subject: prove admit --- src/Experiments/NewPipeline/Arithmetic.v | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index ba023a1d3..eb04c4c4d 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -3208,7 +3208,7 @@ Module WordByWordMontgomery. clear - r_big lgr_big; autounfold with loc; intros. repeat match goal with H : ?x = partition _ _ _ |- _ => rewrite H; clear H end. - rewrite (surjective_pairing (Rows.add _ _ _ _)). + rewrite (surjective_pairing (Rows.add _ _ _ _)). cbn [fst snd]. rewrite Rows.add_partitions, Rows.add_div by (auto; distr_length). autorewrite with push_eval. rewrite <-Z.div_mod'', partition_step by auto. @@ -3244,16 +3244,15 @@ Module WordByWordMontgomery. Qed. Lemma small_drop_high_addT' : forall n a b, small a -> small b -> small (@drop_high_addT' n a b). Proof using lgr_big. - intros n a b Ha Hb; generalize (length_small Ha); generalize (length_small Hb); generalize (@eval_drop_high_addT' n a b Ha). - clear -lgr_big Ha Hb. - cbv [small]. - intro Heq; rewrite Heq; autounfold with loc in *. - rewrite Ha, Hb. - repeat t_step. - rewrite !UniformWeight.uweight_eq_alt by omega. - autorewrite with push_Zof_nat zsimplify_fast. - rewrite Z.pow_succ_r by omega. - Admitted. + pose proof r_big as r_big. + clear - r_big lgr_big; autounfold with loc; intros. + repeat match goal with H : ?x = partition _ _ _ |- _ => + rewrite H; clear H end. + rewrite (surjective_pairing (Rows.add _ _ _ _)). cbn [fst snd]. + rewrite Rows.add_partitions by (distr_length; auto using length_partition). + autorewrite with push_eval. + auto using partition_eq_mod with zarith. + Qed. Local Axiom eval_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_sub v N) = eval v + if eval N <=? eval v then -eval N else 0. Local Axiom small_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_sub v N). Local Axiom eval_sub_then_maybe_add : forall a b, small a -> small b -> 0 <= eval a < eval N -> 0 <= eval b < eval N -> eval (sub_then_maybe_add a b) = eval a - eval b + if eval a - eval b