Define carry_opp in terms of carry_sub

2 files changed, 8 insertions, 17 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.