Define carry_opp in terms of carry_sub

3 files changed, 12 insertions, 21 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index ff2c23ab8..5c0d143c2 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -74,7 +74,7 @@ Section ModularBaseSystem.
   Definition carry_opp (carry_chain : list nat) (modulus_multiple : digits)
              (modulus_multiple_correct : decode modulus_multiple = 0%F)
              (x : digits) : digits :=
-    carry_ carry_chain (opp modulus_multiple modulus_multiple_correct x).
+    carry_sub carry_chain modulus_multiple modulus_multiple_correct zero x.
 
   Definition rep (us : digits) (x : F modulus) := decode us = x.
   Local Notation "u ~= x" := (rep u x).
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index f1b8c601b..ff1dd87dd 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -533,29 +533,20 @@ Section Subtraction.
     : opp_opt us = opp coeff coeff_mod us
     := proj2_sig (opp_opt_sig us).
 
-  Definition carry_opp_opt_sig {T} (f:digits -> T)
-    (us : digits) : { x | x = f (carry_opp carry_chain coeff coeff_mod us) }.
+  Definition carry_opp_opt_sig (us : digits) : { b : digits | b = carry_opp carry_chain coeff coeff_mod us }.
   Proof.
     eexists.
     cbv [carry_opp].
-    rewrite <-carry__opt_cps_correct, <-opp_opt_correct.
-    cbv [carry_sequence_opt_cps carry__opt_cps opp_opt opp sub_opt].
-    rewrite to_list_from_list.
+    rewrite <-carry_sub_opt_correct.
     reflexivity.
   Defined.
 
-  Definition carry_opp_opt_cps {T} (f:digits -> T) (us : digits) : T
-    := Eval cbv [proj1_sig carry_opp_opt_sig] in proj1_sig (carry_opp_opt_sig f us).
-
-  Definition carry_opp_opt_cps_correct {T} (f:digits -> T) (us : digits)
-    : carry_opp_opt_cps f us = f (carry_opp carry_chain coeff coeff_mod us)
-    := proj2_sig (carry_opp_opt_sig f us).
-
-  Definition carry_opp_opt := carry_opp_opt_cps id.
+  Definition carry_opp_opt (us : digits) : digits
+    := Eval cbv [proj1_sig carry_opp_opt_sig] in proj1_sig (carry_opp_opt_sig us).
 
-  Definition carry_opp_opt_correct (us : digits)
-    : carry_opp_opt us = carry_opp carry_chain coeff coeff_mod us :=
-    carry_opp_opt_cps_correct id us.
+  Definition carry_opp_opt_correct us
+    : carry_opp_opt us = carry_opp carry_chain coeff coeff_mod us
+    := proj2_sig (carry_opp_opt_sig us).
 
 End Subtraction.
 
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index faf8b0519..b2f768469 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -325,10 +325,10 @@ Definition carry_opp_sig (f : fe25519) :
   { g : fe25519 | g = carry_opp_opt f }.
 Proof.
   eexists.
-  rewrite <-(@app_10_correct fe25519).
-  cbv.
-  autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. (* FIXME: The speed of this rewrite depends on the fact that we have 10 limbs; there are some lemmas in [zsimplify_Z_to_pos] which are specific to 10. *)
-  autorewrite with zsimplify_Z_to_pos; cbv.
+  cbv [carry_opp_opt].
+  rewrite <-carry_sub_correct.
+  rewrite zero_subst.
+  cbv [carry_sub].
   reflexivity.
 Defined.