diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-14 22:33:44 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-14 22:33:44 -0400 |
| commit | 2c2ac41de0bedabc3b8fd53d28f8b65859eb4287 (patch) | |
| tree | f216a5e289d810a29bc7fc22c489d1abafd3277e /src/Util/ListUtil.v | |
| parent | 44b5603cae95f9ed42fc29b01ebf5d917da4ecd5 (diff) | |
Fix a name clash
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 902d4cb7e..df355d202 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -782,16 +782,16 @@ Lemma skipn_firstn {A} (ls : list A) n m Proof. revert n m; induction ls, m, n; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list. Qed. -Lemma firstn_skipn {A} (ls : list A) n m +Lemma firstn_skipn_add {A} (ls : list A) n m : firstn n (skipn m ls) = skipn m (firstn (m + n) ls). Proof. revert n m; induction ls, m; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list. Qed. -Lemma firstn_skipn' {A} (ls : list A) n m +Lemma firstn_skipn_add' {A} (ls : list A) n m : firstn n (skipn m ls) = skipn m (firstn (n + m) ls). -Proof. rewrite firstn_skipn; do 2 f_equal; auto with arith. Qed. -Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_firstn. -Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_skipn. +Proof. rewrite firstn_skipn_add; do 2 f_equal; auto with arith. Qed. +Hint Rewrite <- @firstn_skipn_add @firstn_skipn_add' : simpl_firstn. +Hint Rewrite <- @firstn_skipn_add @firstn_skipn_add' : simpl_skipn. Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat -> firstn n (xs ++ ys) = firstn n xs. |