blob: d28124c7ad0ee3c04972ee093e4d30289d952057 (
plain)
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
Require Import Coqlib.
Require Import Lia.
(** TODO: are these def and lemma already defined in the standard library ?
In this case, it should be better to reuse those of the standard library !
*)
Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A :=
match n with
| O => x
| S n0 => iter n0 f (f x)
end.
Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x).
Proof.
induction n; simpl; auto.
intros; erewrite <- IHn; simpl; auto.
Qed.
Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x).
Proof.
induction n; simpl; auto.
Qed.
Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l.
Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l).
Proof.
apply iter_S.
Qed.
Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l).
Proof.
apply iter_plus.
Qed.
Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2.
Proof.
induction l1; auto.
Qed.
Lemma iter_tail_nil A n: @iter_tail A n nil = nil.
Proof.
unfold iter_tail; induction n; simpl; auto.
Qed.
Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil.
Proof.
rewrite (app_nil_end l) at 2.
rewrite iter_tail_length.
auto.
Qed.
Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
Proof.
unfold iter_tail; induction n; auto.
intros l; destruct l. { simpl; lia. }
intros; simpl. erewrite IHn; eauto.
simpl in *; lia.
Qed.
Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
Proof.
unfold iter_tail; induction n; simpl.
- intros l; destruct l; simpl; lia || eauto.
- intros l H; destruct (IHn (tl l)) as (x & H1).
+ destruct l; simpl in *; try lia.
+ rewrite H1; eauto.
Qed.
Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2.
Proof.
intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
rewrite EQ.
rewrite (length_iter_tail n2 l); eauto.
lia.
Qed.
Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
Proof.
destruct (le_lt_dec n (List.length l)); try lia.
intros; exploit (iter_tail_inject1 n (length l) l); try lia.
rewrite iter_tail_reach_nil. auto.
Qed.
Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l).
Proof.
induction l; auto.
rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. lia.
Qed.
Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l).
Proof.
intros; rewrite list_length_z_nat, Nat2Z.id. auto.
Qed.
Lemma is_tail_list_nth_z A (l1 l2: list A):
is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
Proof.
induction 1; simpl.
- replace (list_length_z c - list_length_z c) with 0; lia || auto.
- assert (X: list_length_z (i :: c2) > list_length_z c1).
{ rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
exploit is_tail_bound; simpl; eauto.
lia. }
destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try lia.
replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
rewrite list_length_z_cons.
lia.
Qed.
|
