fin_collections.v 7.52 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
Require Import Permutation.
7
Require Export collections numbers listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
10
11
Instance collection_size `{Elements A C} : Size C := length  elements.
Definition collection_fold `{Elements A C} {B}
  (f : A  B  B) (b : B) : C  B := foldr f b  elements.
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
  * apply elements_nodup.
  * apply elements_nodup.
21
  * intros. by rewrite <-!elements_spec, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
Qed.
Global Instance collection_size_proper: Proper (() ==> (=)) size.
24
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
25

26
Lemma size_empty : size ( : C) = 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Proof.
28
29
  unfold size, collection_size. simpl.
  rewrite (elem_of_nil_inv (elements )).
30
  * done.
31
  * intro. rewrite <-elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Qed.
33
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
Proof.
  intros. apply equiv_empty. intro. rewrite elements_spec.
36
  rewrite (nil_length (elements X)). by rewrite elem_of_nil. done.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Qed.
38
Lemma size_empty_iff (X : C) : size X = 0  X  .
39
Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

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

59
Lemma elem_of_or_empty X : ( x, x  X)  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof.
61
62
  destruct (elements X) as [|x xs] eqn:E.
  * right. apply equiv_empty. intros x Ex.
63
    by rewrite elements_spec, E, elem_of_nil in Ex.
64
65
  * left. exists x. rewrite elements_spec, E.
    by constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Qed.
67
68
69
70
71
72
73
74

Lemma choose X : X     x, x  X.
Proof.
  destruct (elem_of_or_empty X) as [[x ?]|?].
  * by exists x.
  * done.
Qed.
Lemma size_pos_choose X : 0 < size X   x, x  X.
75
Proof.
76
77
78
  intros E1. apply choose.
  intros E2. rewrite E2, size_empty in E1.
  by apply (Lt.lt_n_0 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80
Lemma size_1_choose X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Proof.
  intros E. destruct (size_pos_choose X).
83
  * rewrite E. auto with arith.
84
  * exists x. apply elem_of_equiv. split.
85
86
    + intro. rewrite elem_of_singleton.
      eauto using size_singleton_inv.
87
    + solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
Qed.

Lemma size_union X Y : X  Y    size (X  Y) = size X + size Y.
Proof.
92
  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  apply Permutation_length, NoDup_Permutation.
94
  * apply elements_nodup.
95
  * apply NoDup_app; repeat split; try apply elements_nodup.
96
    intros x. rewrite <-!elements_spec. esolve_elem_of.
97
  * intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
99
100
101

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
102
  refine (cast_if (decide_rel () x (elements X)));
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
    by rewrite (elements_spec _).
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
    Decision (X  Y) | 100 :=
  match decide_rel (=) (size (X  Y)) 0 with
  | left E1 => left _
  | right E1 => right _
  end.
Next Obligation.
  intros x Ex; apply dec_stable; intro.
  destruct (proj1 (elem_of_empty x)).
  apply (size_empty_inv _ E1).
  by rewrite elem_of_difference.
Qed.
Next Obligation.
  intros E2. destruct E1.
  apply size_empty_iff, equiv_empty. intros x.
  rewrite elem_of_difference. intros [E3 ?].
  by apply E2 in E3.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
124
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
125
Proof.
126
  rewrite <-size_union. by rewrite union_difference. solve_elem_of.
127
Qed.
128
Lemma size_add X x : x  X  size ({[ x ]}  X) = S (size X).
129
Proof.
130
  intros. rewrite size_union. by rewrite size_singleton. solve_elem_of.
131
Qed.
132

133
Lemma size_difference X Y : X  Y  size X + size (Y  X) = size Y.
134
Proof. intros. by rewrite <-size_union_alt, subseteq_union_1. Qed.
135
Lemma size_remove X x : x  X  S (size (X  {[ x ]})) = size X.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
137
138
  intros. rewrite <-(size_difference {[ x ]} X).
  * rewrite size_singleton. auto with arith.
139
  * solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
Qed.

Lemma subseteq_size X Y : X  Y  size X  size Y.
143
Proof.
144
  intros. rewrite <-(subseteq_union_1 X Y) by done.
145
  rewrite <-(union_difference X Y), size_union by solve_elem_of.
146
  auto with arith.
147
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149

Lemma collection_wf_ind (P : C  Prop) :
150
151
  ( X, ( Y, size Y < size X  P Y)  P X) 
   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
153
154
155
  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.
156
  * by destruct (Lt.lt_n_0 (size X)).
157
  * apply Hind. intros. apply IHn. eauto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
Qed.

Lemma collection_ind (P : C  Prop) :
161
162
163
164
  Proper (() ==> iff) P 
  P  
  ( x X, x  X  P X  P ({[ x ]}  X)) 
   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
Proof.
  intros ? Hemp Hadd. apply collection_wf_ind.
  intros X IH. destruct (Compare_dec.zerop (size X)).
168
  * by rewrite size_empty_inv.
169
  * destruct (size_pos_choose X); auto.
170
    rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
171
    rewrite <-union_difference.
172
    apply Hadd; [solve_elem_of |]. apply IH.
173
    rewrite <-(size_remove X x); auto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
176
177
Qed.

Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
178
179
180
  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
181
182
Proof.
  intros ? Hemp Hadd.
183
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
184
  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
185
186
187
188
  induction 1 as [|x l ?? IHl].
  * intros X HX. setoid_rewrite elem_of_nil in HX.
    rewrite equiv_empty; firstorder.
  * intros X HX. setoid_rewrite elem_of_cons in HX.
189
    rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
190
    rewrite <-union_difference.
191
    apply Hadd. solve_elem_of. apply IHl.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
    intros y. split.
193
194
    + intros. destruct (proj1 (HX y)); solve_elem_of.
    + esolve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
Qed.

197
198
199
200
201
202
203
204
205
206
207
Lemma collection_fold_proper {B} (R : relation B)
    `{!Equivalence R}
    (f : A  B  B) (b : B)
    `{!Proper ((=) ==> R ==> R) f}
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper (() ==> R) (collection_fold f b).
Proof.
  intros ?? E. apply (foldr_permutation R f b).
  * auto.
  * by rewrite E.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
208

209
Global Instance cforall_dec `(P : A  Prop)
210
  `{ x, Decision (P x)} X : Decision (cforall P X) | 100.
211
212
Proof.
  refine (cast_if (decide (Forall P (elements X))));
213
214
    abstract (unfold cforall; setoid_rewrite elements_spec;
      by rewrite <-Forall_forall).
215
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217
218
219
220
Global Instance cexists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (cexists P X) | 100.
Proof.
  refine (cast_if (decide (Exists P (elements X))));
221
222
    abstract (unfold cexists; setoid_rewrite elements_spec;
      by rewrite <-Exists_exists).
223
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
224

225
226
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
227
End fin_collection.