From 33193a5fb30b39d794d4c77f2229145e90130410 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 5 Nov 2015 22:54:39 -0500 Subject: Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. --- src/Util/ListUtil.v | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) (limited to 'src/Util/ListUtil.v') 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. -- cgit v1.2.3