From 2c813835518ce6c67c524355977ea22b77438e40 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Mar 2017 14:20:50 -0400 Subject: Add In_firstn_skipn_split --- src/Util/ListUtil.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 517ab1850..9c5514ccc 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1152,6 +1152,16 @@ Proof. induction n; destruct l; boring. Qed. +Lemma In_firstn_skipn_split {T} n (x : T) + : forall l, In x l -> In x (firstn n l) \/ In x (skipn n l). +Proof. + induction n; destruct l; boring. + match goal with + | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ] + => destruct (IH _ H') + end; auto. +Qed. + Lemma firstn_firstn_min : forall {A} m n (l : list A), firstn n (firstn m l) = firstn (min n m) l. Proof. -- cgit v1.2.3