diff options
| author | Olivier Laurent | 2019-10-30 12:53:05 +0100 |
|---|---|---|
| committer | Olivier Laurent | 2019-12-06 14:34:30 +0100 |
| commit | 53231ac0ee2e91b01b64ab6d5b1c17cab2f36eaf (patch) | |
| tree | 23b8b0d303d14d503152fdefb47e1fb1f9d8e01c | |
| parent | dff979d31a18dcf892fac75cd8a1e608adaefb9e (diff) | |
redundancy between skipn_node and skipn_all
| -rw-r--r-- | theories/Lists/List.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 38723e291f..f608458f45 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1825,9 +1825,11 @@ Section Cutting. Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. Proof. reflexivity. Qed. - Lemma skipn_none : forall l, skipn (length l) l = []. + Lemma skipn_all : forall l, skipn (length l) l = nil. Proof. now induction l. Qed. +#[deprecated(since="8.11",note="Use skipn_all instead.")] Notation skipn_none := skipn_all. + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. Proof. intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. @@ -1855,9 +1857,6 @@ Section Cutting. - destruct l; simpl; auto. Qed. - Lemma skipn_all l: skipn (length l) l = nil. - Proof. now induction l. Qed. - Lemma skipn_app n : forall l1 l2, skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). Proof. induction n; auto; intros [|]; simpl; auto. Qed. @@ -1884,7 +1883,7 @@ Section Cutting. intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. - now rewrite L, Nat.sub_0_r, skipn_none. + now rewrite L, Nat.sub_0_r, skipn_all. - replace (length (rev l) - (length (rev l) - x)) with (length (rev l) + x - length (rev l)). rewrite minus_plus. reflexivity. |