Move side lemmas to appropriate files

3 files changed, 87 insertions, 161 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index 48c4f2402..b3eff4caa 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -144,3 +144,32 @@ Section LengthProofs.
   Qed.
 
 End LengthProofs.
+
+Section ConditionalSubtractModulusProofs.
+  Context `{prm :PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
+
+  Lemma ge_modulus_spec : forall u, length u = length limb_widths ->
+    (ge_modulus u = false <-> 0 <= BaseSystem.decode base u < modulus).
+  Proof.
+  Admitted.
+
+  Lemma conditional_subtract_modulus_spec : forall u cond,
+    length u = length limb_widths ->
+    BaseSystem.decode base (conditional_subtract_modulus u cond) =
+    BaseSystem.decode base u - (if cond then 1 else 0) * modulus.
+  Proof.
+  Admitted.
+
+  Lemma conditional_subtract_modulus_preserves_bounded : forall u,
+      bounded limb_widths u ->
+      bounded limb_widths (conditional_subtract_modulus u (ge_modulus u)).
+  Proof.
+  Admitted.
+
+  Lemma conditional_subtract_lt_modulus : forall u,
+    bounded limb_widths u ->
+    ge_modulus (conditional_subtract_modulus u (ge_modulus u)) = false.
+  Proof.
+  Admitted.
+End ConditionalSubtractModulusProofs.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index ae5db0fc2..a551adc2f 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -92,87 +92,12 @@ Section FieldOperationProofs.
     + eauto using base_upper_bound_compatible, limb_widths_nonneg.
   Qed.
 
-  (* TODO : move to Pow2Base *)
-  Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil.
-  Proof.
-    cbv [bounded]; intros.
-    rewrite nth_default_nil.
-    apply nth_default_preserves_properties; intros; split; zero_bounds.
-  Qed.
-
-  (* TODO : move to Pow2Base *)
-  Lemma length_encode' : forall lw z i, length (encode' lw z i) = i.
-  Proof.
-    induction i; intros; simpl encode'; distr_length.
-  Qed.
-  Hint Rewrite length_encode' : distr_length.
-
-  (* TODO : move to ListUtil *)
-  Lemma nth_default_firstn : forall {A} (d : A) l i n,
-    nth_default d (firstn n l) i = if le_dec n (length l)
-                                   then if lt_dec i n then nth_default d l i else d
-                                   else nth_default d l i.
-  Proof.
-    induction n; intros; break_if; autorewrite with push_nth_default; auto; try omega.
-    + rewrite (firstn_succ d) by omega.
-      autorewrite with push_nth_default; repeat (break_if; distr_length);
-        rewrite Min.min_l in * by omega; try omega.
-      - apply IHn; omega.
-      - replace i with n in * by omega.
-        rewrite Nat.sub_diag.
-        autorewrite with push_nth_default; auto.
-      - rewrite nth_default_out_of_bounds; distr_length; auto.
-    + rewrite firstn_all2 by omega.
-      auto.
-  Qed.
-  Hint Rewrite @nth_default_firstn : push_nth_default.
-
-  (* TODO : move to Pow2Base *)
-  Lemma bounded_encode' : forall z i, (0 <= z) ->
-    bounded (firstn i limb_widths) (encode' limb_widths z i).
-  Proof.
-    intros; induction i; simpl encode';
-      repeat match goal with
-             | |- _ => progress intros
-             | |- _ => progress autorewrite with push_nth_default in * 
-             | |- _ => progress autorewrite with Ztestbit
-             | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in *
-             | |- _ => rewrite Z.testbit_pow2_mod by auto
-             | |- _ => rewrite Z.ones_spec by zero_bounds
-             | |- _ => rewrite sum_firstn_succ_default
-             | |- _ => rewrite nth_default_out_of_bounds by distr_length
-             | |- _ => break_if; distr_length
-             | |- _ => apply bounded_nil_r
-             | |- appcontext[nth_default _ (_ :: nil) ?i] => case_eq i; intros; autorewrite with push_nth_default
-             | |- Z.pow2_mod (?a >> ?b) _ = (?a >> ?b) => apply Z.bits_inj'
-             | IH : forall i, _ = nth_default 0 (encode' _ _ _) i
-                              |- appcontext[nth_default 0 limb_widths ?i] => specialize (IH i)
-             | H : In _ (firstn _ _) |- _ => apply In_firstn in H
-             | H1 : ~ (?a < ?b)%nat, H2 : (?a < S ?b)%nat |- _ =>
-               progress replace a with b in * by omega
-             | H : bounded _ _ |- bounded _ _ =>
-               apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H
-             | |- _ => solve [auto] 
-             | |- _ => contradiction
-             | |- _ => reflexivity
-             end.
-  Qed.
-
-  (* TODO : move to Pow2Base *)
-  Lemma bounded_encodeZ : forall z, (0 <= z) ->
-    bounded limb_widths (encodeZ limb_widths z).
-  Proof.
-    cbv [encodeZ]; intros.
-    pose proof (bounded_encode' z (length limb_widths)) as Hencode'.
-    rewrite firstn_all in Hencode'; auto.
-  Qed.
-
   Lemma bounded_encode : forall x, bounded limb_widths (to_list (encode x)).
   Proof.
     intros.
     cbv [encode]; rewrite to_list_from_list.
     cbv [ModularBaseSystemList.encode].
-    apply bounded_encodeZ.
+    apply bounded_encodeZ; auto.
     apply F.to_Z_range.
     pose proof prime_modulus; prime_bound.
   Qed.
@@ -873,55 +798,6 @@ Section CanonicalizationProofs.
       auto using length_carry_full, bound_after_second_loop.
   Qed.
 
-  Lemma ge_modulus_spec : forall u, length u = length limb_widths ->
-    (ge_modulus u = false <-> 0 <= BaseSystem.decode base u < modulus).
-  Proof.
-  Admitted.
-
-  Lemma conditional_subtract_modulus_spec : forall u cond,
-    length u = length limb_widths ->
-    BaseSystem.decode base (conditional_subtract_modulus u cond) =
-    BaseSystem.decode base u - (if cond then 1 else 0) * modulus.
-  Proof.
-  Admitted.
-
-  Lemma conditional_subtract_modulus_preserves_bounded : forall u,
-      bounded limb_widths u ->
-      bounded limb_widths (conditional_subtract_modulus u (ge_modulus u)).
-  Proof.
-  Admitted.
-
-  Lemma conditional_subtract_lt_modulus : forall u,
-    bounded limb_widths u ->
-    ge_modulus (conditional_subtract_modulus u (ge_modulus u)) = false.
-  Proof.
-  Admitted.
-
-  (* bounded canonical -> freeze bounded -> freeze canonical *)
-
-  Import SetoidList.
-  (* TODO : move to Tuple *)
-  Lemma fieldwise_to_list_iff : forall {T n} R (s t : tuple T n),
-      (fieldwise R s t <-> Forall2 R (to_list _ s) (to_list _ t)).
-  Proof.
-    induction n; split; intros.
-    + constructor.
-    + cbv [fieldwise]. auto.
-    + destruct n; cbv [tuple to_list fieldwise] in *.
-      - cbv [to_list']; auto.
-      - simpl in *. destruct s,t; cbv [fst snd] in *.
-        constructor; intuition auto.
-        apply IHn; auto.
-    + destruct n; cbv [tuple to_list fieldwise] in *.
-      - cbv [fieldwise']; auto.
-        cbv [to_list'] in *; inversion H; auto.
-      - simpl in *. destruct s,t; cbv [fst snd] in *.
-        inversion H; subst.
-        split; try assumption.
-        apply IHn; auto.
-  Qed.
-  
-
   Local Notation initial_bounds u := 
       (forall n : nat,
        0 <= to_list (length limb_widths) u [n] <
@@ -931,38 +807,6 @@ Section CanonicalizationProofs.
         else (2 ^ B) >> (limb_widths [Init.Nat.pred n]))).
   Local Notation minimal_rep u := ((bounded limb_widths (to_list (length limb_widths) u))
                                    /\ (ge_modulus (to_list _ u) = false)).
-  Import Morphisms.
-  (* TODO : move somewhere *)
-  Check Proper.
-  Lemma decode_Proper : Proper (Logic.eq ==> (Forall2 Logic.eq) ==> Logic.eq) decode'.
-  Proof.
-    repeat intro; subst.
-    revert y y0 H0; induction x0; intros.
-    + inversion H0. rewrite !decode_nil.
-      reflexivity.
-    + inversion H0; subst.
-      destruct y as [|y0 y]; [rewrite !decode_base_nil; reflexivity | ].
-      specialize (IHx0 y _ H4).
-      rewrite !peel_decode.
-      f_equal; auto.
-  Qed.
-
-  (* TODO : move to ListUtil *)
-  Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys ->
-    (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))).
-  Proof.
-    split; intros.
-    + revert xs ys H H0 H1.
-      induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto.
-      eapply IHi; auto. omega.
-    + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor.
-      - specialize (H0 0%nat); specialize_by omega.
-        autorewrite with push_nth_default in *; auto.
-      - apply IHxs; try omega.
-        intros.
-        specialize (H0 (S i)); specialize_by omega.
-        autorewrite with push_nth_default in *; auto.
-  Qed.
   
   Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v ->
     (fieldwise Logic.eq u v <->
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 7158dc22a..be2986ce6 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -555,6 +555,13 @@ Section Pow2BaseProofs.
     autorewrite with distr_length simpl_sum_firstn pull_Zpow.
     reflexivity.
   Qed.
+  
+  Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil.
+  Proof.
+    cbv [bounded]; intros.
+    rewrite nth_default_nil.
+    apply nth_default_preserves_properties; intros; split; zero_bounds.
+  Qed.
 
   Section make_base_vector.
     Local Notation k := (sum_firstn limb_widths (length limb_widths)).
@@ -639,6 +646,8 @@ Section BitwiseDecodeEncode.
                                           sum_firstn limb_widths (i + j) <=
                                           sum_firstn limb_widths i + sum_firstn limb_widths j).
   Local Hint Resolve limb_widths_nonneg.
+  Local Hint Resolve nth_default_limb_widths_nonneg.
+  Local Hint Resolve sum_firstn_limb_widths_nonneg.
   Local Notation "w[ i ]" := (nth_default 0 limb_widths i).
   Local Notation base := (base_from_limb_widths limb_widths).
   Local Notation upper_bound := (upper_bound limb_widths).
@@ -650,7 +659,7 @@ Section BitwiseDecodeEncode.
     + rewrite encode'_zero. reflexivity.
     + rewrite encode'_succ, <-IHi by omega.
       simpl; do 2 f_equal.
-      rewrite Z.land_ones, Z.shiftr_div_pow2 by auto using sum_firstn_limb_widths_nonneg.
+      rewrite Z.land_ones, Z.shiftr_div_pow2 by auto.
       match goal with H : (S _ <= length limb_widths)%nat |- _ =>
         apply le_lt_or_eq in H; destruct H end.
       - repeat f_equal; rewrite nth_default_base by (omega || auto); reflexivity.
@@ -660,6 +669,50 @@ Section BitwiseDecodeEncode.
         congruence.
   Qed.
 
+  Lemma length_encode' : forall lw z i, length (encode' lw z i) = i.
+  Proof.
+    induction i; intros; simpl encode'; distr_length.
+  Qed.
+  Hint Rewrite length_encode' : distr_length.
+
+  Lemma bounded_encode' : forall z i, (0 <= z) ->
+    bounded (firstn i limb_widths) (encode' limb_widths z i).
+  Proof.
+    intros; induction i; simpl encode';
+      repeat match goal with
+             | |- _ => progress intros
+             | |- _ => progress autorewrite with push_nth_default in * 
+             | |- _ => progress autorewrite with Ztestbit
+             | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in *
+             | |- _ => rewrite Z.testbit_pow2_mod by auto
+             | |- _ => rewrite Z.ones_spec by zero_bounds
+             | |- _ => rewrite sum_firstn_succ_default
+             | |- _ => rewrite nth_default_out_of_bounds by distr_length
+             | |- _ => break_if; distr_length
+             | |- _ => apply bounded_nil_r
+             | |- appcontext[nth_default _ (_ :: nil) ?i] => case_eq i; intros; autorewrite with push_nth_default
+             | |- Z.pow2_mod (?a >> ?b) _ = (?a >> ?b) => apply Z.bits_inj'
+             | IH : forall i, _ = nth_default 0 (encode' _ _ _) i
+                              |- appcontext[nth_default 0 limb_widths ?i] => specialize (IH i)
+             | H : In _ (firstn _ _) |- _ => apply In_firstn in H
+             | H1 : ~ (?a < ?b)%nat, H2 : (?a < S ?b)%nat |- _ =>
+               progress replace a with b in * by omega
+             | H : bounded _ _ |- bounded _ _ =>
+               apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H
+             | |- _ => solve [auto] 
+             | |- _ => contradiction
+             | |- _ => reflexivity
+             end.
+  Qed.
+
+  Lemma bounded_encodeZ : forall z, (0 <= z) ->
+    bounded limb_widths (encodeZ limb_widths z).
+  Proof.
+    cbv [encodeZ]; intros.
+    pose proof (bounded_encode' z (length limb_widths)) as Hencode'.
+    rewrite firstn_all in Hencode'; auto.
+  Qed.
+
   Lemma base_upper_bound_compatible : @base_max_succ_divide base upper_bound.
   Proof.
     unfold base_max_succ_divide; intros i lt_Si_length.
@@ -667,14 +720,14 @@ Section BitwiseDecodeEncode.
     rewrite Nat.lt_eq_cases in lt_Si_length; destruct lt_Si_length;
       rewrite !nth_default_base by (omega || auto).
     + erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega).
-      rewrite Z.pow_add_r; eauto using sum_firstn_limb_widths_nonneg, nth_default_limb_widths_nonneg.
+      rewrite Z.pow_add_r; eauto.
       apply Z.divide_factor_r.
     + rewrite nth_default_out_of_bounds by (distr_length; omega).
       unfold Pow2Base.upper_bound.
       replace (length limb_widths) with (S (pred (length limb_widths))) by omega.
       replace i with (pred (length limb_widths)) by omega.
       erewrite sum_firstn_succ by (eapply nth_error_Some_nth_default with (x := 0); omega).
-      rewrite Z.pow_add_r; eauto using sum_firstn_limb_widths_nonneg, nth_default_limb_widths_nonneg.
+      rewrite Z.pow_add_r; eauto.
       apply Z.divide_factor_r.
   Qed.
   Hint Resolve base_upper_bound_compatible.
@@ -686,7 +739,7 @@ Section BitwiseDecodeEncode.
     assert (length base = length limb_widths) by distr_length.
     unfold encodeZ; rewrite encode'_spec by omega.
     erewrite BaseSystemProofs.encode'_spec; unfold Pow2Base.upper_bound;
-      zero_bounds; intros; eauto using sum_firstn_limb_widths_nonneg, base_positive, b0_1. {
+      zero_bounds; intros; eauto using base_positive, b0_1. {
       rewrite nth_default_out_of_bounds by omega.
       reflexivity.
     } {