diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-19 12:09:42 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-19 12:09:42 -0400 |
| commit | 7dcfc8c1955aa1a75d08bf6f6e45dd274355b743 (patch) | |
| tree | decac634824a6745b16e4a35ba53c12512396266 /src/Util/ListUtil.v | |
| parent | a1d8da5d4e012c56c3ef69ef177f5dfe15f0f32e (diff) | |
Add firstn_firstn_min
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 -> |