diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index df355d202..517ab1850 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1152,8 +1152,8 @@ 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. +Lemma firstn_firstn_min : forall {A} m n (l : list A), + firstn n (firstn m l) = firstn (min n m) l. Proof. induction m; destruct n; intros; try omega; auto. destruct l; auto. @@ -1162,6 +1162,14 @@ Proof. apply IHm; omega. Qed. +Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat -> + firstn n (firstn m l) = firstn n l. +Proof. + intros; rewrite firstn_firstn_min. + apply Min.min_case_strong; intro; [ reflexivity | ]. + assert (n = m) by omega; subst; reflexivity. +Qed. + Hint Rewrite @firstn_firstn using omega : push_firstn. Lemma firstn_succ : forall {A} (d : A) n l, (n < length l)%nat -> |