From f5b35696b789fdd427823eefecad2eb5428e70bf Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 9 Nov 2015 13:05:05 -0500 Subject: ModularBaseSystem: finished most admits for addition and multiplication, moved some lemmas to ListUtil. --- src/Util/ListUtil.v | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 229fb7488..626a33f02 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -204,15 +204,21 @@ Proof. destruct n; auto. Qed. -Lemma firstn_app : forall A (l l': list A), firstn (length l) (l ++ l') = l. +Lemma firstn_app : forall {A} n (xs ys : list A), (n <= length xs)%nat -> + firstn n xs = firstn n (xs ++ ys). Proof. - intros. - induction l; simpl; auto. - f_equal; auto. + induction n; destruct xs; destruct ys; simpl_list; boring; try omega. + rewrite (IHn xs (a0 :: ys)) by omega; auto. Qed. - + Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'. Proof. intros. induction l; simpl; auto. Qed. + +Lemma skipn_length : forall {A} n (xs : list A), + length (skipn n xs) = (length xs - n)%nat. +Proof. +induction n; destruct xs; boring. +Qed. -- cgit v1.2.3