fin_collections.v 7.71 KB
Newer Older
1
2
3
4
5
(* Copyright (c) 2012, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
9
Require Import Permutation.
Require Export collections listset.

Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
10
11
Definition collection_fold `{Elements A C} {B} (f : A  B  B)
  (b : B) (X : C) : B := fold_right f b (elements X).
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
17
18

Section fin_collection.
Context `{FinCollection A C}.

Global Instance elements_proper: Proper (() ==> Permutation) elements.
Proof.
  intros ?? E. apply NoDup_Permutation.
19
20
21
  * apply elements_nodup.
  * apply elements_nodup.
  * intros. now rewrite <-!elements_spec, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
Qed.
Global Instance collection_size_proper: Proper (() ==> (=)) size.
Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.

Lemma size_empty : size  = 0.
Proof.
  unfold size, collection_size. rewrite (in_nil_inv (elements )).
29
  * easy.
30
  * intro. rewrite <-elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
37
38
39
Qed.
Lemma size_empty_inv X : size X = 0  X  .
Proof.
  intros. apply equiv_empty. intro. rewrite elements_spec.
  rewrite (nil_length (elements X)); intuition.
Qed.
Lemma size_empty_iff X : size X = 0  X  .
Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.

40
Lemma size_singleton x : size {[ x ]} = 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Proof.
42
  change (length (elements {[ x ]}) = length [x]).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  apply Permutation_length, NoDup_Permutation.
44
45
  * apply elements_nodup.
  * apply NoDup_singleton.
46
  * intros. rewrite <-elements_spec. esolve_elem_of firstorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
Qed.
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
  unfold size, collection_size. rewrite !elements_spec.
  generalize (elements X). intros [|? l].
52
53
54
  * discriminate.
  * injection 1. intro. rewrite (nil_length l) by easy.
    simpl. intuition congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
58
Qed.

Lemma choose X : X    { x | x  X }.
Proof.
59
60
  destruct (elements X) as [|x l] eqn:E.
  * intros []. apply equiv_empty.
61
    intros x. rewrite elements_spec, E. contradiction.
62
  * exists x. rewrite elements_spec, E. now left.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
Qed.
Lemma size_pos_choose X : 0 < size X  { x | x  X }.
65
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  intros E. apply choose.
67
68
  intros E2. rewrite E2, size_empty in E.
  now destruct (Lt.lt_n_0 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70
Lemma size_1_choose X : size X = 1  { x | X  {[ x ]} }.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
Proof.
  intros E. destruct (size_pos_choose X).
73
  * rewrite E. auto with arith.
74
75
76
  * exists x. apply elem_of_equiv. split.
    + intro. rewrite elem_of_singleton. eauto using size_singleton_inv.
    + solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
Qed.

79
80
Program Instance collection_car_eq_dec_slow (x y : A) :
    Decision (x = y) | 100 :=
81
  match Compare_dec.zerop (size ({[ x ]}  {[ y ]})) with
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
84
85
86
  | left _ => right _
  | right _ => left _
  end.
Next Obligation.
  intro. apply empty_ne_singleton with x.
87
88
  transitivity ({[ x ]}  {[ y ]}).
  * symmetry. now apply size_empty_iff.
89
  * solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
91
Next Obligation. edestruct size_pos_choose; esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95
96
97
98

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100 :=
  match decide_rel In x (elements X) with
  | left Hx => left (proj2 (elements_spec _ _) Hx)
  | right Hx => right (Hx  proj1 (elements_spec _ _))
  end.

99
Lemma union_difference X Y : X  Y  X  X  Y.
100
Proof. split; intros x; destruct (decide (x  X)); solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
103
104
105

Lemma size_union X Y : X  Y    size (X  Y) = size X + size Y.
Proof.
  intros [E _]. unfold size, collection_size. rewrite <-app_length.
  apply Permutation_length, NoDup_Permutation.
106
107
108
109
  * apply elements_nodup.
  * apply NoDup_app; try apply elements_nodup.
    intros x. rewrite <-!elements_spec. esolve_elem_of.
  * intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
112
113
114
Proof.
  rewrite <-size_union. now rewrite union_difference. solve_elem_of.
Qed.
115
Lemma size_add X x : x  X  size ({[ x ]}  X) = S (size X).
116
117
118
Proof.
  intros. rewrite size_union. now rewrite size_singleton. solve_elem_of.
Qed.
119
Lemma size_difference X Y : X  Y  size X + size (Y  X) = size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof. intros. now rewrite <-size_union_alt, subseteq_union_1. Qed.
121
Lemma size_remove X x : x  X  S (size (X  {[ x ]})) = size X.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof.
123
124
  intros. rewrite <-(size_difference {[ x ]} X).
  * rewrite size_singleton. auto with arith.
125
  * solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
128
Qed.

Lemma subseteq_size X Y : X  Y  size X  size Y.
129
130
Proof.
  intros. rewrite <-(subseteq_union_1 X Y) by easy.
131
  rewrite <-(union_difference X Y), size_union by solve_elem_of.
132
  auto with arith.
133
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135

Lemma collection_wf_ind (P : C  Prop) :
136
137
  ( X, ( Y, size Y < size X  P Y)  P X) 
   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Proof.
139
140
141
142
143
  intros Hind. cut ( n X, size X < n  P X).
  { intros help X. apply help with (S (size X)). auto with arith. }
  induction n; intros.
  * now destruct (Lt.lt_n_0 (size X)).
  * apply Hind. intros. apply IHn. eauto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
146
Qed.

Lemma collection_ind (P : C  Prop) :
147
148
149
150
  Proper (() ==> iff) P 
  P  
  ( x X, x  X  P X  P ({[ x ]}  X)) 
   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
Proof.
  intros ? Hemp Hadd. apply collection_wf_ind.
  intros X IH. destruct (Compare_dec.zerop (size X)).
154
155
  * now rewrite size_empty_inv.
  * destruct (size_pos_choose X); auto.
156
    rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
157
    rewrite <-union_difference.
158
    apply Hadd; [solve_elem_of |]. apply IH.
159
    rewrite <-(size_remove X x); auto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
163
Qed.

Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
164
165
166
  P b  
  ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
   X, P (collection_fold f b X) X.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
Proof.
  intros ? Hemp Hadd.
169
170
171
172
173
  cut ( l, NoDup l   X, ( x, x  X  In x l)  P (fold_right f b l) X).
  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
  induction 1 as [|x l ?? IHl]; simpl.
  * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
  * intros X HX.
174
    rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
175
    rewrite <-union_difference.
176
    apply Hadd. solve_elem_of. apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
    intros y. split.
178
179
    + intros. destruct (proj1 (HX y)); solve_elem_of.
    + esolve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
Qed.

Lemma collection_fold_proper {B} (f : A  B  B) (b : B) :
183
184
185
  ( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) 
  Proper (() ==> (=)) (collection_fold f b).
Proof. intros ??? E. apply fold_right_permutation. auto. now rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186

187
188
Global Program Instance cforall_dec `(P : A  Prop)
    `{ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
191
192
  match decide (Forall P (elements X)) with
  | left Hall => left _
  | right Hall => right _
  end.
193
194
Next Obligation.
  red. setoid_rewrite elements_spec. now apply Forall_forall.
195
Qed.
196
197
198
Next Obligation.
  intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199

200
201
Global Program Instance cexists_dec `(P : A  Prop)
    `{ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
205
  match decide (Exists P (elements X)) with
  | left Hex => left _
  | right Hex => right _
  end.
206
Next Obligation.
207
208
  red. setoid_rewrite elements_spec. now apply Exists_exists.
Qed.
209
210
211
Next Obligation.
  intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212

213
214
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
  Decision (elem_of_upto R x X) | 100 := decide (cexists (R x) X).
215
216
217
218
219

Lemma not_elem_of_intersection x X Y : x  X  Y  x  X  x  Y.
Proof. destruct (decide (x  X)); solve_elem_of. Qed.
Lemma not_elem_of_difference x X Y : x  X  Y  x  X  x  Y.
Proof. destruct (decide (x  Y)); solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
End fin_collection.