Prove In_to_list_left_tl, In_left_hd, to_list_left_append

3 files changed, 44 insertions, 24 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index 4cedadfd0..d00fd9bdc 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -30,7 +30,7 @@ Section WordByWordMontgomery.
   Local Notation eval_add := (@eval_add_same (Z.pos r) (Zorder.Zgt_pos_0 _)).
   Local Notation eval_add' := (@eval_add_S1 (Z.pos r) (Zorder.Zgt_pos_0 _)).
   Local Notation drop_high := (@drop_high (S R_numlimbs)).
-  Local Notation small_drop_high := (@small_drop_high (Z.pos r) (Zorder.Zgt_pos_0 _) (S R_numlimbs)).
+  Local Notation small_drop_high := (@small_drop_high (Z.pos r) (S R_numlimbs)).
   Context (A_numlimbs : nat)
           (N : T R_numlimbs)
           (A : T A_numlimbs)
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index d69a36449..e01b39ee8 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -784,14 +784,6 @@ Section API.
     Definition eval {n} (p : T n) : Z :=
       B.Positional.eval (uweight bound) p.
 
-    Lemma In_to_list_left_tl n (p : Z^S n) x:
-      In x (to_list n (left_tl p)) -> In x (to_list (S n) p).
-    Admitted.
-
-    Lemma In_left_hd n (p : Z^S n):
-      In (left_hd p) (to_list _ p).
-    Admitted.
-
     Lemma eval_small n (p : T n) (Hsmall : small p) :
       0 <= eval p < uweight bound n.
     Proof.
@@ -804,7 +796,7 @@ Section API.
              | _ =>
                let H := fresh "H" in
                match type of IHn with
-                 ?P -> _ => assert P as H by auto using In_to_list_left_tl;
+                 ?P -> _ => assert P as H by auto using Tuple.In_to_list_left_tl;
                               specialize (IHn H)
                end
              | |- context [?b ^ Z.of_nat (S ?n)] =>
@@ -815,7 +807,7 @@ Section API.
              | _ => omega
              end.
 
-        specialize (Hsmall _ (In_left_hd _ p)).
+        specialize (Hsmall _ (Tuple.In_left_hd _ p)).
         split; [Z.zero_bounds; omega |].
         apply Z.lt_le_trans with (m:=bound^Z.of_nat n * (left_hd p+1)).
         { rewrite Z.mul_add_distr_l.
@@ -900,10 +892,6 @@ Section API.
     Proof. apply eval_add; omega. Qed.
     Hint Rewrite eval_add_same eval_add_S1 eval_add_S2 : push_basesystem_eval.
 
-    Lemma to_list_left_append {n} (p:T n) x:
-      (to_list _ (left_append x p)) = to_list n p ++ x :: nil.
-    Admitted.
-
     Lemma uweight_le_mono n m : (n <= m)%nat ->
       uweight bound n <= uweight bound m.
     Proof.
@@ -949,7 +937,7 @@ Section API.
         match goal with
           H : _ \/ False |- _ => destruct H; [|exfalso; assumption] end.
         subst x. apply Z.mod_pos_bound, Z.gt_lt, bound_pos. }
-      { rewrite to_list_left_append.
+      { rewrite Tuple.to_list_left_append.
         let H := fresh "H" in
         intros x H; apply in_app_or in H; destruct H;
           [solve[auto]| cbv [In] in H; destruct H;
@@ -968,7 +956,7 @@ Section API.
       intros. pose_all.
       cbv [small add_cps add Let_In]. repeat autounfold.
       autorewrite with uncps push_id.
-      rewrite to_list_left_append.
+      rewrite Tuple.to_list_left_append.
       let H := fresh "H" in intros x H; apply in_app_or in H;
                               destruct H as [H | H];
                               [apply (small_compact _ _ H)
@@ -1000,7 +988,7 @@ Section API.
     Qed.
 
     Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v).
-    Proof. cbv [small]. auto using In_to_list_left_tl. Qed.
+    Proof. cbv [small]. auto using Tuple.In_to_list_left_tl. Qed.
 
     Lemma small_divmod n (p: T (S n)) (Hsmall : small p) :
       left_hd p = eval p / uweight bound n /\ eval (left_tl p) = eval p mod (uweight bound n).
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v
index 67cb4ebaa..587a25290 100644
--- a/src/Util/CPSUtil.v
+++ b/src/Util/CPSUtil.v
@@ -317,7 +317,7 @@ Module Tuple.
     rewrite IHn. reflexivity.
   Qed.
 
-  Definition tl_cps {A n} : 
+  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)
@@ -329,7 +329,7 @@ Module Tuple.
     @tl_cps A n xs R f = f (tl xs).
   Proof. destruct n; reflexivity. Qed.
 
-  Definition hd_cps {A n} : 
+  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)
@@ -340,8 +340,8 @@ Module Tuple.
   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} : 
+
+  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)
@@ -349,7 +349,7 @@ Module Tuple.
   | 0%nat => fun _ _ f => f tt
   | S n' =>
       fun xs _ f =>
-        tl_cps xs (fun xtl => hd_cps xs (fun xhd => 
+        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 :
@@ -360,7 +360,7 @@ Module Tuple.
     rewrite IHn. reflexivity.
   Qed.
 
-  Fixpoint left_hd_cps {A n} : 
+  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)
@@ -377,6 +377,38 @@ Module Tuple.
     rewrite IHn. reflexivity.
   Qed.
 
+  Lemma In_left_hd {A} n (p : tuple A (S n))
+    : In (left_hd p) (to_list _ p).
+  Proof.
+    simpl in *.
+    induction n as [|n IHn].
+    { left; reflexivity. }
+    { destruct p; simpl in *; right; auto. }
+  Qed.
+
+  Lemma In_to_list_left_tl {A} n (p : tuple A (S n)) x
+    : In x (to_list n (left_tl p)) -> In x (to_list (S n) p).
+  Proof.
+    simpl in *.
+    remember (to_list n (left_tl p)) as ls eqn:H.
+    intro Hin; revert Hin H.
+    revert n p.
+    induction ls as [|l ls IHls], n.
+    { simpl; intros ? []. }
+    { simpl; intros ? []. }
+    { simpl; congruence. }
+    { simpl; intros [? p] [H0|H1] H; simpl in *;
+        setoid_rewrite to_list_append in H;
+        inversion H; clear H; subst; auto. }
+  Qed.
+
+  Lemma to_list_left_append {A} {n} (p:tuple A n) x
+    : (to_list _ (left_append x p)) = to_list n p ++ x :: nil.
+  Proof.
+    destruct n as [|n]; simpl in *; [ reflexivity | ].
+    induction n as [|n IHn]; simpl in *; [ reflexivity | ].
+    destruct p; simpl in *; rewrite IHn; simpl; reflexivity.
+  Qed.
 End Tuple.
 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