1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
From Coq.Lists Require Import List.
From Coq.ZArith Require Import ZArith.
From Coq.micromega Require Import Lia.
(** For backwards compatibility with hint locality attributes. *)
Set Warnings "-unsupported-attributes".
Lemma firstn_app_L : forall T n (a b : list T),
n <= length a ->
firstn n (a ++ b) = firstn n a.
Proof.
induction n; destruct a; simpl in *; intros; auto.
exfalso; lia.
f_equal. eapply IHn; eauto. lia.
Qed.
Lemma firstn_app_R : forall T n (a b : list T),
length a <= n ->
firstn n (a ++ b) = a ++ firstn (n - length a) b.
Proof.
induction n; destruct a; simpl in *; intros; auto.
exfalso; lia.
f_equal. eapply IHn; eauto. lia.
Qed.
Lemma firstn_all : forall T n (a : list T),
length a <= n ->
firstn n a = a.
Proof.
induction n; destruct a; simpl; intros; auto.
exfalso; lia.
simpl. f_equal. eapply IHn; lia.
Qed.
Lemma firstn_0 : forall T n (a : list T),
n = 0 ->
firstn n a = nil.
Proof.
intros; subst; auto.
Qed.
Lemma firstn_cons : forall T n a (b : list T),
0 < n ->
firstn n (a :: b) = a :: firstn (n - 1) b.
Proof.
destruct n; intros.
lia.
simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
Qed.
#[global]
Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using lia : list_rw.
Lemma skipn_app_R : forall T n (a b : list T),
length a <= n ->
skipn n (a ++ b) = skipn (n - length a) b.
Proof.
induction n; destruct a; simpl in *; intros; auto.
exfalso; lia.
eapply IHn. lia.
Qed.
Lemma skipn_app_L : forall T n (a b : list T),
n <= length a ->
skipn n (a ++ b) = (skipn n a) ++ b.
Proof.
induction n; destruct a; simpl in *; intros; auto.
exfalso; lia.
eapply IHn. lia.
Qed.
Lemma skipn_0 : forall T n (a : list T),
n = 0 ->
skipn n a = a.
Proof.
intros; subst; auto.
Qed.
Lemma skipn_all : forall T n (a : list T),
length a <= n ->
skipn n a = nil.
Proof.
induction n; destruct a; simpl in *; intros; auto.
exfalso; lia.
apply IHn; lia.
Qed.
Lemma skipn_cons : forall T n a (b : list T),
0 < n ->
skipn n (a :: b) = skipn (n - 1) b.
Proof.
destruct n; intros.
lia.
simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
Qed.
#[global]
Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.
|
