diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-19 12:48:47 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2017-06-20 07:40:01 -0400 |
commit | e309733856b89e63a6e4f2165fc162f8bd483efd (patch) | |
tree | 0a05aa65d984df6651db6af84c23644bf86feb56 /src/Arithmetic/MontgomeryReduction/WordByWord | |
parent | f442684811ee0628afe5b427384be6c35a9bc675 (diff) |
Make use of new small_add
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/WordByWord')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 9a9ba8149..780a5de60 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -58,24 +58,18 @@ Section WordByWordMontgomery. subst R; destruct (Z.pos r ^ Z.of_nat R_numlimbs) eqn:?; [ | reflexivity | ]; lia. Qed. - - - (*****************************************************************************************) - (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *) Local Lemma small_add : forall n a b, small a -> small b -> small (@add n a b). Proof. - intros; apply Saturated.small_add; auto; try lia. - cbv [uweight]. - rewrite ?Znat.Nat2Z.inj_succ, ?Z.pow_succ_r by lia. - try nia. - Admitted. + intros; apply Saturated.small_add; auto; lia. + Qed. Local Lemma small_add' : forall n a b, small a -> small b -> small (@add' n a b). Proof. - intros; apply Saturated.small_add; auto; try lia. - (*cbv [uweight]. - rewrite !Znat.Nat2Z.inj_succ, !Z.pow_succ_r by lia. - try nia.*) - Admitted. + intros; apply Saturated.small_add; auto; lia. + Qed. + + + (*****************************************************************************************) + (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *) Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs). (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *) Local Notation conditional_subtract := conditional_subtract. |