Clean up some montgomery wbw instantiation, make display

3 files changed, 7 insertions, 32 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
index 60a3e59fc..266fc1f6f 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v
@@ -53,7 +53,7 @@ Section WordByWordMontgomery.
     {small_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> small (conditional_sub v)}
     {sub_then_maybe_add : T R_numlimbs -> T R_numlimbs -> T R_numlimbs} (* computes [a - b + if (a - b) <? 0 then N else 0] *)
     {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 <? 0 then eval N else 0}
-    {small_sub_then_maybe_add : forall a b, small a -> small b -> 0 <= eval a < eval N -> 0 <= eval b < eval N -> small (sub_then_maybe_add a b)}
+    {small_sub_then_maybe_add : forall a b, small (sub_then_maybe_add a b)}
     (B : T R_numlimbs)
     (B_bounds : 0 <= eval B < R)
     (small_B : small B)
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
index 33a0ea535..1560b702e 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -26,7 +26,6 @@ Section WordByWordMontgomery.
   Local Notation addT := (fun n => @Saturated.add (Z.pos r) n n n).
   Local Notation conditional_sub_cps := (fun V => @conditional_sub_cps (Z.pos r) _ (Z.pos r - 1) V N _).
   Local Notation conditional_sub := (fun V => @conditional_sub (Z.pos r) _ (Z.pos r - 1) V N).
-
   Local Notation sub_then_maybe_add_cps :=
     (fun V1 V2 => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N).
   Local Notation sub_then_maybe_add := (fun V1 V2 => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) V1 V2 N).
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index 6e6b19f3f..837a709b7 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -233,34 +233,10 @@ Section WordByWordMontgomery.
        (fun p q => @sub_then_maybe_add_cps (Z.pos r) R_numlimbs (Z.pos r - 1) p q N).
     Local Notation sub_then_maybe_add :=
       (fun p q => @sub_then_maybe_add (Z.pos r) R_numlimbs (Z.pos r - 1) p q N).
-
-
-    Local Lemma eval_sub_then_maybe_add : forall a b : T R_numlimbs,
-        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 <? 0 then eval N else 0).
-    Proof.
-      intros; cbv beta; apply eval_sub_then_maybe_add; try assumption; nia.
-    Qed.
-      
-    Local Lemma small_sub_then_maybe_add : forall a b : T R_numlimbs,
-        small a ->
-        small b ->
-        0 <= eval a < eval N ->
-        0 <= eval b < eval N ->
-        small (sub_then_maybe_add a b).
-    Proof.
-      intros; cbv beta; apply small_sub_then_maybe_add; try assumption; nia.
-    Qed.
-    Local Lemma sub_then_maybe_add_cps_id : forall (Av Bv : T R_numlimbs) cpsT (f : _ -> cpsT), sub_then_maybe_add_cps Av Bv _ f = f (sub_then_maybe_add Av Bv).
-    Proof.
-      intros; cbv beta; apply sub_then_maybe_add_id; try assumption; nia.
-    Qed.
-    Hint Rewrite sub_then_maybe_add_cps_id : uncps.
+    Local Notation eval_sub_then_maybe_add :=
+      (fun p q smp smq => @eval_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N smp smq small_N N_mask).
+    Local Notation small_sub_then_maybe_add :=
+      (fun p q => @small_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N).
 
     Definition add_no_cps_bound : 0 <= eval add_no_cps < eval N
       := @add_bound T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
@@ -272,9 +248,9 @@ Section WordByWordMontgomery.
     Definition small_add_no_cps : small add_no_cps
       := @small_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@small_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.
     Definition small_sub_no_cps : small sub_no_cps
-      := @small_sub T (@eval) R_numlimbs (@small) N (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av Bv small_Av small_Bv Av_bound Bv_bound.
+      := @small_sub T R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av Bv.
     Definition small_opp_no_cps : small opp_no_cps
-      := @small_opp T (@eval) (@zero) r R R_numlimbs (@small) (@eval_zero) (@small_zero) N (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av small_Av Av_bound.
+      := @small_opp T (@zero) R_numlimbs (@small) (@sub_then_maybe_add) (@small_sub_then_maybe_add) Av.
 
     Definition eval_add_no_cps : eval add_no_cps = eval Av + eval Bv + (if eval N <=? eval Av + eval Bv then - eval N else 0)
       := @eval_add T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound.