fin_collections.v 7.22 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 listset numbers.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9

Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
10
Definition collection_fold `{Elements A C} {B} (f : A  B  B)
11
  (b : B) (X : C) : B := foldr f b (elements X).
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
27
28

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

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

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

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.
73
Proof.
74
75
76
  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
77
Qed.
78
Lemma size_1_choose X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
Proof.
  intros E. destruct (size_pos_choose X).
81
  * rewrite E. auto with arith.
82
  * exists x. apply elem_of_equiv. split.
83
84
    + intro. rewrite elem_of_singleton.
      eauto using size_singleton_inv.
85
    + solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
89
90
91
Qed.

Lemma size_union X Y : X  Y    size (X  Y) = size X + size Y.
Proof.
  intros [E _]. unfold size, collection_size. rewrite <-app_length.
  apply Permutation_length, NoDup_Permutation.
92
93
94
95
  * apply elements_nodup.
  * apply NoDup_app; try apply elements_nodup.
    intros x. rewrite <-!elements_spec. esolve_elem_of.
  * intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Qed.
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
  refine (cast_if (decide_rel In x (elements X)));
    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
122
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
123
Proof.
124
  rewrite <-size_union. by rewrite union_difference. solve_elem_of.
125
Qed.
126
Lemma size_add X x : x  X  size ({[ x ]}  X) = S (size X).
127
Proof.
128
  intros. rewrite size_union. by rewrite size_singleton. solve_elem_of.
129
Qed.
130

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

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

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

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

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

Lemma collection_fold_proper {B} (f : A  B  B) (b : B) :
195
196
  ( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) 
  Proper (() ==> (=)) (collection_fold f b).
197
Proof. intros ??? E. apply foldr_permutation. auto. by rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198

199
200
201
202
203
204
205
Global Instance cforall_dec `(P : A  Prop)
    `{ x, Decision (P x)} X : Decision (cforall P X) | 100.
Proof.
  refine (cast_if (decide (Forall P (elements X))));
  abstract (unfold cforall; setoid_rewrite elements_spec;
    by rewrite <-Forall_forall).
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
206

207
208
209
210
211
212
213
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))));
  abstract (unfold cexists; setoid_rewrite elements_spec;
    by rewrite <-Exists_exists).
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
214

215
216
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
217
End fin_collection.