1 files changed, 53 insertions, 10 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 36d8a3ad3..0426c0834 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -18,7 +18,7 @@ Proof.
 intros. induction n; boring.
 Qed.
 
-Ltac nth_tac' := 
+Ltac nth_tac' :=
   intros; simpl in *; unfold error,value in *; repeat progress (match goal with
     | [  |- context[nth_error nil ?n] ] => rewrite nth_error_nil_error
     | [ H: ?x = Some _  |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x
@@ -79,10 +79,10 @@ Proof.
   reflexivity.
   nth_tac'.
   pose proof (nth_error_error_length A n l H0).
-  omega.  
+  omega.
 Qed.
 
-Ltac nth_tac := 
+Ltac nth_tac :=
   repeat progress (try nth_tac'; try (match goal with
     | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H
     | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H
@@ -191,7 +191,7 @@ Proof.
 Qed.
 
 Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
-  set_nth n x xs = 
+  set_nth n x xs =
   if lt_dec n (length xs)
   then splice_nth n x xs
   else xs.
@@ -210,7 +210,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
     end.
 Proof.
   (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypotheses at once *)
-  induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac; 
+  induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac;
     try (f_equal; specialize (IHn x xs ys ); rewrite H in IHn; rewrite <- IHn);
     try (specialize (nth_error_value_length _ _ _ _ H); omega).
   assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto).
@@ -258,13 +258,13 @@ Proof.
   destruct (lt_dec n (length xs)); auto.
 Qed.
 
-Lemma combine_truncate_r : forall {A} (xs ys : list A),
+Lemma combine_truncate_r : forall {A B} (xs : list A) (ys : list B),
   combine xs ys = combine xs (firstn (length xs) ys).
 Proof.
   induction xs; destruct ys; boring.
 Qed.
 
-Lemma combine_truncate_l : forall {A} (xs ys : list A),
+Lemma combine_truncate_l : forall {A B} (xs : list A) (ys : list B),
   combine xs ys = combine (firstn (length ys) xs) ys.
 Proof.
   induction xs; destruct ys; boring.
@@ -330,7 +330,7 @@ Proof.
   intros.
   rewrite firstn_app_inleft; auto using firstn_all; omega.
 Qed.
-    
+
 Lemma skipn_app_sharp : forall {A} n (l l': list A),
   length l = n ->
   skipn n (l ++ l') = l'.
@@ -422,7 +422,7 @@ Proof.
     right; repeat eexists; auto.
   }
 Qed.
- 
+
 Lemma nil_length0 : forall {T}, length (@nil T) = 0%nat.
 Proof.
   auto.
@@ -512,7 +512,7 @@ Ltac nth_error_inbounds :=
   match goal with
   | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
     case_eq (nth_error xs i);
-    match goal with 
+    match goal with
       | [ |- forall _, nth_error xs i = Some _ -> _ ] =>
           let x := fresh "x" in
           let H := fresh "H" in
@@ -582,3 +582,46 @@ Lemma In_firstn : forall {T} n l (x : T), In x (firstn 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.
+  induction m; destruct n; intros; try omega; auto.
+  destruct l; auto.
+  simpl.
+  f_equal.
+  apply IHm; omega.
+Qed.
+
+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.
+  induction n; destruct l; rewrite ?(@nil_length0 A); intros; try omega.
+  + rewrite nth_default_cons; auto.
+  + simpl.
+    rewrite nth_default_cons_S.
+    rewrite <-IHn by (rewrite cons_length in *; omega).
+    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 set_nth_nth_default : forall {A} (d:A) n x l i, (0 <= i < length l)%nat ->
+  nth_default d (set_nth n x l) i =
+  if (eq_nat_dec i n) then x else nth_default d l i.
+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