-
Notifications
You must be signed in to change notification settings - Fork 1
/
MM.v
470 lines (420 loc) · 21.8 KB
/
MM.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
(* ---------------------------------------------------------------------------------------
This file contains results of Maximum matchings.
The file contains a function produce_MM, which produces a maximum matching
from any list of bids B and list of asks A. We also prove that matching produced
by this function is largest in size as compared to any other possible matching
on the same set of bids B and asks A.
Lemma produce_MM_is_MM: Sorted by_dbp B -> Sorted by_dsp A-> Is_MM (produce_MM B A) B A.
-------------------------------------------------------------------------------------- *)
Require Import ssreflect ssrbool.
Require Export Lists.List.
Require Export GenReflect SetSpecs.
Require Export DecSort MinMax.
Require Export BidAsk.
Require Export DecList.
Require Export Matching.
Require Export AuctionInvar.
Require Export Fair.
Section MM.
Fixpoint produce_MM (B:list Bid) (A: list Ask): (list fill_type) :=
match (B, A) with
|(nil, _) => nil
|(b::B', nil) => nil
|(b::B', a::A') => match (Nat.leb (sp a) (bp b)) with
|true => ({|bid_of:= b ; ask_of:= a ; tp:=(bp b) |})::(produce_MM B' A')
|false => produce_MM B A'
end
end.
(*------------ Sorting by decreasing ask prices and their properties --------------*)
Definition by_dsp := fun a1 a2 : Ask => a2 <=? a1.
Lemma by_dsp_P : transitive by_dsp /\ comparable by_dsp.
Proof. { split.
{ unfold transitive. unfold by_dsp.
intros y x z H H1. move /leP in H1. move /leP in H.
apply /leP. omega. }
{ unfold comparable. unfold by_dsp. intros.
move /leP in H. apply /leP. omega. } } Qed.
Lemma by_dsp_refl: reflexive by_dsp.
Proof. eauto. Qed.
Hint Resolve by_dsp_P by_dsp_refl: core.
Lemma nil_is_MM_forB (B: list Bid): Is_MM nil B nil.
Proof. { unfold Is_MM. split.
{ eauto. }
{ intros. destruct H. destruct H0.
assert (H2: asks_of M'=nil). eauto.
assert (H3: |M'|=|asks_of M'|). eapply asks_of_size.
assert (H4: |asks_of M'| = 0). rewrite H2. auto. omega. } } Qed.
Lemma nil_is_MM_forA (A: list Ask): Is_MM nil nil A.
Proof. { unfold Is_MM. split.
{ eauto. }
{ intros. destruct H. destruct H0.
assert (H2: bids_of M'=nil). eauto.
assert (H3: |M'|=|bids_of M'|). eapply bids_of_size.
assert (H4: |bids_of M'| = 0). rewrite H2. auto. omega. } } Qed.
Hint Resolve nil_is_MM_forB nil_is_MM_forA: core.
Lemma produce_MM_bids_in_B(B: list Bid)(A: list Ask): bids_of (produce_MM B A) [<=] B.
Proof. { revert B. induction A.
{ intros. simpl. case B eqn: H0. all:simpl;auto. }
{ intros. simpl. case B eqn: H0.
{ simpl;auto. }
{ destruct (a <=? b) eqn: Hab.
{ simpl. intros x H1.
destruct H1 as [H1 | H1].
subst b. auto. cut (In x l). auto.
apply IHA. exact. }
{ apply IHA. } } } } Qed.
Lemma produce_MM_asks_in_A (B: list Bid)(A: list Ask): asks_of (produce_MM B A) [<=] A.
Proof. { revert B. induction A.
{ intros. simpl. case B eqn: H0. all:simpl;auto. }
{ intros. simpl. case B eqn: H0.
{ simpl;auto. }
{ destruct (a <=? b) eqn: Hab.
{ simpl. intros x H1.
destruct H1 as [H1 | H1].
subst a. auto. cut (In x A). auto.
eapply IHA. exact H1. }
{ intros x H1. cut (In x A). auto. eapply IHA. exact H1. } } } } Qed.
Lemma produce_MM_is_matching(B: list Bid)(A: list Ask)(no_dup_B: NoDup B)(no_dup_A: NoDup A):
Sorted by_dbp B -> Sorted by_dsp A -> matching_in B A (produce_MM B A).
Proof. { revert B no_dup_B. induction A as [| a].
{ intros. simpl.
case B eqn: H1.
{ simpl. eauto. }
{ simpl. eauto. } }
{ intros.
case B eqn: H2.
{ simpl. eauto. }
{ split.
{(*--- matching (produce_MM (b :: l) (a :: A)) ----*)
split.
{ (*-- All_matchable (produce_MM (b :: l) (a :: A))----*)
simpl.
destruct (a <=? b) eqn:Hab.
{ apply All_matchable_intro. simpl. move /leP in Hab. exact.
cut (matching_in l A (produce_MM l A)).
intro H3. apply H3.
apply IHA. all: eauto. }
{ cut (matching_in (b::l) A (produce_MM (b::l) A)).
intro H3. apply H3.
apply IHA. all: eauto. } }
split.
{ (*---- NoDup (bids_of (produce_MM (b :: l) (a :: A))) ---*)
simpl.
destruct (a <=? b) eqn:Hab.
{ simpl. apply nodup_intro.
{ intro H3.
assert (H4: In b l). eapply produce_MM_bids_in_B. exact H3.
absurd (In b l). all: auto. }
{ cut (matching_in l A (produce_MM l A)).
intro H3. apply H3.
apply IHA. all: eauto. } }
{ cut (matching_in (b::l) A (produce_MM (b::l) A)).
intro H3. apply H3.
apply IHA. all: eauto. } }
{ (*----- NoDup (asks_of (produce_MM (b :: B) (a :: l))) ----*)
simpl.
destruct (a <=? b) eqn:Hab.
{ simpl. apply nodup_intro.
{ intro H3.
assert (H4: In a A). eapply produce_MM_asks_in_A. exact H3.
absurd (In a A). all: auto. }
{ cut (matching_in l A (produce_MM l A)).
intro H3. apply H3.
apply IHA. all: eauto. } }
{ cut (matching_in (b::l) A (produce_MM (b::l) A)).
intro H3. apply H3.
apply IHA. all: eauto. } } }
split.
{ (*--- bids_of (produce_MM (b :: B) (a :: l)) [<=] b :: B --*)
eapply produce_MM_bids_in_B. }
{ (*---- asks_of (produce_MM (b :: B) (a :: l)) [<=] a :: l--- *)
eapply produce_MM_asks_in_A. } } } } Qed.
Lemma produce_MM_is_MM (B: list Bid)(A: list Ask)(no_dup_B: NoDup B)(no_dup_A: NoDup A):
Sorted by_dbp B -> Sorted by_dsp A-> Is_MM (produce_MM B A) B A.
Proof. revert B no_dup_B. induction A as [|a A'].
{ (* base case: when A is nil *)
intros B hB H H0. case B. simpl.
{ eauto. }
{ intros b l. simpl. eauto. } }
{ (* induction step: when A is a::A' *)
intros B hB h h0. case B as [| b B'].
{ simpl. eauto. }
{ (*----- induction step : b::B' and a:: A' ---------*)
assert (Case: b < a \/ b >= a ). omega.
destruct Case as [C1 | C2].
{ (*------C1: when b and a are not matchable then produce_MM (b::B') A' *)
simpl. replace (a <=? b) with false.
2:{ symmetry. apply /leP. omega. }
assert (h1: Is_MM (produce_MM (b::B') A') (b::B') A').
{ apply IHA'. all: eauto. }
unfold Is_MM. split.
{ (*-- matching_in (b :: B') (a :: A') (produce_MM (b :: B') A') ---*)
destruct h1 as [h1a h1]. eauto. }
{ intros M' h2. destruct h1 as [h1a h1].
apply h1.
(* --- Goal: matching_in (b :: B') A' M'---- trivial proof ---*)
unfold matching_in. split.
apply h2. split. apply h2.
assert (h3: asks_of M' [<=] (a::A')). apply h2.
intros x h4.
assert (h5: In x (a::A')). auto. destruct h5.
{ subst x.
assert (h5: exists m, In m M' /\ a = ask_of m). auto.
destruct h5 as [m h5]. destruct h5 as [h5a h5].
assert (h6: a <= bid_of m).
{ subst a. cut (matching M').
unfold matching. intro h6. destruct h6. auto.
apply h2. }
assert (h7: In (bid_of m) (b::B')).
{ cut (In (bid_of m) (bids_of M')).
cut ((bids_of M') [<=] (b::B')). auto.
apply h2. auto. }
assert (h8: (bid_of m) <= b).
{ assert (h9: by_dbp b (bid_of m)). eapply Sorted_elim2. auto.
exact h. exact h7.
unfold by_dbp in h9. apply /leP. auto. }
omega. }
{ auto. } } }
{ (*-- C2: when b and a are matchable then Output is (b,a):: produce_MM B' A'----*)
assert (h1: matching_in (b::B') (a::A') (produce_MM (b::B') (a::A'))).
{ auto using produce_MM_is_matching. }
unfold Is_MM. split. auto.
simpl. replace (a <=? b) with true. 2:{ symmetry. apply /leP. auto. }
intros M h2. simpl.
assert (Hb: In b (bids_of M) \/ ~ In b (bids_of M)). eauto.
assert (Ha: In a (asks_of M) \/ ~ In a (asks_of M)). eauto.
assert (H0: Is_MM (produce_MM B' A') B' A').
{ apply IHA'. all: eauto. }
destruct Hb as [Hb1 | Hb2]; destruct Ha as [Ha1 | Ha2].
{ (* Case_ab1: In b (bids_of M) and In a (asks_of M)------*)
assert (h3: exists m1, In m1 M /\ a = ask_of m1). eauto.
assert (h4: exists m2, In m2 M /\ b = bid_of m2). eauto.
destruct h3 as [m1 h3]. destruct h3 as [h3a h3].
destruct h4 as [m2 h4]. destruct h4 as [h4a h4].
assert (h5: m1 = m2 \/ m1 <> m2). eauto.
destruct h5 as [h5a | h5b].
{ (*-------- h5a : m1 = m2 ---------*)
subst m2.
set (M' := delete m1 M).
assert (h5: matching_in B' A' M').
{ unfold matching_in. unfold M'. split.
{ cut(matching M). auto. apply h2. } split.
{ intros x h5.
assert (h6: In x (b::B')).
{ cut (In x (bids_of M)). apply h2.
cut ((delete m1 M) [<=] M). intro h6.
eapply bids_of_intro1. apply h6. all: auto. }
destruct h6 as [h6 | h6].
{ absurd (In b (bids_of (delete m1 M))).
subst x. subst b. eauto. subst x;auto. }
{ auto. } }
{ intros x h5.
assert (h6: In x (a::A')).
{ cut (In x (asks_of M)). apply h2.
cut ((delete m1 M) [<=] M). intro h6.
eapply asks_of_intro1. apply h6. all: auto. }
destruct h6 as [h6 | h6].
{ absurd (In a (asks_of (delete m1 M))).
subst x. subst a. eauto. subst x;auto. }
{ auto. } } }
assert (h6: |M| = S (|M'|)).
{ unfold M'. eapply delete_size1a. exact. }
assert (h7: |M'| <= |(produce_MM B' A')|). apply H0. exact.
omega. }
{ (*-------- h5b : m1 <> m2 ---------*)
set (M'' := delete m1 (delete m2 M)).
assert (h5: |M| = S (S (|M''|))).
{ unfold M''.
assert (h3b: In m1 (delete m2 M)).
{ auto. }
assert (h6: S (| delete m1 (delete m2 M) |) = |delete m2 M|).
{ symmetry. auto. }
rewrite h6. auto. }
set (m:= {|bid_of:= bid_of m1 ; ask_of:= ask_of m2 ; tp:=(bp (bid_of m1))|}).
set (M' := (m :: M'')).
assert (h6: matching_in B' A' M').
{ unfold matching_in. split.
{ (*----- matching M' ---------------*)
unfold matching. split.
{ unfold M'. cut (ask_of m <= bid_of m).
cut (All_matchable M''). auto.
unfold M''. cut (All_matchable M).
auto. eauto. simpl. cut (ask_of m2 <= ask_of m1).
cut (ask_of m1 <= bid_of m1). omega.
eauto. rewrite <- h3. cut (In (ask_of m2) (a::A')).
intro h6. assert(h7: by_dsp a (ask_of m2)). eapply Sorted_elim2.
auto. exact h0. exact h6.
unfold by_dsp in h7. apply /leP. auto.
eapply matching_in_elim5a. apply h2. auto. } split.
{ (*---- NoDup (bids_of M') ----*)
unfold M'. simpl.
cut (~ In (bid_of m1) (bids_of M'')).
cut (NoDup (bids_of M'')). auto.
{ (*--- NoDup (bids_of M'')---*)
cut (matching M''). auto.
unfold M''. eauto. }
{ unfold M''. apply matching_elim10. apply matching_elim9.
eapply matching_in_elim0. exact h2. apply delete_intro.
exact h3a. exact h5b. } }
{ (*---- NoDup (asks_of M') ----*)
unfold M'. simpl.
cut (~ In (ask_of m2) (asks_of M'')).
cut (NoDup (asks_of M'')). auto.
{ (*--- NoDup (asks_of M'')---*)
cut (matching M''). auto.
unfold M''. eauto. }
{ unfold M''.
assert(h6:asks_of(delete m1 (delete m2 M))[<=]asks_of(delete m2 M)).
eauto. intro h7.
absurd (In (ask_of m2) (asks_of (delete m2 M))).
apply matching_elim11. eapply matching_in_elim0. exact h2.
exact h4a. auto. } } } split.
{ (*----- bids_of M' [<=] B'-------------*)
unfold M'. simpl.
intros x h6. destruct h6 as [h6 | h6].
{ cut (In x (b::B')). cut ( x <> b). intros. apply element_list with
(b:=x)(a:=b). auto. exact.
{ subst x; subst b. eapply matching_elim14 with (M:= M).
all: auto. eauto. }
{ subst x. eapply matching_in_elim4a. apply h2. auto. } }
{ unfold M'' in h6.
assert (h7: In x (bids_of M)).
{ eauto. }
assert (h8: x <> bid_of m2).
{ intro h8. subst x.
assert (h9: In (bid_of m2) (bids_of (delete m2 M))).
eapply bids_of_elim1. exact h6.
absurd (In (bid_of m2) (bids_of (delete m2 M))).
apply matching_elim10. eapply matching_in_elim0.
exact h2. exact h4a. auto. }
rewrite <- h4 in h8.
assert (h9: In x (b::B')).
{ apply h2. auto. }
destruct h9. symmetry in H. contradiction. auto. } }
{ (*------ asks_of M' [<=] A' -------*)
unfold M'. simpl.
intros x h6. destruct h6 as [h6 | h6].
{ cut (In x (a::A')). cut ( x <> a). intros. eapply element_list.
apply not_eq_sym ; trivial. exact H. exact H1.
{ subst x; subst a. eapply matching_elim15 with (M:= M).
all: auto. eauto. }
{ subst x. eapply matching_in_elim5a. apply h2. auto. } }
{ unfold M'' in h6.
assert (h7: In x (asks_of M)).
{ eauto. }
assert (h8: x <> ask_of m1).
{ intro h8. subst x.
assert (h9: In (ask_of m1) (asks_of (delete m2 M))).
apply asks_of_intro. apply delete_intro. exact h3a. exact h5b.
absurd (In (ask_of m1) (asks_of (delete m1 (delete m2 M)))).
apply matching_elim11. apply matching_elim9.
eapply matching_in_elim0. exact h2. apply delete_intro.
exact h3a. exact h5b. auto. }
rewrite <- h3 in h8.
assert (h9: In x (a::A')).
{ apply h2. auto. }
destruct h9. symmetry in H. contradiction. auto. } } }
assert (h7: |M'| <= |(produce_MM B' A')|). apply H0. exact.
unfold M' in h7. simpl in h7. rewrite h5. simpl. omega. } }
{ (* Case_ab2: In b (bids_of M) and ~ In a (asks_of M)----*)
assert (h3: exists m, In m M /\ b = bid_of m). eauto.
destruct h3 as [m h3]. destruct h3 as [h3a h3].
set (M' := delete m M).
assert (h4: matching_in B' A' M').
{ unfold matching_in. split.
{ (*------ matching M' -----------*)
unfold M'. eauto. } split.
{ (*------bids_of M' [<=] B'------*)
intros x h4.
assert (h5: In x (bids_of M)).
{ unfold M' in h4. eauto. }
assert (h5a: In x (b::B')).
{ apply h2. auto. }
assert (h6: x <> b).
{ intro h6. unfold M' in h4.
subst x;subst b.
absurd (In (bid_of m) (bids_of (delete m M))).
apply matching_elim10. eapply matching_in_elim0.
exact h2. exact h3a. auto. }
eapply in_inv2. all: eauto. }
{ (*------ asks_of M' [<=] A'-------*)
intros x h4.
assert (h5: In x (asks_of M)).
{ unfold M' in h4. eauto. }
assert (h6: x <> a).
{ intro h6. subst x. contradiction. }
assert (h7: In x (a::A')).
{ apply h2. auto. }
eapply in_inv2. all: eauto. } }
assert (h5: |M| = S (|M'|)).
{ unfold M'. eapply delete_size1a. exact h3a. }
assert (h6: |M'| <= |(produce_MM B' A')|). apply H0. exact.
omega. }
{ (* Case_ab3: ~ In b (bids_of M) and In a (asks_of M)----*)
assert (h3: exists m, In m M /\ a = ask_of m). eauto.
destruct h3 as [m h3]. destruct h3 as [h3a h3].
set (M' := delete m M).
assert (h4: matching_in B' A' M').
{ unfold matching_in. split.
{ (*------ matching M' -----------*)
unfold M'. eauto. } split.
{ (*------bids_of M' [<=] B'------*)
intros x h4.
assert (h5: In x (bids_of M)).
{ unfold M' in h4. eauto. }
assert (h6: x <> b).
{ intro h6. subst x. contradiction. }
assert (h7: In x (b::B')).
{ apply h2. auto. }
eapply in_inv2. all: eauto. }
{ (*------ asks_of M' [<=] A'-------*)
intros x h4.
assert (h5: In x (asks_of M)).
{ unfold M' in h4. eauto. }
assert (h5a: In x (a::A')).
{ apply h2. auto. }
assert (h6: x <> a).
{ intro h6. unfold M' in h4.
subst x;subst a.
absurd (In (ask_of m) (asks_of (delete m M))).
apply matching_elim11. eapply matching_in_elim0.
exact h2. exact h3a. auto. }
eapply in_inv2. all: eauto. } }
assert (h5: |M| = S (|M'|)).
{ unfold M'. eapply delete_size1a. exact h3a. }
assert (h6: |M'| <= |(produce_MM B' A')|). apply H0. exact.
omega. }
{ (* Case_ab4: ~ In b (bids_of M) and ~ In a (asks_of M)---*)
assert (h3: matching_in B' A' M). eauto using matching_in_elim8.
cut (|M| <= | produce_MM B' A'|). omega. apply H0. exact. } } } } Qed.
Theorem exists_fair_maximum (B: list Bid)(A: list Ask) (Nb: NoDup B) (Na: NoDup A):
exists M, (Is_fair M B A /\ Is_MM M B A).
Proof. { set (M:= produce_MM (sort by_dbp B) (sort by_dsp A)).
assert (H1: Is_MM M (sort by_dbp B) (sort by_dsp A)).
{ apply produce_MM_is_MM. all: eauto.
apply sort_correct;eapply by_dbp_P.
apply sort_correct;eapply by_dsp_P. }
assert (H2: Is_MM M B A).
{ destruct H1 as [H1 H2].
split.
{ eapply match_inv with (M:= M)(B:= (sort by_dbp B)) (A:=(sort by_dsp A)).
all: eauto. }
{ intros M' H3. apply H2.
eapply match_inv with (M:= M')(B:= B) (A:= A). all: eauto. } }
assert (H3: matching_in B A M). apply H2.
apply (exists_fair_matching M B A Nb Na) in H3 as H4.
destruct H4 as [M' H4].
exists M'.
split.
{ apply H4. }
{ unfold Is_MM.
destruct H4 as [H4a H4]. destruct H4 as [H4b H4].
split.
exact.
intros M0 H5. rewrite <- H4.
apply H2. exact. } } Qed.
(*
Definition B2:= ({|b_id:= 1 ; bp:= 125 |}) ::({|b_id:= 2 ; bp:= 120 |}) ::({|b_id:= 3 ; bp:= 112 |}) ::({|b_id:= 4 ; bp:= 91 |}) ::({|b_id:= 5 ; bp:= 82 |}) ::({|b_id:= 6 ; bp:= 82 |}) ::({|b_id:= 7 ; bp:= 69 |}) ::({|b_id:= 8 ; bp:= 37 |}) :: nil.
Definition A2:= ({|s_id:= 1 ; sp:= 121 |}) ::({|s_id:= 3 ; sp:= 113 |}) ::({|s_id:= 5 ; sp:= 98 |}) ::({|s_id:= 9 ; sp:= 94 |}) ::({|s_id:= 90 ; sp:= 90 |}) ::({|s_id:= 78 ; sp:= 85 |}) ::({|s_id:= 67 ; sp:= 79 |}) ::({|s_id:= 45 ; sp:= 53 |}) ::nil.
*)
End MM.