Added reduce to karatsuba synthesis

2 files changed, 22 insertions, 11 deletions

diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v
index 3c3009fde..59dcc5108 100644
--- a/src/Arithmetic/Karatsuba.v
+++ b/src/Arithmetic/Karatsuba.v
@@ -150,6 +150,16 @@ Context (weight : nat -> Z)
       (fun sum_z => Positional.from_associational_cps weight _ (sum_z++sz1) f
       ))))))))))).
 
+  Definition goldilocks_mul s xs ys := goldilocks_mul_cps s xs ys id.
+  Lemma goldilocks_mul_id s xs ys R f :
+    @goldilocks_mul_cps s xs ys R f = f (goldilocks_mul s xs ys).
+  Proof.
+    cbv [goldilocks_mul goldilocks_mul_cps id_with_alt_bounds Let_In].
+    repeat autounfold. autorewrite with uncps push_id.
+    reflexivity.
+  Qed.
+  Hint Opaque goldilocks_mul : uncps.
+  Hint Rewrite goldilocks_mul_id : uncps.
 
   Local Existing Instances Z.equiv_modulo_Reflexive
         RelationClasses.eq_Reflexive Z.equiv_modulo_Symmetric
@@ -157,9 +167,9 @@ Context (weight : nat -> Z)
         Z.modulo_equiv_modulo_Proper.
 
   Lemma goldilocks_mul_correct (p : Z) (p_nonzero : p <> 0) s (s_nonzero : s <> 0) (s2_modp : (s^2) mod p = (s+1) mod p) xs ys :
-    (eval weight (goldilocks_mul_cps s xs ys id)) mod p = (eval weight xs * eval weight ys) mod p.
+    (eval weight (goldilocks_mul s xs ys)) mod p = (eval weight xs * eval weight ys) mod p.
   Proof.
-    cbv [goldilocks_mul_cps Let_In].
+    cbv [goldilocks_mul_cps goldilocks_mul Let_In].
     Zmod_to_equiv_modulo.
     progress autounfold.
     progress autorewrite with push_id cancel_pair uncps push_basesystem_eval.
@@ -189,3 +199,5 @@ Context (weight : nat -> Z)
     assumption. assumption. omega.
   Qed.
 End Karatsuba.
+Hint Opaque goldilocks_mul : uncps.
+Hint Rewrite goldilocks_mul_id : uncps.
\ No newline at end of file
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v
index ce8bb86fa..e7bd35424 100644
--- a/src/Specific/Karatsuba.v
+++ b/src/Specific/Karatsuba.v
@@ -215,9 +215,9 @@ Ltac basesystem_partial_evaluation_RHS :=
    [ replace_with_vm_compute t1; clear t1 | reflexivity ].
     Print id_tuple_with_alt.
   Definition goldilocks_mul_sig :
-    {mul : (Z^sz -> Z^sz -> Z^(sz+half_sz))%type |
+    {mul : (Z^sz -> Z^sz -> Z^(sz2))%type |
      forall a b : Z^sz,
-       mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2 ^ 224) a b id}.
+       mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2 ^ 224) a b (fun ab => Positional.reduce_cps (n:=sz2) wt s c ab id)}.
   Proof.
     eexists; cbv beta zeta; intros.
     cbv [goldilocks_mul_cps].
@@ -228,7 +228,7 @@ Ltac basesystem_partial_evaluation_RHS :=
   Defined.
 
   Definition mul_sig :
-    {mul : (Z^sz -> Z^sz -> Z^(sz+half_sz))%type |
+    {mul : (Z^sz -> Z^sz -> Z^sz2)%type |
                forall a b : Z^sz,
                  let eval := Positional.Fdecode (m := m) wt in
                  Positional.Fdecode (m := m) wt (mul a b) = (eval a  * eval b)%F}.
@@ -236,7 +236,7 @@ Ltac basesystem_partial_evaluation_RHS :=
     eexists; cbv beta zeta; intros.
     pose proof wt_nonzero.
     let x := constr:(
-               goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2^224) a b  id) in
+               goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2^224) a b (fun ab => Positional.reduce_cps (n:=sz2) wt s c ab id)) in
     F_mod_eq;
       transitivity (Positional.eval wt x); repeat autounfold;
 
@@ -244,14 +244,14 @@ Ltac basesystem_partial_evaluation_RHS :=
    | autorewrite with uncps push_id push_basesystem_eval;
      apply goldilocks_mul_correct; try assumption; cbv; congruence ].
    cbv [mod_eq]; apply f_equal2;
-     [  | reflexivity ]; apply f_equal.
-   etransitivity;[|apply (proj2_sig (goldilocks_mul_sig))].
+     [  | reflexivity ]. apply f_equal.
+   etransitivity; [|apply (proj2_sig (goldilocks_mul_sig))].
    cbv [proj1_sig goldilocks_mul_sig].
    reflexivity.
  Defined.
 
   Definition square_sig :
-    {square : (Z^sz -> Z^(sz+half_sz))%type |
+    {square : (Z^sz -> Z^sz2)%type |
                forall a : Z^sz,
                  let eval := Positional.Fdecode (m := m) wt in
                  Positional.Fdecode (m := m) wt (square a) = (eval a  * eval a)%F}.
@@ -331,7 +331,6 @@ Ltac basesystem_partial_evaluation_RHS :=
    reflexivity.
   Defined.
 
-  (* TODO: implement reduce, reduce after mul and square
   Definition ring_56 :=
     (Ring.ring_by_isomorphism
          (F := F m)
@@ -355,7 +354,7 @@ Ltac basesystem_partial_evaluation_RHS :=
          (proj2_sig add_sig)
          (proj2_sig sub_sig)
          (proj2_sig mul_sig)
-      ). *)
+      ).
 
 (*
 Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig).