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

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.

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 _).
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
Lemma size_empty : size ( : C) = 0.
55
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
Lemma size_empty_inv (X : C) : size X = 0  X  .
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
61
Qed.
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
65
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
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
69
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.
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
73
74
75
Qed.
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
Proof.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
80
81
82
83
84
85
86
87
88
89
90
91
Qed.
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.
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
Proof.
  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Qed.
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Proof.
  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
97
98
Qed.
Lemma size_union X Y : X  Y    size (X  Y) = size X + size Y.
Proof.
  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
  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
104
105
106
107
108
109
110
Qed.
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.
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 _
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
  end.
Next Obligation.
115
  intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
Qed.
Next Obligation.
119
  intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
123
124
  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
Proof.
  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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
Qed.
Lemma subseteq_size X Y : X  Y  size X  size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X  Y  size X < size Y.
Proof.
  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.
Qed.
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C  Prop) :
  Proper (() ==> iff) P 
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof.
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
  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
152
153
154
155
156
157
158
159
Qed.
Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
   X, P (collection_fold f b X) X.
Proof.
  intros ? Hemp Hadd.
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
  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
166
167
168
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
169
  Proper (() ==> R) (collection_fold f b : C  B).
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
Global Instance set_Forall_dec `(P : A  Prop)
  `{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
Proof.
  refine (cast_if (decide (Forall P (elements X))));
    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
      by rewrite <-Forall_forall).
Defined.
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
Proof.
  refine (cast_if (decide (Exists P (elements X))));
    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
      by rewrite <-Exists_exists).
Defined.
Global Instance rel_elem_of_dec `{ x y, Decision (R x y)} x X :
  Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
End fin_collection.