forked from mit-plv/fiat
-
Notifications
You must be signed in to change notification settings - Fork 0
/
FlattenList.v
115 lines (98 loc) · 2.98 KB
/
FlattenList.v
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
113
114
115
Require Import Coq.Lists.List Coq.Lists.SetoidList Fiat.Common.
Require Import Coq.Arith.Arith.
Unset Implicit Arguments.
Section FlattenList.
Definition flatten {A} seq := List.fold_right (@app A) [] seq.
Lemma flat_map_flatten :
forall {A B: Type},
forall comp seq,
@flat_map A B comp seq = flatten (map comp seq).
Proof.
intros; induction seq; simpl; try rewrite IHseq; reflexivity.
Qed.
Lemma in_flatten_iff :
forall {A} x seqs,
@List.In A x (flatten seqs) <->
exists seq, List.In x seq /\ List.In seq seqs.
Proof.
intros; unfold flatten.
induction seqs; simpl.
firstorder.
rewrite in_app_iff.
rewrite IHseqs.
split.
intros [ in_head | [seq (in_seqs & in_seq) ] ]; eauto.
intros [ seq ( in_seq & [ eq_head | in_seqs ] ) ]; subst; eauto.
Qed.
Lemma flatten_filter :
forall {A} (seq: list (list A)) pred,
List.filter pred (flatten seq) =
flatten (List.map (List.filter pred) seq).
Proof.
intros; induction seq; trivial.
unfold flatten; simpl.
induction a; trivial.
simpl;
destruct (pred a); simpl; rewrite IHa; trivial.
Qed.
Lemma map_flatten :
forall {B C} (f: B -> C) (xs: list (list B)),
map f (flatten xs) = flatten (map (fun x => map f x) xs).
Proof.
induction xs; simpl;
[ | rewrite map_app, IHxs ]; reflexivity.
Qed.
Lemma map_flat_map :
forall {A B C} (f: B -> C) (g: A -> list B) (xs: list A),
map f (flat_map g xs) = flat_map (fun x : A => map f (g x)) xs.
Proof.
intros;
rewrite flat_map_flatten, map_flatten, map_map, <- flat_map_flatten;
reflexivity.
Qed.
Lemma flatten_nils :
forall {A} (seq: list (list A)),
flatten (List.map (fun _ => []) seq) = @nil A.
Proof.
induction seq; intuition.
Qed.
Lemma flatten_app :
forall {A} (seq1 seq2: list (list A)),
flatten (seq1 ++ seq2) = flatten seq1 ++ flatten seq2.
Proof.
unfold flatten; induction seq1; simpl; trivial.
intros; rewrite IHseq1; rewrite app_assoc; trivial.
Qed.
Lemma flatten_head :
forall {A} head tail,
@flatten A (head :: tail) = head ++ flatten tail.
Proof.
intuition.
Qed.
Lemma length_flatten_aux :
forall {A} seq,
forall n,
n + List.length (flatten seq) = List.fold_right (compose plus (@List.length A)) n seq.
Proof.
induction seq; simpl; intros.
- auto with arith.
- unfold compose;
rewrite app_length, <- IHseq.
rewrite Nat.add_comm, <- Nat.add_assoc; auto with arith.
Qed.
Lemma length_flatten :
forall {A} seq,
List.length (flatten seq) = List.fold_right (compose plus (@List.length A)) 0 seq.
Proof.
intros.
pose proof (length_flatten_aux seq 0) as H; simpl in H; eauto.
Qed.
Lemma filter_flat_map :
forall {A B} g (f: B -> bool) xs,
filter f (flat_map g xs) =
flat_map (fun x : A => filter f (g x)) xs.
Proof.
intros; rewrite !flat_map_flatten.
rewrite flatten_filter, map_map; reflexivity.
Qed.
End FlattenList.