fin_collections.v 7.56 KB
Newer Older
1
(* Copyright (c) 2012-2013, 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 . *)
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Require Import Permutation ars.
7
Require Export collections numbers listset.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Definition choose `{Elements A C} (X : C) : option A := head (elements X).
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
16

Section fin_collection.
Context `{FinCollection A C}.

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

27
Lemma size_empty : size ( : C) = 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Proof.
29
  unfold size, collection_size. simpl.
30
31
  rewrite (elem_of_nil_inv (elements )); [done |].
  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_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

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

59
60
61
62
63
64
65
66
67
68
Lemma choose_Some X x : choose X = Some x  x  X.
Proof.
  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
  rewrite elements_spec, E. by left.
Qed.
Lemma choose_None X : choose X = None  X  .
Proof.
  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
  apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
Qed.
69
Lemma elem_of_or_empty X : ( x, x  X)  X  .
70
71
Proof. destruct (choose X) eqn:?; eauto using choose_Some, choose_None. Qed.
Lemma choose_is_Some X : X    is_Some (choose X).
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  destruct (choose X) eqn:?.
74
75
  * rewrite elem_of_equiv_empty. split; eauto using choose_Some.
  * split. intros []; eauto using choose_None. by intros [??].
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77
Lemma not_elem_of_equiv_empty X : X    ( x, x  X).
78
Proof.
79
80
  destruct (elem_of_or_empty X) as [?|E]; [esolve_elem_of |].
  setoid_rewrite E. setoid_rewrite elem_of_empty. naive_solver.
81
Qed.
82
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
83
Proof.
84
85
  intros E1. apply not_elem_of_equiv_empty. intros E2.
  rewrite E2, size_empty in E1. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Qed.
87
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Proof.
89
90
91
92
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
  * rewrite elem_of_singleton. eauto using size_singleton_inv.
  * solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
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
  * apply elements_nodup.
100
  * apply NoDup_app; repeat split; try apply elements_nodup.
101
    intros x. rewrite <-!elements_spec. esolve_elem_of.
102
  * intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Qed.
104
105
106

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
107
  refine (cast_if (decide_rel () x (elements X)));
108
109
110
111
112
113
114
115
116
    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.
117
118
  intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
119
120
Qed.
Next Obligation.
121
122
  intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
123
124
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
125
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
126
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
  rewrite <-size_union by solve_elem_of.
  setoid_replace (Y  X) with ((Y  X)  X) by esolve_elem_of.
  rewrite <-union_difference, (commutative ()); solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
Qed.

Lemma subseteq_size X Y : X  Y  size X  size Y.
133
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
  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
140
141
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
Lemma collection_wf : wf (@subset C _).
Proof. apply well_founded_lt_compat with size, subset_size. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
145
Lemma collection_ind (P : C  Prop) :
146
  Proper (() ==> iff) P 
147
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
152
153
154
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
  intros X IH. destruct (elem_of_or_empty X) as [[x ?]|HX].
  * rewrite (union_difference {[ x ]} X) by solve_elem_of.
    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
  * by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
Qed.

Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
159
160
161
  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
162
163
Proof.
  intros ? Hemp Hadd.
164
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
165
  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  induction 1 as [|x l ?? IH]; simpl.
167
  * intros X HX. setoid_rewrite elem_of_nil in HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
    rewrite equiv_empty. done. esolve_elem_of.
169
  * intros X HX. setoid_rewrite elem_of_cons in HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
    rewrite (union_difference {[ x ]} X) by esolve_elem_of.
    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
Qed.

174
175
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
176
177
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
  Proper (() ==> R) (collection_fold f b).
178
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
179

180
181
Global Instance set_Forall_dec `(P : A  Prop)
  `{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
182
183
Proof.
  refine (cast_if (decide (Forall P (elements X))));
184
    abstract (unfold set_Forall; setoid_rewrite elements_spec;
185
      by rewrite <-Forall_forall).
186
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
187

188
189
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
190
191
Proof.
  refine (cast_if (decide (Exists P (elements X))));
192
    abstract (unfold set_Exists; setoid_rewrite elements_spec;
193
      by rewrite <-Exists_exists).
194
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
195

196
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
197
  Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
Robbert Krebbers's avatar
Robbert Krebbers committed
198
End fin_collection.