fin_collections.v 7.38 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
Require Import Permutation prelude.relations prelude.listset.
Require Export prelude.numbers prelude.collections.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

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

Section fin_collection.
Context `{FinCollection A C}.
15
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

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