fin_collections.v 8.02 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
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
Proof.
  intros ?? E. apply NoDup_Permutation.
23 24 25
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Qed.
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
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
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]}),
    elements_union_singleton, elements_empty by solve_elem_of.
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.

52
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
53
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
54
Lemma size_empty : size ( : C) = 0.
55
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
56
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof.
58 59
  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
60
Qed.
61
Lemma size_empty_iff (X : C) : size X = 0  X  .
62
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
65
Lemma size_singleton (x : A) : size {[ x ]} = 1.
66
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
69
  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
70
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
71
  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Qed.
73
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
74
Proof.
75
  destruct (elements X) as [|x l] eqn:HX; [right|left].
76 77
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
78
Qed.
79 80 81 82
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.
83
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
84
Proof.
85 86
  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
87
Qed.
88
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Proof.
90 91
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
92 93
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
  - solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96
Qed.
Lemma size_union X Y : X  Y    size (X  Y) = size X + size Y.
Proof.
97
  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  apply Permutation_length, NoDup_Permutation.
99 100
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
101
    intros x; rewrite !elem_of_elements; solve_elem_of.
102
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Qed.
104 105
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
106
  refine (cast_if (decide_rel () x (elements X)));
107
    by rewrite <-(elem_of_elements _).
108 109 110
Defined.
Global Program Instance collection_subseteq_dec_slow (X Y : C) :
    Decision (X  Y) | 100 :=
111 112
  match decide_rel (=) (size (X  Y)) 0 return _ with
  | left _ => left _ | right _ => right _
113 114
  end.
Next Obligation.
115
  intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
116
  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
117 118
Qed.
Next Obligation.
119
  intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
120
  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
121
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
123
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  rewrite <-size_union by solve_elem_of.
125
  setoid_replace (Y  X) with ((Y  X)  X) by solve_elem_of.
126
  rewrite <-union_difference, (comm ()); solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
Qed.
Lemma subseteq_size X Y : X  Y  size X  size Y.
129
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134 135
  intros. rewrite (union_difference X Y) by solve_elem_of.
  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
136
Qed.
137
Lemma collection_wf : wf (strict (@subseteq C _)).
138
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Lemma collection_ind (P : C  Prop) :
140
  Proper (() ==> iff) P 
141
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
145
  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
146
  - rewrite (union_difference {[ x ]} X) by solve_elem_of.
147
    apply Hadd. solve_elem_of. apply IH; solve_elem_of.
148
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151
Qed.
Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
152
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
153
   X, P (collection_fold f b X) X.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155
Proof.
  intros ? Hemp Hadd.
156
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
157 158
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  induction 1 as [|x l ?? IH]; simpl.
160
  - intros X HX. setoid_rewrite elem_of_nil in HX.
161
    rewrite equiv_empty. done. solve_elem_of.
162
  - intros X HX. setoid_rewrite elem_of_cons in HX.
163 164
    rewrite (union_difference {[ x ]} X) by solve_elem_of.
    apply Hadd. solve_elem_of. apply IH. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Qed.
166 167
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
168
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
169
  Proper (() ==> R) (collection_fold f b : C  B).
170
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
171 172
Global Instance set_Forall_dec `(P : A  Prop)
  `{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
173 174
Proof.
  refine (cast_if (decide (Forall P (elements X))));
175
    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
176
      by rewrite <-Forall_forall).
177
Defined.
178 179
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
180 181
Proof.
  refine (cast_if (decide (Exists P (elements X))));
182
    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
183
      by rewrite <-Exists_exists).
184
Defined.
185
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
186
  Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
Robbert Krebbers's avatar
Robbert Krebbers committed
187
End fin_collection.