Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.

1 files changed, 152 insertions, 1 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 0426c0834..ed20cd15c 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -3,6 +3,17 @@ Require Import Coq.omega.Omega.
 Require Import Coq.Arith.Peano_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 
+Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).
+
+Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C :=
+  match la with
+  | nil => nil
+  | a :: la' => match lb with
+                | nil => nil
+                | b :: lb' => f a b :: map2 f la' lb'
+                end
+  end.
+
 Ltac boring :=
   simpl; intuition;
   repeat match goal with
@@ -624,4 +635,144 @@ Proof.
   induction n; (destruct l; [intros; simpl in *; omega | ]); simpl;
     destruct i; break_if; try omega; intros; try apply nth_default_cons;
     rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d,
+  (forall x, In x l -> P x) -> P d -> P (nth_default d l n).
+Proof.
+  intros; rewrite nth_default_eq.
+  destruct (nth_in_or_default n l d); auto.
+  congruence.
+Qed.
+
+Lemma nth_error_first : forall {T} (a b : T) l,
+  nth_error (a :: l) 0 = Some b -> a = b.
+Proof.
+  intros; simpl in *.
+  unfold value in *.
+  congruence.
+Qed.
+
+Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x),
+  exists l', l = x :: l'.
+Proof.
+  induction l; try discriminate; eexists.
+  apply nth_error_first in H.
+  subst; eauto.
+Qed.
+
+Lemma list_elementwise_eq : forall {T} (l1 l2 : list T),
+  (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2.
+Proof.
+  induction l1, l2; intros; try reflexivity;
+    pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst.
+  f_equal.
+  apply IHl1.
+  intros i; specialize (H (S i)).
+  boring.
+Qed.
+
+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.
+Qed.
+
+Lemma sum_firstn_succ : forall l i x,
+  nth_error l i = Some x ->
+  sum_firstn l (S i) = (x + sum_firstn l i)%Z.
+Proof.
+  unfold sum_firstn; induction l;
+    [intros; rewrite (@nth_error_nil_error Z) in *; congruence | ].
+  intros ? x nth_err_x; destruct (NPeano.Nat.eq_dec i 0).
+  + subst; simpl in *; unfold value in *.
+    congruence.
+  + rewrite <- (NPeano.Nat.succ_pred i) at 2 by auto.
+    rewrite <- (NPeano.Nat.succ_pred i) in nth_err_x by auto.
+    simpl. simpl in nth_err_x.
+    specialize (IHl (pred i) x).
+    rewrite NPeano.Nat.succ_pred in IHl by auto.
+    destruct (NPeano.Nat.eq_dec (pred i) 0).
+    - replace i with 1%nat in * by omega.
+      simpl. replace (pred 1) with 0%nat in * by auto.
+      apply nth_error_exists_first in nth_err_x.
+      destruct nth_err_x as [l' ?].
+      subst; simpl; omega.
+    - rewrite IHl by auto; omega.
+Qed.
+
+Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
+  nth_default d (map2 f ls1 ls2) i =
+    if lt_dec i (min (length ls1) (length ls2))
+    then f (nth_default d1 ls1 i) (nth_default d2 ls2 i)
+    else d.
+Proof.
+  induction ls1, ls2.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + simpl.
+    destruct i.
+    - intros. rewrite !nth_default_cons.
+      break_if; auto; omega.
+    - intros. rewrite !nth_default_cons_S.
+      rewrite IHls1 with (d1 := d1) (d2 := d2).
+      repeat break_if; auto; omega.
+Qed.
+
+Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b,
+  map2 f (a :: ls1) (b :: ls2) = f a b :: map2 f ls1 ls2.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map2_nil_l : forall A B C (f : A -> B -> C) ls2,
+  map2 f nil ls2 = nil.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map2_nil_r : forall A B C (f : A -> B -> C) ls1,
+  map2 f ls1 nil = nil.
+Proof.
+  destruct ls1; reflexivity.
+Qed.
+Local Hint Resolve map2_nil_r map2_nil_l.
+
+Opaque map2.
+
+Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2,
+  length (map2 f ls1 ls2) = min (length ls1) (length ls2).
+Proof.
+  induction ls1, ls2; intros; try solve [cbv; auto].
+  rewrite map2_cons, !length_cons, IHls1.
+  auto.
+Qed.
+
+Ltac simpl_list_lengths := repeat match goal with
+  | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H
+  | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H
+  | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A)
+  | |- appcontext[length (_ :: _)] => rewrite length_cons
+  end.
+
+Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2',
+  (length ls1 = length ls2) ->
+  map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'.
+Proof.
+  induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence;
+    simpl_list_lengths; try omega.
+  rewrite <-!app_comm_cons, !map2_cons.
+  rewrite IHls1; auto.
+Qed.