fin_collections.v 11.3 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.
9
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
10

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

15 16 17
Instance collection_filter
    `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
  of_list (filter P (elements X)).
18
Typeclasses Opaque collection_filter.
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
Section fin_collection.
Context `{FinCollection A C}.
22
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
23

24 25
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
26 27 28 29 30 31 32 33

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 *)
34
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36
Proof.
  intros ?? E. apply NoDup_Permutation.
37 38 39
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Qed.
41

42 43 44 45 46
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
47 48 49 50 51 52 53 54 55 56 57
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.

58 59 60 61 62 63 64 65 66 67 68 69
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]}),
70
    elements_union_singleton, elements_empty by set_solver.
71 72 73 74 75 76 77
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.

78
(** * The [size] operation *)
79
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
80
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
81

82
Lemma size_empty : size ( : C) = 0.
83
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
84
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
86 87
  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
88
Qed.
89
Lemma size_empty_iff (X : C) : size X = 0  X  .
90
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
93

94
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
95
Proof.
96
  destruct (elements X) as [|x l] eqn:HX; [right|left].
97 98
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
99
Qed.
100 101 102 103
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.
104
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
105
Proof.
106 107
  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
108
Qed.
109 110 111 112 113 114 115 116 117

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.
118
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Proof.
120 121
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
122
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
123
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Qed.
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
Lemma size_union X Y : X  Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  intros. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  apply Permutation_length, NoDup_Permutation.
130 131
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
132
    intros x; rewrite !elem_of_elements; set_solver.
133
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
136
Proof.
137 138 139
  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
140
Qed.
141

Robbert Krebbers's avatar
Robbert Krebbers committed
142
Lemma subseteq_size X Y : X  Y  size X  size Y.
143
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149
  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
150
Qed.
151 152

(** * Induction principles *)
153
Lemma collection_wf : wf (strict (@subseteq C _)).
154
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Lemma collection_ind (P : C  Prop) :
156
  Proper (() ==> iff) P 
157
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
161
  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
162 163
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
164
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Qed.
166 167 168
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.
169 170

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

193
(** * Minimal elements *)
194
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
  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.
210 211
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  X     x, x  X  minimal R x X.
213
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
214

215
(** * Filter *)
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
Section filter.
  Context (P : A  Prop) `{! x, Decision (P x)}.

  Lemma elem_of_filter X x : x  filter P X  P x  x  X.
  Proof.
    unfold filter, collection_filter.
    by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
  Qed.
  Global Instance set_unfold_filter X Q :
    SetUnfold (x  X) Q  SetUnfold (x  filter P X) (P x  Q).
  Proof.
    intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x  X) Q).
  Qed.

  Lemma filter_empty : filter P (:C)  .
  Proof. set_solver. Qed.
  Lemma filter_union X Y : filter P (X  Y)  filter P X  filter P Y.
  Proof. set_solver. Qed.
  Lemma filter_singleton x : P x  filter P ({[ x ]} : C)  {[ x ]}.
  Proof. set_solver. Qed.
  Lemma filter_singleton_not x : ¬P x  filter P ({[ x ]} : C)  .
  Proof. set_solver. Qed.

  Section leibniz_equiv.
    Context `{!LeibnizEquiv C}.
    Lemma filter_empty_L : filter P (:C) = .
    Proof. set_solver. Qed.
    Lemma filter_union_L X Y : filter P (X  Y) = filter P X  filter P Y.
    Proof. set_solver. Qed.
    Lemma filter_singleton_L x : P x  filter P ({[ x ]} : C) = {[ x ]}.
    Proof. set_solver. Qed.
    Lemma filter_singleton_not_L x : ¬P x  filter P ({[ x ]} : C) = .
    Proof. set_solver. Qed.
  End leibniz_equiv.
End filter.
251

252
(** * Decision procedures *)
253 254 255 256 257
Lemma set_Forall_elements P X : set_Forall P X  Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
Lemma set_Exists_elements P X : set_Exists P X  Exists P (elements X).
Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed.

258
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
259 260
  {set_Forall P X} + {set_Exists Q X}.
Proof.
261
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
262 263 264 265 266
   [by apply set_Forall_elements|by apply set_Exists_elements].
Defined.

Lemma not_set_Forall_Exists P `{dec :  x, Decision (P x)} X :
  ¬set_Forall P X  set_Exists (not  P) X.
267
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
268 269 270
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
271 272
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
273 274 275 276
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
277
Proof.
278 279
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
280
Defined.
281 282
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
283
Proof.
284 285
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
286
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
End fin_collection.