diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 5a3f304a7..4d807c779 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -136,8 +136,37 @@ Proof. injection HA; intros; subst; auto. Qed. -Lemma combine_truncate : forall {A} (xs ys : list A), +Lemma combine_truncate_r : forall {A} (xs ys : list A), 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), + combine xs ys = combine (firstn (length ys) xs) ys. +Proof. + induction xs; destruct ys; boring. +Qed. + +Lemma firstn_nil : forall {A} n, firstn n nil = @nil A. +Proof. + destruct n; auto. +Qed. + +Lemma skipn_nil : forall {A} n, skipn n nil = @nil A. +Proof. + destruct n; auto. +Qed. + +Lemma firstn_app : forall A (l l': list A), firstn (length l) (l ++ l') = l. +Proof. + intros. + induction l; simpl; auto. + f_equal; auto. +Qed. + +Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'. +Proof. + intros. + induction l; simpl; auto. +Qed. |