finish tuple-ifying Montgomery API

2 files changed, 69 insertions, 11 deletions

diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index 88bf2dc46..ecc11ccfd 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -720,18 +720,16 @@ Section API.
 
   Definition zero {n:nat} : T n := B.Positional.zeros n.
 
-  Axiom JADE_HOW_DO_I_IMPLEMENT_THIS : forall {T}, T.
-
-  Definition join0_cps {n:nat} (p : T n) {R} (f:T (S n) -> R) : R
-    := JADE_HOW_DO_I_IMPLEMENT_THIS.
+  Definition join0_cps {n:nat} (p : T n) {R} (f:T (S n) -> R)
+    := Tuple.left_append_cps 0 p f.
   Definition join0 {n} p : T (S n) := @join0_cps n p _ id.
 
   Definition divmod_cps {n} (p : T (S n)) {R} (f:T n * Z->R) : R
-    := JADE_HOW_DO_I_IMPLEMENT_THIS (*f (List.tl p, List.hd 0 p)*).
+    := Tuple.tl_cps p (fun d => Tuple.hd_cps p (fun m =>  f (d, m))).
   Definition divmod {n} p : T n * Z := @divmod_cps n p _ id.
 
-  Definition drop_high_cps {n : nat} (p : T (S n)) {R} (f:T n->R) : R
-    := JADE_HOW_DO_I_IMPLEMENT_THIS (*firstn_cps n p f*).
+  Definition drop_high_cps {n : nat} (p : T (S n)) {R} (f:T n->R)
+    := Tuple.left_tl_cps p f.
   Definition drop_high {n} p : T n := @drop_high_cps n p _ id.
 
   Definition scmul_cps {n} (c : Z) (p : T n) {R} (f:T (S n)->R) :=
@@ -755,15 +753,15 @@ Section API.
 
     Lemma join0_id n p R f :
       @join0_cps n p R f = f (join0 p).
-    Proof. cbv [join0_cps join0]. exact JADE_HOW_DO_I_IMPLEMENT_THIS; prove_id. Qed.
+    Proof. cbv [join0_cps join0]. prove_id. Qed.
 
     Lemma divmod_id n p R f :
       @divmod_cps n p R f = f (divmod p).
-    Proof. cbv [divmod_cps divmod]. exact JADE_HOW_DO_I_IMPLEMENT_THIS; prove_id. Qed.
+    Proof. cbv [divmod_cps divmod]; prove_id. Qed.
 
     Lemma drop_high_id n p R f :
       @drop_high_cps n p R f = f (drop_high p).
-    Proof. cbv [drop_high_cps drop_high]. exact JADE_HOW_DO_I_IMPLEMENT_THIS; prove_id. Qed.
+    Proof. cbv [drop_high_cps drop_high]; prove_id. Qed.
 
     Lemma scmul_id n c p R f :
       @scmul_cps n c p R f = f (scmul c p).
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index 67a909a61..67cb4ebaa 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -316,8 +316,68 @@ Module Tuple.
     simpl left_append. simpl left_append_cps.
     rewrite IHn. reflexivity.
   Qed.
+
+  Definition tl_cps {A n} : 
+    tuple A (S n) -> forall {R}, (tuple A n -> R) -> R :=
+  match
+    n as n0 return (tuple A (S n0) -> forall R, (tuple A n0 -> R) -> R)
+  with
+  | 0%nat => fun _ _ f => f tt
+  | S n' => fun xs _ f => f (fst xs)
+  end.
+  Lemma tl_cps_correct A n xs R f :
+    @tl_cps A n xs R f = f (tl xs).
+  Proof. destruct n; reflexivity. Qed.
+
+  Definition hd_cps {A n} : 
+    tuple A (S n) -> forall {R}, (A -> R) -> R :=
+  match
+    n as n0 return (tuple A (S n0) -> forall R, (A -> R) -> R)
+  with
+  | 0%nat => fun x _ f => f x
+  | S n' => fun xs _ f => f (snd xs)
+  end.
+  Lemma hd_cps_correct A n xs R f :
+    @hd_cps A n xs R f = f (hd xs).
+  Proof. destruct n; reflexivity. Qed.
   
+  Fixpoint left_tl_cps {A n} : 
+    tuple A (S n) -> forall {R}, (tuple A n -> R) -> R :=
+  match
+    n as n0 return (tuple A (S n0) -> forall R, (tuple A n0 -> R) -> R)
+  with
+  | 0%nat => fun _ _ f => f tt
+  | S n' =>
+      fun xs _ f =>
+        tl_cps xs (fun xtl => hd_cps xs (fun xhd => 
+          left_tl_cps xtl (fun r => f (append xhd r))))
+  end.
+  Lemma left_tl_cps_correct A n xs R f :
+    @left_tl_cps A n xs R f = f (left_tl xs).
+  Proof.
+    induction n; [reflexivity|].
+    simpl left_tl. simpl left_tl_cps.
+    rewrite IHn. reflexivity.
+  Qed.
+
+  Fixpoint left_hd_cps {A n} : 
+    tuple A (S n) -> forall {R}, (A -> R) -> R :=
+  match
+    n as n0 return (tuple A (S n0) -> forall R, (A -> R) -> R)
+  with
+  | 0%nat => fun x _ f => f x
+  | S n' =>
+      fun xs _ f => tl_cps xs (fun xtl => left_hd_cps xtl f)
+  end.
+  Lemma left_hd_cps_correct A n xs R f :
+    @left_hd_cps A n xs R f = f (left_hd xs).
+  Proof.
+    induction n; [reflexivity|].
+    simpl left_hd. simpl left_hd_cps.
+    rewrite IHn. reflexivity.
+  Qed.
+
 End Tuple.
-Hint Rewrite @Tuple.map_cps_correct @Tuple.left_append_cps_correct : uncps.
+Hint Rewrite @Tuple.map_cps_correct @Tuple.left_append_cps_correct @Tuple.left_tl_cps_correct @Tuple.left_hd_cps_correct @Tuple.tl_cps_correct @Tuple.hd_cps_correct : uncps.
 Hint Rewrite @Tuple.mapi_with_cps_correct @Tuple.mapi_with'_cps_correct
      using (intros; autorewrite with uncps; auto): uncps.