fin_collections.v 7.16 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
Require Import Permutation.
Require Export collections listset.

Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
Definition collection_fold `{Elements A C} {B} (f : A  B  B) (b : B) (X : C) : B := 
  fold_right f b (elements X).

Section fin_collection.
Context `{FinCollection A C}.

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

Lemma size_empty : size  = 0.
Proof.
  unfold size, collection_size. rewrite (in_nil_inv (elements )).
24
25
  * easy.
  * intro. rewrite <-elements_spec. simplify_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
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  .
Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.

35
Lemma size_singleton x : size {[ x ]} = 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Proof.
37
  change (length (elements {[ x ]}) = length [x]).
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  apply Permutation_length, NoDup_Permutation.
39
40
41
  * apply elements_nodup.
  * apply NoDup_singleton.
  * intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
45
46
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].
47
48
49
  * discriminate.
  * injection 1. intro. rewrite (nil_length l) by easy.
    simpl. intuition congruence.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
52
53
54
Qed.

Lemma choose X : X    { x | x  X }.
Proof.
  case_eq (elements X).
55
56
57
58
  * intros E. intros []. apply equiv_empty.
    intros x. rewrite elements_spec, E. contradiction.
  * intros x l E. exists x.
    rewrite elements_spec, E. now left.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
Qed.
Lemma size_pos_choose X : 0 < size X  { x | x  X }.
Proof. 
  intros E. apply choose.
63
64
  intros E2. rewrite E2, size_empty in E.
  now destruct (Lt.lt_n_0 0).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Qed.
66
Lemma size_1_choose X : size X = 1  { x | X  {[ x ]} }.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
Proof.
  intros E. destruct (size_pos_choose X).
69
70
  * rewrite E. auto with arith.
  * exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
Qed.

Program Instance collection_car_eq_dec_slow (x y : A) : Decision (x = y) | 100 :=
74
  match Compare_dec.zerop (size ({[ x ]}  {[ y ]})) with
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
79
  | left _ => right _
  | right _ => left _
  end.
Next Obligation.
  intro. apply empty_ne_singleton with x.
80
81
82
  transitivity ({[ x ]}  {[ y ]}).
  * symmetry. now apply size_empty_iff.
  * simplify_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
85
86
87
88
89
90
91
Qed.
Next Obligation. edestruct size_pos_choose; esimplify_elem_of. Qed.

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100 :=
  match decide_rel In x (elements X) with
  | left Hx => left (proj2 (elements_spec _ _) Hx)
  | right Hx => right (Hx  proj1 (elements_spec _ _))
  end.

92
Lemma union_difference X Y : X  Y  X  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
101
102
103
104
105
Proof. split; intros x; destruct (decide (x  X)); simplify_elem_of. 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.
    apply elements_nodup.
   apply NoDup_app; try apply elements_nodup.
   intros x. rewrite <-!elements_spec.
   intros ??. apply (elem_of_empty x), E. simplify_elem_of.
  intros. rewrite in_app_iff, <-!elements_spec. simplify_elem_of.
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
106
107
Proof. rewrite <-size_union. now rewrite union_difference. simplify_elem_of. Qed.
Lemma size_add X x : x  X  size ({[ x ]}  X) = S (size X).
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof. intros. rewrite size_union. now rewrite size_singleton. simplify_elem_of. Qed.
109
Lemma size_difference X Y : X  Y  size X + size (Y  X) = size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof. intros. now rewrite <-size_union_alt, subseteq_union_1. Qed.
111
Lemma size_remove X x : x  X  S (size (X  {[ x ]})) = size X.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
113
114
115
  intros. rewrite <-(size_difference {[ x ]} X).
  * rewrite size_singleton. auto with arith.
  * simplify_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
Qed.

Lemma subseteq_size X Y : X  Y  size X  size Y.
119
120
121
122
123
Proof.
  intros. rewrite <-(subseteq_union_1 X Y) by easy.
  rewrite <-(union_difference X Y), size_union by simplify_elem_of.
  auto with arith.
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127

Lemma collection_wf_ind (P : C  Prop) :
  ( X, ( Y, size Y < size X  P Y)  P X)   X, P X.
Proof.
128
129
130
131
132
  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.
  * now destruct (Lt.lt_n_0 (size X)).
  * apply Hind. intros. apply IHn. eauto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
Qed.

Lemma collection_ind (P : C  Prop) :
136
  Proper (() ==> iff) P  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
Proof.
  intros ? Hemp Hadd. apply collection_wf_ind.
  intros X IH. destruct (Compare_dec.zerop (size X)).
140
141
142
143
144
145
  * now rewrite size_empty_inv.
  * destruct (size_pos_choose X); auto.
    rewrite <-(subseteq_union_1 {[ x ]} X) by simplify_elem_of.
    rewrite <-union_difference.
    apply Hadd; simplify_elem_of. apply IH.
    rewrite <-(size_remove X x); auto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
148
149
Qed.

Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
150
151
152
  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
153
154
Proof.
  intros ? Hemp Hadd.
155
156
157
158
159
160
161
  cut ( l, NoDup l   X, ( x, x  X  In x l)  P (fold_right f b l) X).
  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
  induction 1 as [|x l ?? IHl]; simpl.
  * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
  * intros X HX.
    rewrite <-(subseteq_union_1 {[ x ]} X) by esimplify_elem_of.
    rewrite <-union_difference.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
    apply Hadd. simplify_elem_of. apply IHl.
    intros y. split.
164
165
    + intros. destruct (proj1 (HX y)); simplify_elem_of.
    + esimplify_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
168
169
170
171
Qed.

Lemma collection_fold_proper {B} (f : A  B  B) (b : B) :
  ( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b))  Proper (() ==> (=)) (collection_fold f b).
Proof. intros ??? E. apply fold_right_permutation. auto. now rewrite E. Qed. 

172
173
Global Program Instance cforall_dec `(P : A  Prop)
    `{ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
176
177
  match decide (Forall P (elements X)) with
  | left Hall => left _
  | right Hall => right _
  end.
178
179
180
181
182
183
Next Obligation.
  red. setoid_rewrite elements_spec. now apply Forall_forall.
Qed. 
Next Obligation.
  intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
184

185
186
Global Program Instance cexists_dec `(P : A  Prop)
    `{ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
189
190
  match decide (Exists P (elements X)) with
  | left Hex => left _
  | right Hex => right _
  end.
191
192
193
194
195
196
Next Obligation.
  red. setoid_rewrite elements_spec. now apply Exists_exists. 
Qed. 
Next Obligation.
  intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
197

198
199
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
200
End fin_collection.