fin_collections.v 8.91 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
3
4
5
(* 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 . *)
6
7
8
From Coq Require Import Permutation.
From stdpp Require Import relations listset.
From stdpp Require Export numbers collections.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10
11
12
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
13
14
15

Section fin_collection.
Context `{FinCollection A C}.
16
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18
19
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
20
21
22
23
24
25
26
27

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
  refine (cast_if (decide_rel () x (elements X)));
    by rewrite <-(elem_of_elements _).
Defined.

(** * The [elements] operation *)
28
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
Proof.
  intros ?? E. apply NoDup_Permutation.
31
32
33
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Qed.
35

36
37
38
39
40
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
41
42
43
44
45
46
47
48
49
50
51
Lemma elements_empty_inv X : elements X = []  X  .
Proof.
  intros HX; apply elem_of_equiv_empty; intros x.
  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
Qed.
Lemma elements_empty' X : elements X = []  X  .
Proof.
  split; intros HX; [by apply elements_empty_inv|].
  by rewrite <-Permutation_nil, HX, elements_empty.
Qed.

52
53
54
55
56
57
58
59
60
61
62
63
Lemma elements_union_singleton (X : C) x :
  x  X  elements ({[ x ]}  X)  x :: elements X.
Proof.
  intros ?; apply NoDup_Permutation.
  { apply NoDup_elements. }
  { by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
  intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
  by rewrite elem_of_cons, elem_of_elements.
Qed.
Lemma elements_singleton x : elements {[ x ]} = [x].
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
64
    elements_union_singleton, elements_empty by set_solver.
65
66
67
68
69
70
71
Qed.
Lemma elements_contains X Y : X  Y  elements X `contains` elements Y.
Proof.
  intros; apply NoDup_contains; auto using NoDup_elements.
  intros x. rewrite !elem_of_elements; auto.
Qed.

72
(** * The [size] operation *)
73
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
74
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
75

76
Lemma size_empty : size ( : C) = 0.
77
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
78
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof.
80
81
  intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
  by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Qed.
83
Lemma size_empty_iff (X : C) : size X = 0  X  .
84
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
87

88
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
89
Proof.
90
  destruct (elements X) as [|x l] eqn:HX; [right|left].
91
92
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
93
Qed.
94
95
96
97
Lemma collection_choose X : X     x, x  X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X     x, x  X.
Proof. unfold_leibniz. apply collection_choose. Qed.
98
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
99
Proof.
100
101
  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Qed.
103
104
105
106
107
108
109
110
111

Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
112
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Proof.
114
115
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
116
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
117
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Qed.
119

Robbert Krebbers's avatar
Robbert Krebbers committed
120
Lemma size_union X Y : X  Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
  intros. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  apply Permutation_length, NoDup_Permutation.
124
125
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
126
    intros x; rewrite !elem_of_elements; set_solver.
127
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
130
Proof.
131
132
133
  rewrite <-size_union by set_solver.
  setoid_replace (Y  X) with ((Y  X)  X) by set_solver.
  rewrite <-union_difference, (comm ()); set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Qed.
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
Lemma subseteq_size X Y : X  Y  size X  size Y.
137
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
140
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
  rewrite size_union_alt, difference_twice.
  cut (size (Y  X)  0); [lia |].
  by apply size_non_empty_iff, non_empty_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Qed.
145
146

(** * Induction principles *)
147
Lemma collection_wf : wf (strict (@subseteq C _)).
148
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Lemma collection_ind (P : C  Prop) :
150
  Proper (() ==> iff) P 
151
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
155
  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
156
157
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
158
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Qed.
160
161
162
Lemma collection_ind_L `{!LeibnizEquiv C} (P : C  Prop) :
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
163
164

(** * The [collection_fold] operation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
167
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
168
   X, P (collection_fold f b X) X.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
Proof.
  intros ? Hemp Hadd.
171
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
172
173
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  induction 1 as [|x l ?? IH]; simpl.
175
  - intros X HX. setoid_rewrite elem_of_nil in HX.
176
    rewrite equiv_empty. done. set_solver.
177
  - intros X HX. setoid_rewrite elem_of_cons in HX.
178
179
    rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Qed.
181
182
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
183
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
184
  Proper (() ==> R) (collection_fold f b : C  B).
185
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
Lemma minimal_exists `{!StrictOrder R,  x y, Decision (R x y)} (X : C) :
  X     x, x  X  minimal R x X.
Proof.
  pattern X; apply collection_ind; clear X.
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
  intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX].
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
      eauto using union_minimal, singleton_minimal, minimal_weaken.
    - exists x'; split; [set_solver|].
      auto using union_minimal, singleton_minimal_not_above. }
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
Lemma minimal_exists_L
    `{!LeibnizEquiv C, !StrictOrder R,  x y, Decision (R x y)} (X : C) :
  X     x, x  X  minimal R x X.
Proof. unfold_leibniz. apply minimal_exists. Qed.

208
(** * Decision procedures *)
209
210
Global Instance set_Forall_dec `(P : A  Prop)
  `{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
211
212
Proof.
  refine (cast_if (decide (Forall P (elements X))));
213
    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
214
      by rewrite <-Forall_forall).
215
Defined.
216
217
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
218
219
Proof.
  refine (cast_if (decide (Exists P (elements X))));
220
    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
221
      by rewrite <-Exists_exists).
222
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
End fin_collection.