unstuck carry_mul_opt_cps using from_list_default

2 files changed, 8 insertions, 15 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index be7f2f257..40ad3f3ec 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -13,17 +13,10 @@ Section s.
 
   Definition fe := tuple Z (length PseudoMersenneBaseParamProofs.base).
 
-  About from_list.
+  Definition mul {k_ c_} (pfk : k = k_) (pfc:c = c_) (x y:fe) : fe :=
+    carry_mul_opt_cps k_ c_ (fun xs : digits => from_list_default 0%Z (length base) xs)
+      (to_list _ x) (to_list _ y).
 
-  Lemma carry_mul_on_tuple x y :
-    length (carry_mul (to_list (length base) x) (to_list (length base) y)) = length base.
-  Admitted.
-
-  Definition mul {k_ c_} (pfk : k = k_) (pfc:c = c_) (x y:fe) : fe.
-    refine (carry_mul_opt_cps (fun xs => from_list _ xs) (to_list _ x) (to_list _ y) _).
-    abstract (apply carry_mul_on_tuple).
-  Defined.
-  
   Definition add : fe -> fe -> fe.
     refine (on_tuple2 add_opt _).
     abstract (intros; rewrite add_opt_correct, add_length_exact; case_max; omega).
@@ -33,4 +26,5 @@ Section s.
     refine (on_tuple2 sub_opt _).
     abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
   Defined.
+
 End s.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index e11186cfb..3d7168c5a 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -486,21 +486,20 @@ Section Multiplication.
     : mul_opt us vs = mul us vs
     := proj2_sig (mul_opt_sig us vs).
 
-  Definition carry_mul_opt_sig {T:digits->Type} (f:forall d:digits, T d) (us vs : digits) : { x | x = f (carry_mul us vs) }.
+  Definition carry_mul_opt_sig {T} (f:digits -> T)
+    (us vs : digits) : { x | x = f (carry_mul us vs) }.
   Proof.
     eexists.
     cbv [carry_mul].
-    (* FIXME
     erewrite <-carry_full_opt_cps_correct by eauto.
     erewrite <-mul_opt_correct.
     reflexivity.
-   *)
   Defined.
 
-  Definition carry_mul_opt_cps {T} (f:forall d:digits, T d) (us vs : digits) : T (carry_mul us vs)
+  Definition carry_mul_opt_cps {T} (f:digits -> T) (us vs : digits) : T
     := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig f us vs).
 
-  Definition carry_mul_opt_cps_correct {T} (f:forall d:digits, T d) (us vs : digits)
+  Definition carry_mul_opt_cps_correct {T} (f:digits -> T) (us vs : digits)
     : carry_mul_opt_cps f us vs = f (carry_mul us vs)
     := proj2_sig (carry_mul_opt_sig f us vs).
 End Multiplication.