Add some list util, and decode'_map_mul

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m41.37s | Total                                             | 3m29.78s || +0m11.59s
------------------------------------------------------------------------------------
0m49.73s | Specific/GF25519                                  | 0m31.66s || +0m18.06s
0m23.64s | ModularArithmetic/Pow2BaseProofs                  | 0m31.36s || -0m07.71s
0m42.29s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m44.80s || -0m02.50s
0m08.88s | Specific/GF1305                                   | 0m07.07s || +0m01.81s
0m19.09s | ModularArithmetic/ModularBaseSystemProofs         | 0m19.86s || -0m00.76s
0m16.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.74s || -0m00.11s
0m15.31s | Experiments/SpecEd25519                           | 0m14.40s || +0m00.91s
0m10.10s | Testbit                                           | 0m10.15s || -0m00.05s
0m04.95s | BaseSystemProofs                                  | 0m04.49s || +0m00.46s
0m03.96s | Util/ListUtil                                     | 0m03.16s || +0m00.79s
0m03.40s | Experiments/SpecificCurve25519                    | 0m03.31s || +0m00.08s
0m02.36s | ModularArithmetic/BarrettReduction/ZBounded       | 0m02.69s || -0m00.33s
0m02.23s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.24s || -0m00.01s
0m02.14s | Util/Tuple                                        | 0m01.87s || +0m00.27s
0m01.92s | Experiments/EdDSARefinement                       | 0m01.85s || +0m00.06s
0m01.71s | Encoding/PointEncodingPre                         | 0m01.67s || +0m00.04s
0m01.71s | BaseSystem                                        | 0m01.28s || +0m00.42s
0m01.28s | ModularArithmetic/Montgomery/ZBounded             | 0m00.85s || +0m00.43s
0m01.16s | ModularArithmetic/ExtendedBaseVector              | 0m01.65s || -0m00.49s
0m01.04s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.94s || +0m00.10s
0m00.95s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.96s || -0m00.01s
0m00.89s | ModularArithmetic/ModularBaseSystemField          | 0m00.90s || -0m00.01s
0m00.87s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.77s || +0m00.09s
0m00.78s | Encoding/ModularWordEncodingTheorems              | 0m00.69s || +0m00.09s
0m00.73s | Spec/EdDSA                                        | 0m00.67s || +0m00.05s
0m00.69s | Util/AdditionChainExponentiation                  | 0m00.74s || -0m00.05s
0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.73s || -0m00.04s
0m00.67s | ModularArithmetic/ModularBaseSystemList           | 0m00.71s || -0m00.03s
0m00.61s | ModularArithmetic/ModularBaseSystem               | 0m00.70s || -0m00.08s
0m00.52s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.45s || +0m00.07s
0m00.47s | ModularArithmetic/Pow2Base                        | 0m00.42s || +0m00.04s

3 files changed, 184 insertions, 140 deletions

diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index 8de0fdd0a..6e5bbbaea 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+Require Import Coq.Lists.List Coq.micromega.Psatz.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
@@ -73,6 +73,22 @@ Section BaseSystemProofs.
     autorewrite with core; ring_simplify; auto.
   Qed.
 
+  Lemma decode'_map_mul : forall v xs bs,
+    decode' (map (Z.mul v) bs) xs =
+    Z.mul v (decode' bs xs).
+  Proof.
+    unfold decode'.
+    induction xs; destruct bs; boring.
+    unfold accumulate; simpl; nia.
+  Qed.
+
+  Lemma decode_map_mul : forall v xs,
+    decode (map (Z.mul v) base) xs =
+    Z.mul v (decode base xs).
+  Proof.
+    unfold decode; intros; apply decode'_map_mul.
+  Qed.
+
   Lemma sub_rep : forall bs us vs, decode' bs (sub us vs) = decode' bs us - decode' bs vs.
   Proof.
     induction bs; destruct us; destruct vs; boring; ring.
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index ab0943ad6..631e3a970 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -13,22 +13,45 @@ Local Open Scope Z_scope.
 Create HintDb simpl_add_to_nth discriminated.
 Create HintDb push_upper_bound discriminated.
 Create HintDb pull_upper_bound discriminated.
+Create HintDb push_base_from_limb_widths discriminated.
+Create HintDb pull_base_from_limb_widths discriminated.
 
 Hint Extern 1 => progress autorewrite with push_upper_bound in * : push_upper_bound.
 Hint Extern 1 => progress autorewrite with pull_upper_bound in * : pull_upper_bound.
+Hint Extern 1 => progress autorewrite with push_base_from_limb_widths in * : push_base_from_limb_widths.
+Hint Extern 1 => progress autorewrite with pull_base_from_limb_widths in * : pull_base_from_limb_widths.
 
 Section Pow2BaseProofs.
   Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w).
   Local Notation base := (base_from_limb_widths limb_widths).
 
-  Lemma base_from_limb_widths_length : length base = length limb_widths.
+  Lemma base_from_limb_widths_length ls : length (base_from_limb_widths ls) = length ls.
   Proof.
-    clear limb_widths_nonneg.
-    induction limb_widths; [ reflexivity | simpl in * ].
+    clear limb_widths limb_widths_nonneg.
+    induction ls; [ reflexivity | simpl in * ].
     autorewrite with distr_length; auto.
   Qed.
   Hint Rewrite base_from_limb_widths_length : distr_length.
 
+  Lemma base_from_limb_widths_cons : forall l0 l,
+    base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l).
+  Proof. reflexivity. Qed.
+  Hint Rewrite base_from_limb_widths_cons : push_base_from_limb_widths.
+  Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths.
+
+  Lemma base_from_limb_widths_nil : base_from_limb_widths nil = nil.
+  Proof. reflexivity. Qed.
+  Hint Rewrite base_from_limb_widths_nil : push_base_from_limb_widths.
+
+  Lemma firstn_base_from_limb_widths : forall n, firstn n (base_from_limb_widths limb_widths) = base_from_limb_widths (firstn n limb_widths).
+  Proof.
+    clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *)
+    induction limb_widths as [|l ls IHls]; intros [|n]; try reflexivity.
+    autorewrite with push_base_from_limb_widths push_firstn; boring.
+  Qed.
+  Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths pull_firstn.
+  Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths push_firstn.
+
   Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n.
   Proof.
     unfold sum_firstn; intros.
@@ -47,6 +70,7 @@ Section Pow2BaseProofs.
     nth_error limb_widths i = Some w ->
     nth_error base (S i) = Some (two_p w * b).
   Proof.
+    clear limb_widths_nonneg. (* don't use this in the inductive hypothesis *)
     induction limb_widths; intros ? ? ? ? nth_err_w nth_err_b;
       unfold base_from_limb_widths in *; fold base_from_limb_widths in *;
       [rewrite (@nil_length0 Z) in *; omega | ].
@@ -151,12 +175,6 @@ Section Pow2BaseProofs.
      case_eq limb_widths; intros; [congruence | reflexivity].
    Qed.
 
-  Lemma base_from_limb_widths_cons : forall l0 l,
-    base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l).
-  Proof.
-    reflexivity.
-  Qed.
-
   Lemma base_from_limb_widths_app : forall l0 l
                                            (l0_nonneg : forall x, In x l0 -> 0 <= x)
                                            (l_nonneg : forall x, In x l -> 0 <= x),
@@ -169,6 +187,19 @@ Section Pow2BaseProofs.
       do 2 f_equal; apply map_ext; intros; lia. }
   Qed.
 
+  Lemma skipn_base_from_limb_widths : forall n, skipn n (base_from_limb_widths limb_widths) = map (Z.mul (two_p (sum_firstn limb_widths n))) (base_from_limb_widths (skipn n limb_widths)).
+  Proof.
+    intro n; pose proof (base_from_limb_widths_app (firstn n limb_widths) (skipn n limb_widths)) as H.
+    specialize_by eauto using In_firstn, In_skipn.
+    autorewrite with simpl_firstn simpl_skipn in *.
+    rewrite H, skipn_app, skipn_all by auto with arith distr_length; clear H.
+    simpl; distr_length.
+    apply Min.min_case_strong; intro;
+      unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn;
+        reflexivity.
+  Qed.
+  Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths pull_skipn.
+  Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths push_skipn.
 
   Lemma pow2_mod_bounded :forall lw us i, (forall w, In w lw -> 0 <= w) -> bounded lw us ->
                                           Z.pow2_mod (nth_default 0 us i) (nth_default 0 lw i) = nth_default 0 us i.
@@ -260,8 +291,9 @@ Section Pow2BaseProofs.
   Proof.
     intros; induction i;
     repeat match goal with
-           | |- _ => rewrite firstn_0, sum_firstn_0, decode_nil, Z.pow2_mod_0_r; reflexivity
+           | |- _ => rewrite sum_firstn_0, decode_nil, Z.pow2_mod_0_r; reflexivity
            | |- _ => progress distr_length
+           | |- _ => progress autorewrite with simpl_firstn
            | |- _ => rewrite firstn_succ with (d := 0)
            | |- _ => rewrite set_higher
            | |- _ => rewrite nth_default_base
@@ -444,40 +476,12 @@ Section Pow2BaseProofs.
   Lemma decode_shift_app : forall us0 us1, (length (us0 ++ us1) <= length limb_widths)%nat ->
     BaseSystem.decode base (us0 ++ us1) = (BaseSystem.decode (base_from_limb_widths (firstn (length us0) limb_widths)) us0) + ((BaseSystem.decode (base_from_limb_widths (skipn (length us0) limb_widths)) us1) << sum_firstn limb_widths (length us0)).
   Proof.
-    induction limb_widths as [|l ls IHls]; intros;
-      repeat match goal with
-             | _ => progress simpl @app
-             | [ |- context[BaseSystem.decode (base_from_limb_widths ?xs) ?ys] ]
-               => match constr:((xs, ys)) with
-                  | (nil, _) => is_var ys; destruct ys
-                  | (_::_, _) => is_var ys; destruct ys
-                  | (nil, ?y ++ _) => is_var y; destruct y
-                  | (_::_, ?y ++ _) => is_var y; destruct y
-                  end
-             | _ => rewrite base_from_limb_widths_cons, peel_decode
-             | _ => rewrite !two_p_correct, !(Z.mul_comm (2^_)), <- !Z.shiftl_mul_pow2
-             | _ => rewrite <- ?Z.add_assoc; apply Z.add_cancel_l
-             | [ H : forall w, In w (?x :: ?xs) -> @?P w |- _ ]
-               => assert (forall w, In w xs -> P w) by auto using in_cons;
-                    try assert (forall len, 0 <= sum_firstn xs len) by auto using sum_firstn_nonnegative;
-                    assert (P x) by auto using in_eq;
-                    clear H;
-                    cbv beta in *
-             | [ H : forall len, 0 <= sum_firstn ?ls len |- context[sum_firstn ?ls ?len'] ]
-               => specialize (H len')
-             | |- appcontext[tl (_ :: _)] => cbv [tl]
-             | |- appcontext[map (Z.mul ?a) _] => fold (BaseSystem.mul_each a);
-                                                    rewrite <-!mul_each_base, !mul_each_rep
-             | _ => progress distr_length
-             | _ => progress specialize_by auto using in_eq, in_cons
-             | _ => progress specialize_by omega
-             | _ => setoid_rewrite IHls; clear IHls
-             | _ => progress autorewrite with push_nth_default zsimplify simpl_skipn simpl_firstn simpl_sum_firstn
-             | _ => progress unfold BaseSystem.decode
-             | _ => progress autorewrite with push_Zshift Zshift_to_pow zsimplify
-             | _ => solve [auto using in_eq, Z.mul_comm]
-             | _ => nia
-            end.
+    unfold BaseSystem.decode; intros us0 us1 ?.
+    assert (0 <= sum_firstn limb_widths (length us0)) by auto using sum_firstn_nonnegative.
+    rewrite decode'_splice; autorewrite with push_firstn.
+    apply Z.add_cancel_l.
+    autorewrite with pull_base_from_limb_widths Zshift_to_pow zsimplify.
+    rewrite decode'_map_mul, two_p_correct; nia.
   Qed.
 
   Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat ->
@@ -567,6 +571,14 @@ Section Pow2BaseProofs.
     Qed.
   End make_base_vector.
 End Pow2BaseProofs.
+Hint Rewrite base_from_limb_widths_cons base_from_limb_widths_nil : push_base_from_limb_widths.
+Hint Rewrite <- base_from_limb_widths_cons : pull_base_from_limb_widths.
+
+Hint Rewrite <- @firstn_base_from_limb_widths : push_base_from_limb_widths pull_firstn.
+Hint Rewrite @firstn_base_from_limb_widths : pull_base_from_limb_widths push_firstn.
+Hint Rewrite <- @skipn_base_from_limb_widths : push_base_from_limb_widths pull_skipn.
+Hint Rewrite @skipn_base_from_limb_widths : pull_base_from_limb_widths push_skipn.
+
 Hint Rewrite @base_from_limb_widths_length : distr_length.
 Hint Rewrite @upper_bound_nil @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : push_upper_bound.
 Hint Rewrite <- @upper_bound_cons @upper_bound_app using solve [ eauto with znonzero ] : pull_upper_bound.
@@ -777,34 +789,15 @@ Section UniformBase.
   Admitted.
 
   (* TODO : move *)
-  Lemma firstn_map : forall {A B} n (f : A -> B) ls, firstn n (map f ls) = map f (firstn n ls).
-  Proof.
-    induction n; destruct ls; boring.
-  Qed.
-
-  (* TODO : move *)
-  Lemma firstn_base_from_limb_widths : forall n lw,
-      firstn n (base_from_limb_widths lw) = base_from_limb_widths (firstn n lw).
-  Proof.
-    induction n; destruct lw; boring.
-    f_equal.
-    rewrite <-IHn, firstn_map.
-    reflexivity.
-  Qed.
-
-  (* TODO : move *)
   Lemma tl_repeat : forall {A} xs n (x : A), (forall y, In y xs -> y = x) ->
                                              (n < length xs)%nat ->
                                              firstn n xs = firstn n (tl xs).
   Proof.
-    induction xs; destruct n; try solve [boring]; intros.
-    rewrite firstn_cons_S.
-    erewrite IHxs by (eauto using in_cons; distr_length).
-    destruct xs; distr_length.
-    cbv [tl].
-    rewrite firstn_cons_S.
-    f_equal.
-    transitivity x; [|symmetry]; eauto using in_eq, in_cons.
+    intros.
+    erewrite (repeat_spec_eq xs) by first [ eassumption | reflexivity ].
+    rewrite ListUtil.tl_repeat.
+    autorewrite with push_firstn.
+    apply f_equal; omega *.
   Qed.
 
   Lemma decode_tl_base : forall us, (length us < length limb_widths)%nat ->
@@ -853,7 +846,7 @@ Section SplitIndex.
        splits a bit index in the decoded value into a digit index and a bit
        index within the digit. Examples:
        limb_widths [4;4] : split_index 6 = (1,2)
-       limb_widths [26,25,26] : split_index 30 = (1,4) 
+       limb_widths [26,25,26] : split_index 30 = (1,4)
        limb_widths [26,25,26] : split_index 51 = (2,0)
   *)
   Local Notation "u # i" := (nth_default 0 u i) (at level 30).
@@ -882,10 +875,10 @@ Section SplitIndex.
   Proof.
     intros; functional induction (split_index' i index lw);
       repeat match goal with
-             | |- _ => break_if 
+             | |- _ => break_if
              | |- _ => rewrite sum_firstn_nil in *
              | |- _ => rewrite sum_firstn_succ_cons in *
-             | |- _ => progress distr_length 
+             | |- _ => progress distr_length
              | |- _ => progress (simpl fst; simpl snd)
              | H : appcontext [split_index' ?a ?b ?c] |- _ =>
                unique pose proof (split_index'_ge_index a b c)
@@ -967,7 +960,7 @@ Section SplitIndex.
     repeat match goal with
            | |- _ => progress autorewrite with Ztestbit natsimplify in *
            | |- _ => erewrite digit_select by eassumption
-           | |- _ => break_if 
+           | |- _ => break_if
            | |- _ => rewrite Z.testbit_pow2_mod by auto using nth_default_limb_widths_nonneg
            | |- _ => omega
            | |- _ => f_equal; omega
@@ -1006,7 +999,7 @@ Section SplitIndex.
              pose proof (bit_index_not_done i); specialize_by omega; omega
            end.
   Qed.
-  
+
     Lemma rem_bits_in_digit_le_rem_bits : forall i, 0 <= i < bitsIn limb_widths ->
                                                     i + (limb_widths # digit_index i - bit_index i) <= bitsIn limb_widths.
   Admitted.
@@ -1021,7 +1014,7 @@ Section SplitIndex.
   Lemma bit_index_pos_iff : forall i, 0 <= i ->
                                   0 < limb_widths # (digit_index i) - bit_index i <->
                                   i < sum_firstn limb_widths (length limb_widths).
-                                 
+
   Admitted.
 
   Lemma digit_index_not_lt_length : forall i, 0 <= i ->
@@ -1029,7 +1022,7 @@ Section SplitIndex.
                                               sum_firstn limb_widths (length limb_widths) <= i.
   Admitted.
 
-  
+
   Lemma le_remaining_bits : forall i, 0 <= i < sum_firstn limb_widths (length limb_widths) ->
                                       0 <= sum_firstn limb_widths (length limb_widths)
                                            - (i + (limb_widths # (digit_index i) - bit_index i)).
@@ -1068,8 +1061,8 @@ Section ConversionHelper.
            end.
   Qed.
 
-  Definition update_by_concat_bits num_low_bits bits x := concat_bits num_low_bits x bits. 
-  
+  Definition update_by_concat_bits num_low_bits bits x := concat_bits num_low_bits x bits.
+
 End ConversionHelper.
 
 Section Conversion.
@@ -1104,7 +1097,7 @@ Section Conversion.
              unique pose proof (bit_index_not_done lw H i)
            | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] =>
              unique pose proof (rem_bits_in_digit_le_rem_bits lw H i)
-           | |- _ => rewrite Z2Nat.id 
+           | |- _ => rewrite Z2Nat.id
            | |- _ => rewrite Nat2Z.inj_add
            | |- (Z.to_nat _ < Z.to_nat _)%nat => apply Z2Nat.inj_lt
            | |- (?a - _ < ?a - _) => apply Z.sub_lt_mono_l
@@ -1118,9 +1111,9 @@ Section Conversion.
     /\ bounded limb_widthsB out
     /\ Z.of_nat i <= bitsIn limb_widthsA
     /\ forall n, Z.testbit (decodeB out) n = if Z_lt_dec n (Z.of_nat i) then Z.testbit (decodeA inp) n else false.
-  
+
   Ltac subst_lia := repeat match goal with | x := _ |- _ => subst x end; subst; lia.
-  
+
   Lemma convert'_bounded_step : forall inp i out,
     bounded limb_widthsB out ->
     let digitA := digit_index limb_widthsA (Z.of_nat i) in
@@ -1171,8 +1164,8 @@ Section Conversion.
               unique pose proof (uniform_limb_widths_nonneg H0 lw H)
            | |- _ => progress specialize_by assumption
            | H : _ /\ _ |- _ => destruct H
-           | |- _ => break_if 
-           | |- _ => split 
+           | |- _ => break_if
+           | |- _ => split
            | a := digit_index _ ?i, H : forall x, 0 <= x < bitsIn _ -> _ |- _ => specialize (H i); forward H
            | |- _ => subst_lia
            | |- _ => apply bit_index_pos_iff; auto
@@ -1232,7 +1225,7 @@ Section Conversion.
            | d1 := digit_index ?lw _ |- Z.testbit (?a # ?d1) _ = Z.testbit (?a # ?d2) _ =>
                    assert (d2 = d1); [ | repeat f_equal]
            | H : ~ (?n < ?i), H0 : ?n < ?i + ?d,
-               d1 := digit_index ?lw ?i, H1 : digit_index ?lw ?n <> ?d1 |- _ => exfalso; apply H1  
+               d1 := digit_index ?lw ?i, H1 : digit_index ?lw ?n <> ?d1 |- _ => exfalso; apply H1
            | d := digit_index ?lw ?j,
                    b := bit_index ?lw ?j,
                    H : digit_index ?lw ?i = ?d |- _ =>
@@ -1262,12 +1255,12 @@ Section Conversion.
            | |- _ => progress intros
            | |- _ => progress specialize_by assumption
            | H : _ /\ _ |- _ => destruct H
-           | |- _ => break_if 
+           | |- _ => break_if
            | H : 0 <= ?i, H0 : forall x, 0 <= x -> if _ then _ else _ |- _ => specialize (H0 i H)
            | |- _ => repeat match goal with x := _ |- _ => subst x end; subst; lia
            end.
   Qed.
-  
+
   Lemma convert'_invariant_holds : forall inp i out,
     length inp = length limb_widthsA ->
     bounded limb_widthsA inp ->
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 70bcda49a..648edf5a1 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -22,6 +22,8 @@ Create HintDb pull_nth_default discriminated.
 Create HintDb push_nth_default discriminated.
 Create HintDb pull_firstn discriminated.
 Create HintDb push_firstn discriminated.
+Create HintDb pull_skipn discriminated.
+Create HintDb push_skipn discriminated.
 Create HintDb pull_update_nth discriminated.
 Create HintDb push_update_nth discriminated.
 Create HintDb znonzero discriminated.
@@ -40,6 +42,14 @@ Hint Rewrite
   : distr_length.
 
 Hint Extern 1 => progress autorewrite with distr_length in * : distr_length.
+Ltac distr_length := autorewrite with distr_length in *;
+  try solve [simpl in *; omega].
+
+Hint Rewrite @firstn_skipn : simpl_firstn simpl_skipn.
+Hint Rewrite @firstn_nil @firstn_cons @List.firstn_all @firstn_O @firstn_app_2 @List.firstn_firstn : push_firstn simpl_firstn.
+Hint Rewrite @firstn_app : push_firstn.
+Hint Rewrite <- @firstn_cons @firstn_app @List.firstn_firstn : pull_firstn.
+Hint Rewrite @firstn_all2 @removelast_firstn @firstn_removelast using omega : push_firstn simpl_firstn.
 
 Local Arguments value / .
 Local Arguments error / .
@@ -364,9 +374,6 @@ Hint Rewrite @nth_error_value_eq_nth_default using eassumption : simpl_nth_defau
 Lemma skipn0 : forall {T} (xs:list T), skipn 0 xs = xs.
 Proof. auto. Qed.
 
-Lemma firstn0 : forall {T} (xs:list T), firstn 0 xs = nil.
-Proof. auto. Qed.
-
 Lemma destruct_repeat : forall {A} xs y, (forall x : A, In x xs -> x = y) ->
   xs = nil \/ exists xs', xs = y :: xs' /\ (forall x : A, In x xs' -> x = y).
 Proof.
@@ -572,41 +579,20 @@ Proof.
   induction xs, xs', ys, ys'; boring; omega.
 Qed.
 
-Lemma firstn_nil : forall {A} n, firstn n nil = @nil A.
-Proof. destruct n; auto. Qed.
-
-Hint Rewrite @firstn_nil : simpl_firstn.
-
 Lemma skipn_nil : forall {A} n, skipn n nil = @nil A.
 Proof. destruct n; auto. Qed.
 
-Hint Rewrite @skipn_nil : simpl_skipn.
-
-Lemma firstn_0 : forall {A} xs, @firstn A 0 xs = nil.
-Proof. reflexivity. Qed.
-
-Hint Rewrite @firstn_0 : simpl_firstn.
+Hint Rewrite @skipn_nil : simpl_skipn push_skipn.
 
 Lemma skipn_0 : forall {A} xs, @skipn A 0 xs = xs.
 Proof. reflexivity. Qed.
 
-Hint Rewrite @skipn_0 : simpl_skipn.
-
-Lemma firstn_cons_S : forall {A} n x xs, @firstn A (S n) (x::xs) = x::@firstn A n xs.
-Proof. reflexivity. Qed.
-
-Hint Rewrite @firstn_cons_S : simpl_firstn.
+Hint Rewrite @skipn_0 : simpl_skipn push_skipn.
 
 Lemma skipn_cons_S : forall {A} n x xs, @skipn A (S n) (x::xs) = @skipn A n xs.
 Proof. reflexivity. Qed.
 
-Hint Rewrite @skipn_cons_S : simpl_skipn.
-
-Lemma firstn_app : forall {A} n (xs ys : list A),
-  firstn n (xs ++ ys) = firstn n xs ++ firstn (n - length xs) ys.
-Proof.
-  induction n, xs, ys; boring.
-Qed.
+Hint Rewrite @skipn_cons_S : simpl_skipn push_skipn.
 
 Lemma skipn_app : forall {A} n (xs ys : list A),
   skipn n (xs ++ ys) = skipn n xs ++ skipn (n - length xs) ys.
@@ -614,23 +600,43 @@ Proof.
   induction n, xs, ys; boring.
 Qed.
 
+Hint Rewrite @skipn_app : push_skipn.
+
 Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
   firstn n (xs ++ ys) = firstn n xs.
 Proof.
   induction n, xs, ys; boring; try omega.
 Qed.
 
+Hint Rewrite @firstn_app_inleft using solve [ distr_length ] : simpl_firstn push_firstn.
+
 Lemma skipn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
   skipn n (xs ++ ys) = skipn n xs ++ ys.
 Proof.
   induction n, xs, ys; boring; try omega.
 Qed.
 
+Hint Rewrite @skipn_app_inleft using solve [ distr_length ] : push_skipn.
+
+Lemma firstn_map : forall {A B} (f : A -> B) n (xs : list A), firstn n (map f xs) = map f (firstn n xs).
+Proof. induction n, xs; boring. Qed.
+
+Hint Rewrite @firstn_map : push_firstn.
+Hint Rewrite <- @firstn_map : pull_firstn.
+
+Lemma skipn_map : forall {A B} (f : A -> B) n (xs : list A), skipn n (map f xs) = map f (skipn n xs).
+Proof. induction n, xs; boring. Qed.
+
+Hint Rewrite @skipn_map : push_skipn.
+Hint Rewrite <- @skipn_map : pull_skipn.
+
 Lemma firstn_all : forall {A} n (xs:list A), n = length xs -> firstn n xs = xs.
 Proof.
   induction n, xs; boring; omega.
 Qed.
 
+Hint Rewrite @firstn_all using solve [ distr_length ] : simpl_firstn push_firstn.
+
 Lemma skipn_all : forall {T} n (xs:list T),
   (n >= length xs)%nat ->
   skipn n xs = nil.
@@ -638,6 +644,8 @@ Proof.
   induction n, xs; boring; omega.
 Qed.
 
+Hint Rewrite @skipn_all using solve [ distr_length ] : simpl_skipn push_skipn.
+
 Lemma firstn_app_sharp : forall {A} n (l l': list A),
   length l = n ->
   firstn n (l ++ l') = l.
@@ -646,6 +654,8 @@ Proof.
   rewrite firstn_app_inleft; auto using firstn_all; omega.
 Qed.
 
+Hint Rewrite @firstn_app_sharp using solve [ distr_length ] : simpl_firstn push_firstn.
+
 Lemma skipn_app_sharp : forall {A} n (l l': list A),
   length l = n ->
   skipn n (l ++ l') = l'.
@@ -654,12 +664,16 @@ Proof.
   rewrite skipn_app_inleft; try rewrite skipn_all; auto; omega.
 Qed.
 
+Hint Rewrite @skipn_app_sharp using solve [ distr_length ] : simpl_skipn push_skipn.
+
 Lemma skipn_length : forall {A} n (xs : list A),
   length (skipn n xs) = (length xs - n)%nat.
 Proof.
   induction n, xs; boring.
 Qed.
 
+Hint Rewrite @skipn_length : distr_length.
+
 Lemma fold_right_cons : forall {A B} (f:B->A->A) a b bs,
   fold_right f a (b::bs) = f b (fold_right f a bs).
 Proof.
@@ -672,6 +686,8 @@ Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs).
   reflexivity.
 Qed.
 
+Hint Rewrite @length_cons : distr_length.
+
 Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
 Proof.
   auto.
@@ -694,6 +710,9 @@ Proof.
   induction n, xs, ys; boring.
 Qed.
 
+Hint Rewrite @firstn_combine : push_firstn.
+Hint Rewrite <- @firstn_combine : pull_firstn.
+
 Lemma combine_nil_r : forall {A B} (xs:list A),
   combine xs (@nil B) = nil.
 Proof.
@@ -707,6 +726,9 @@ Proof.
   rewrite combine_nil_r; reflexivity.
 Qed.
 
+Hint Rewrite @skipn_combine : push_skipn.
+Hint Rewrite <- @skipn_combine : pull_skipn.
+
 Lemma break_list_last: forall {T} (xs:list T),
   xs = nil \/ exists xs' y, xs = xs' ++ y :: nil.
 Proof.
@@ -740,6 +762,8 @@ Proof.
   auto.
 Qed.
 
+Hint Rewrite @nil_length0 : distr_length.
+
 Lemma nth_error_Some_nth_default : forall {T} i x (l : list T), (i < length l)%nat ->
   nth_error l i = Some (nth_default x l i).
 Proof.
@@ -760,16 +784,6 @@ Proof. intros; apply update_nth_cons. Qed.
 
 Hint Rewrite @set_nth_cons : simpl_set_nth.
 
-Hint Rewrite
-  @nil_length0
-  @length_cons
-  @skipn_length
-  @length_update_nth
-  @length_set_nth
-  : distr_length.
-Ltac distr_length := autorewrite with distr_length in *;
-  try solve [simpl in *; omega].
-
 Lemma cons_update_nth : forall {T} n f (y : T) us,
   y :: update_nth n f us = update_nth (S n) f (y :: us).
 Proof.
@@ -937,6 +951,11 @@ Proof.
   induction n; destruct l; boring.
 Qed.
 
+Lemma In_skipn : forall {T} n l (x : T), In x (skipn n l) -> In x l.
+Proof.
+  induction n; destruct l; boring.
+Qed.
+
 Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat ->
   firstn n (firstn m l) = firstn n l.
 Proof.
@@ -947,6 +966,8 @@ Proof.
   apply IHm; omega.
 Qed.
 
+Hint Rewrite @firstn_firstn using omega : push_firstn.
+
 Lemma firstn_succ : forall {A} (d : A) n l, (n < length l)%nat ->
   firstn (S n) l = (firstn n l) ++ nth_default d l n :: nil.
 Proof.
@@ -958,19 +979,6 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma firstn_all_strong : forall {A} (xs : list A) n, (length xs <= n)%nat ->
-  firstn n xs = xs.
-Proof.
-  induction xs; intros; try apply firstn_nil.
-  destruct n;
-    match goal with H : (length (_ :: _)  <= _)%nat |- _ =>
-      simpl in H; try omega end.
-  simpl.
-  f_equal.
-  apply IHxs.
-  omega.
-Qed.
-
 Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs.
 Proof.
   induction n; destruct xs; simpl; try congruence; try omega; intros.
@@ -1072,8 +1080,7 @@ Lemma sum_firstn_all_succ : forall n l, (length l <= n)%nat ->
   sum_firstn l (S n) = sum_firstn l n.
 Proof.
   unfold sum_firstn; intros.
-  rewrite !firstn_all_strong by omega.
-  congruence.
+  autorewrite with push_firstn; reflexivity.
 Qed.
 
 Hint Rewrite @sum_firstn_all_succ using omega : simpl_sum_firstn.
@@ -1082,8 +1089,7 @@ Lemma sum_firstn_all : forall n l, (length l <= n)%nat ->
   sum_firstn l n = sum_firstn l (length l).
 Proof.
   unfold sum_firstn; intros.
-  rewrite !firstn_all_strong by omega.
-  congruence.
+  autorewrite with push_firstn; reflexivity.
 Qed.
 
 Hint Rewrite @sum_firstn_all using omega : simpl_sum_firstn.
@@ -1338,3 +1344,32 @@ Proof.
 Qed.
 
 Hint Rewrite repeat_length : distr_length.
+
+Lemma repeat_spec_iff : forall {A} (ls : list A) x n,
+    (length ls = n /\ forall y, In y ls -> y = x) <-> ls = repeat x n.
+Proof.
+  split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ].
+  induction ls, n; simpl; intros; intuition try congruence.
+  f_equal; auto.
+Qed.
+
+Lemma repeat_spec_eq : forall {A} (ls : list A) x n,
+    length ls = n
+    -> (forall y, In y ls -> y = x)
+    -> ls = repeat x n.
+Proof.
+  intros; apply repeat_spec_iff; auto.
+Qed.
+
+Lemma tl_repeat {A} x n : tl (@repeat A x n) = repeat x (pred n).
+Proof. destruct n; reflexivity. Qed.
+
+Lemma firstn_repeat : forall {A} x n k, firstn k (@repeat A x n) = repeat x (min k n).
+Proof. induction n, k; boring. Qed.
+
+Hint Rewrite @firstn_repeat : push_firstn.
+
+Lemma skipn_repeat : forall {A} x n k, skipn k (@repeat A x n) = repeat x (n - k).
+Proof. induction n, k; boring. Qed.
+
+Hint Rewrite @skipn_repeat : push_skipn.