-
Notifications
You must be signed in to change notification settings - Fork 1
/
UM.v
872 lines (770 loc) · 41.9 KB
/
UM.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
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
(* ---------------------------------------------------------------------------------
This file contains results of Uniform matchings. function produce_UM, which
produces a uniform matching from any list of bids B and list of aks A.
We prove that matching produced by this function is largest among
all possible uniform matching on B and A. We also prove that matching
produced is fair, IR and uniform.
Important results:
Theorem UM_is_maximal_Uniform: Sorted by_dbp B -> Sorted by_sp A->
(forall M: list fill_type, Is_uniform M B A-> |M| <= | (pair_uniform 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 MoreDecList.
Require Export Matching.
Require Export AuctionInvar.
Require Export Fair.
Section UM.
Fixpoint pair_uniform (B:list Bid) (A:list Ask) :=
match (B,A) with
|(nil, _) => nil
|(_,nil)=> nil
|(b::B',a::A') => match Nat.leb (sp a) (bp b) with
|false =>nil
|true => ({|bid_of:= b ; ask_of:= a ; tp:=(bp b) |})::pair_uniform B' A'
end
end.
Lemma UM_correct (B:list Bid) (A:list Ask) : forall m, In m (pair_uniform B A) ->
(bp (bid_of m)) >= (sp (ask_of m)).
Proof. { intros m. revert A. induction B. simpl. auto. intro A.
induction A. simpl. auto. simpl. intro H1.
destruct (a0 <=? a) eqn: H2. destruct H1.
subst m. unfold bid_of. unfold ask_of. move /eqP in H2.
move /eqP in H2. move /leP in H2. auto.
move /leP in H2. eapply IHB. exact H. inversion H1. } Qed.
Lemma UM_is_matching (B: list Bid) (A: list Ask) (NDB: NoDup B) (NDA: NoDup A):
Sorted by_dbp B -> Sorted by_sp A -> matching_in B A (pair_uniform B A).
Proof. { revert B NDB. induction A.
{ case B eqn: H1. simpl. auto. simpl. auto. }
{ case B eqn:H1. simpl. auto.
intros H2 H3 H4. simpl. destruct (a <=? b) eqn:Hab.
assert (Hm:matching_in l A (pair_uniform l A)).
{ eapply IHA with (B:=l). eauto. subst B. eauto. subst B. eauto. eauto. }
eapply matching_in_intro.
{ simpl. move /leP in Hab. exact Hab. }
{ eauto. }
{ simpl. intro H5. assert (Hl:In b l). subst B. unfold matching_in in Hm.
destruct Hm as [Hm1 Hm]. destruct Hm as [Hm2 Hm]. eauto. absurd (In b l).
all:auto.
}
{ simpl. intro H5. assert (Hl:In a A). unfold matching_in in Hm.
destruct Hm as [Hm1 Hm]. destruct Hm as [Hm2 Hm]. eauto. absurd (In a A).
all:auto.
} simpl. left;auto. simpl. left;auto.
auto. } } Qed.
Lemma pair_uniform_bids_sublist_B(B: list Bid)(A: list Ask): sublist (bids_of (pair_uniform 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. rewrite Hab. simpl.
case (b_eqb b b) eqn: Hbb.
{ apply IHA. }
{ unfold b_eqb in Hbb. move /andP in Hbb. destruct Hbb. auto. } }
{ simpl. rewrite Hab. simpl. auto. } } } } Qed.
Lemma pair_uniform_asks_sublist_A(B: list Bid)(A: list Ask): sublist (asks_of (pair_uniform 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. rewrite Hab. simpl.
case (a_eqb a a) eqn: Haa.
{ apply IHA. }
{ unfold b_eqb in Haa. move /andP in Haa. destruct Haa. auto. } }
{ simpl. rewrite Hab. simpl. auto. } } } } Qed.
Lemma bids_of_UM_sorted (B: list Bid) (A: list Ask) :
(Sorted by_dbp B -> (Sorted by_dbp (bids_of (pair_uniform B A)))).
Proof. { assert (H0:sublist (bids_of (pair_uniform B A)) B). apply pair_uniform_bids_sublist_B.
intros. eapply sublist_is_sorted with (lr:=by_dbp) (s:=B). exact. exact. } Qed.
Lemma asks_of_UM_sorted (B: list Bid) (A: list Ask) :
(Sorted by_sp A -> (Sorted by_sp (asks_of (pair_uniform B A)))).
Proof. { assert (H0:sublist (asks_of (pair_uniform B A)) A). apply pair_uniform_asks_sublist_A.
intros. eapply sublist_is_sorted with (lr:=by_sp) (s:=A). exact. exact. } Qed.
Lemma last_in_tail (A:Type): forall l:list A, forall a b d:A,
(last (a::b::l) d) = (last (b::l) d).
Proof. intros. eauto. Qed.
(*--------------------------------------------------------*)
Lemma bid_of_last_and_last_of_bids (F: list fill_type) (b : Bid):
(bid_of (last F m0)) = (last (bids_of F) b0).
Proof.
induction F as [|m']. simpl. auto. {
case F eqn:H1. simpl. auto. replace (last (m' :: f :: l) m0) with (last (f :: l) m0). unfold asks_of;fold asks_of. replace
(last (ask_of m' :: ask_of f :: asks_of l) a0) with
(last (ask_of f :: asks_of l) a0). exact. symmetry.
eapply last_in_tail. symmetry. eapply last_in_tail. } Qed.
Lemma ask_of_last_and_last_of_asks (F: list fill_type) (a: Ask):
(ask_of (last F m0)) = (last (asks_of F) a0).
Proof.
induction F as [|m']. simpl. auto. {
case F eqn:H1. simpl. auto. replace (last (m' :: f :: l) m0) with (last (f :: l) m0). unfold asks_of;fold asks_of. replace
(last (ask_of m' :: ask_of f :: asks_of l) a0) with
(last (ask_of f :: asks_of l) a0). exact. symmetry.
eapply last_in_tail. symmetry. eapply last_in_tail. } Qed.
Lemma UM_returns_IR (B: list Bid) (A: list Ask) (NDB: NoDup B) (NDA: NoDup A):
Sorted by_dbp B -> Sorted by_sp A -> forall m, In m (pair_uniform B A) ->
(bp (bid_of m))>= (tp m) /\ (sp (ask_of m)) <= (tp m).
Proof. { revert NDA. revert A. induction B. intros. split. simpl in H1.
destruct H1. simpl in H1. destruct H1. intros.
case A eqn: Ha. simpl in H1. destruct H1.
simpl in H1. case (a0 <=? a) eqn: Ha0. simpl in H1.
destruct H1. subst m. move /leP in Ha0. simpl. eauto. eapply IHB in H1.
exact. eauto. eauto. eauto. eauto. destruct H1. } Qed.
Fixpoint replace_column (l:list fill_type)(n:nat):=
match l with
|nil=>nil
|m::l'=> ({|bid_of:= bid_of m ; ask_of:= ask_of m ; tp:=n|})::(replace_column l' n)
end.
Lemma replace_column_is_uniform (l: list fill_type)(n:nat):
uniform (trade_prices_of (replace_column l n)).
Proof. { induction l. simpl. constructor.
case l eqn: H. simpl. constructor. simpl. simpl in IHl. constructor;auto. } Qed.
Lemma last_column_is_trade_price (l:list fill_type)(m:fill_type)(n:nat): In m (replace_column l n)->
(tp m = n).
Proof. { intro H. induction l. auto. inversion H as [H0 |].
inversion H0 as [H1 ]. simpl. exact. apply IHl in H0. exact. } Qed.
Lemma replace_column_elim (l: list fill_type)(n:nat): forall m', In m' (replace_column l n)-> exists m, In m l /\ bid_of m = bid_of m'
/\ ask_of m = ask_of m'.
Proof. { intros m' H. induction l.
{ simpl in H. inversion H. }
{ simpl in H. destruct H.
{ exists a. split. auto. split. subst m'. simpl. auto. subst m'. simpl. auto. }
{ apply IHl in H as H1. destruct H1 as [m H1]. exists m.
destruct H1 as [H2 H1]. destruct H1 as [H3 H1]. split.
auto. split;auto. } } } Qed.
Lemma replace_column_elim_bid (l: list fill_type)(n:nat) (m:fill_type):
In m (replace_column l n) -> In (bid_of m) (bids_of l).
Proof. { induction l. intros. simpl. destruct H.
intros. simpl in H. simpl. destruct H. left.
simpl in H. subst m. simpl. exact. right. apply IHl. exact. } Qed.
Lemma replace_column_elim_ask (l: list fill_type)(n:nat) (m:fill_type):
In m (replace_column l n) -> In (ask_of m) (asks_of l).
Proof. { induction l. intros. simpl. destruct H.
intros. simpl in H. simpl. destruct H. left.
simpl in H. subst m. simpl. exact. right. apply IHl. exact. } Qed.
Lemma replace_column_bids_perm (l: list fill_type)(n:nat):
perm (bids_of l) (bids_of (replace_column l n)).
Proof. { induction l.
{ simpl. auto. }
{ simpl. unfold perm. unfold perm in IHl.
move /andP in IHl. destruct IHl.
apply /andP. split.
apply included_elim4b with (a0:=(bid_of a)) in H. exact.
apply included_elim4b with (a0:=(bid_of a)) in H0. exact. }
} Qed.
Lemma replace_column_asks_perm (l: list fill_type)(n:nat):
perm (asks_of l) (asks_of (replace_column l n)).
Proof. { induction l.
{ simpl. auto. }
{ simpl. unfold perm. unfold perm in IHl.
move /andP in IHl. destruct IHl.
apply /andP. split.
apply included_elim4b with (a0:=(ask_of a)) in H. exact.
apply included_elim4b with (a0:=(ask_of a)) in H0. exact. }
} Qed.
Lemma replace_column_size (l: list fill_type)(n:nat):
|(l)| = |((replace_column l n))|.
Proof. induction l. simpl. auto.
simpl. omega. Qed.
Definition uniform_price B A := bp (bid_of (last (pair_uniform B A) m0)).
Lemma uniform_price_bid (B: list Bid) (A:list Ask) (b: Bid) : Sorted by_dbp (B) -> Sorted by_sp (A) -> In b (bids_of (pair_uniform B A)) ->
b >=(uniform_price B A).
Proof. { intros H1 H2 H3. unfold uniform_price.
eapply bids_of_UM_sorted with (A:=A) in H1 as H4 .
assert (H5: by_dbp b (bid_of (last (pair_uniform B A) m0))).
assert (Hlastb: last (bids_of (pair_uniform B A)) b0 = bid_of (last (pair_uniform B A) m0)).
symmetry. eapply bid_of_last_and_last_of_bids with (F:= ((pair_uniform B A))). auto. rewrite <- Hlastb.
eapply last_in_Sorted. apply by_dbp_P. apply by_dbp_refl. exact H4. auto.
unfold by_dbp in H5. move /leP in H5. auto. } Qed.
Lemma pair_uniform_bids_ge_asks (B: list Bid) (A:list Ask) (m: fill_type):
In m (pair_uniform B A) -> (bid_of m) >= (ask_of m).
Proof. { revert B m. induction A.
{ intros. case B eqn: HB.
{ simpl in H. destruct H. }
{ simpl in H. destruct H. } }
{ intros B m H0. case B eqn: HB.
{ simpl in H0. destruct H0. }
{ simpl in H0. case (a <=? b) eqn: Hab.
{ destruct H0.
{ subst m. simpl. move /leP in Hab. auto. }
{ eapply IHA. exact H. } }
{ destruct H0. } } } } Qed.
(*Move below lemma to DecList *)
Lemma last_in_list (T:Type)(l:list T)(x:T)(d:T) : In x l -> In (last l d) l.
Proof. { revert x d.
induction l as [| a l'].
{ (*------ l = nil ------*)
simpl. auto. }
{ (*------ l = a::l'-----*)
destruct l' as [| b l''].
{ (*----- l = [a]------*)
simpl. intros; left;auto. }
{ (*------ l = a ::b::l'' --------*)
intros x d H0.
assert (H1: last (a::b::l'') d = last (b::l'') d).
{ simpl. destruct l'';auto. }
rewrite H1.
cut(In (last (b :: l'') d) (b :: l'')). auto.
eapply IHl' with (x:=b). auto. } } } Qed.
Lemma uniform_price_ask (B: list Bid) (A:list Ask) (a: Ask):
Sorted by_dbp B -> Sorted by_sp (A) -> In a (asks_of (pair_uniform B A))-> a <= (uniform_price B A).
Proof. { intros H1 H2 H3. unfold uniform_price.
eapply asks_of_UM_sorted with (B:=B) in H2 as H4.
eapply bids_of_UM_sorted with (A:=A) in H1 as H4b.
assert (H5: by_sp a (ask_of (last (pair_uniform B A) m0))).
assert (Hlasta: last (asks_of (pair_uniform B A)) a0 = ask_of (last (pair_uniform B A) m0)).
symmetry. eapply ask_of_last_and_last_of_asks. auto. auto.
rewrite <- Hlasta.
eapply last_in_Sorted. apply by_sp_P. apply by_sp_refl. exact H4. auto. unfold by_sp in H5. move /leP in H5.
assert (H6: bid_of (last (pair_uniform B A) m0) >= ask_of (last (pair_uniform B A) m0)).
{ apply pair_uniform_bids_ge_asks with (B:=B) (A:=A).
assert (Hma: exists m, In m (pair_uniform B A) /\ a = ask_of m).
eauto. destruct Hma as [m Hma].
apply last_in_list with (x:=m). apply Hma. }
{ assert (Hma: exists m, In m (pair_uniform B A) /\ a = ask_of m).
eauto. destruct Hma as [m Hma]. omega. } } Qed.
Definition produce_UM (B:list Bid) (A:list Ask) : (list fill_type) :=
replace_column (pair_uniform B A)
(uniform_price B A).
Theorem UM_is_Ind_Rat (B: list Bid) (A:list Ask):
Sorted by_dbp B -> Sorted by_sp A -> Is_IR (produce_UM B A).
Proof. { intros H1 H2. unfold produce_UM. unfold Is_IR.
intros m H3. unfold rational. split.
{ assert (H4: tp m = (uniform_price B A)).
eapply last_column_is_trade_price. exact H3.
rewrite H4. eapply replace_column_elim_bid in H3.
apply uniform_price_bid. exact. exact. exact. }
{ assert (H4: tp m = (uniform_price B A)).
eapply last_column_is_trade_price. exact H3.
rewrite H4. eapply replace_column_elim_ask in H3.
apply uniform_price_ask. exact. exact. exact. } } Qed.
Theorem UM_is_Uniform (B: list Bid) (A:list Ask) : Uniform ( produce_UM B A).
Proof. unfold Uniform. unfold produce_UM. apply replace_column_is_uniform. Qed.
Definition Is_uniform M B A := (Uniform M /\ matching_in B A M /\ Is_IR M).
Lemma matching_on_nilA (B:list Bid) (M:list fill_type) : matching_in B nil M -> M=nil.
Proof. { intros H1. unfold matching_in in H1. destruct H1 as [H1 H2].
destruct H2 as [H2 H3]. unfold matching in H1. destruct H1 as [H1 H4].
unfold All_matchable in H1. assert (HAMnil: (asks_of M) = nil). eauto.
case M eqn: HM. auto. simpl in HAMnil. inversion HAMnil. } Qed.
Lemma matching_on_nilB (A: list Ask)(M:list fill_type) : matching_in nil A M -> M=nil.
Proof. { intros H1. unfold matching_in in H1. destruct H1 as [H1 H2].
destruct H2 as [H2 H3]. unfold matching in H1. destruct H1 as [H1 H4].
unfold All_matchable in H1. assert (HBMnil: (bids_of M) = nil). eauto.
case M eqn: HM. auto. simpl in HBMnil. inversion HBMnil. } Qed.
Lemma unmatchableAB_nil (B:list Bid) (A:list Ask) (b:Bid)(a:Ask) (M:list fill_type): Sorted by_dbp (b::B) -> Sorted by_sp (a::A) ->matching_in (b::B) (a::A) M -> b<a-> M=nil.
Proof. { intros H1 H2 H3 H4.
case M as [|f M'] eqn:HM.
{ auto. }
{ set (b0:= bid_of f). set (a0:= ask_of f).
assert (Hfask: In (ask_of f) (a::A)).
{ eapply matching_in_elim5. exact H3. }
assert (Hfbid: In (bid_of f) (b::B)).
{ eapply matching_in_elim4. exact H3. }
assert (Hmatch: bid_of f >= ask_of f). eauto.
assert (h1: by_dbp b b0).
{ unfold b0. unfold is_true. apply bool_fun_equal.
intro. exact is_true_true. intro.
eapply Sorted_elim2. exact by_dbp_refl.
exact H1. exact Hfbid. }
move /leP in h1. unfold b0 in h1.
assert (h2: by_sp a a0).
{ unfold a0. eauto. }
move /leP in h2. unfold a0 in h2. omega. } } Qed.
Lemma delete_IR_is_IR (M : list fill_type) (m:fill_type): Is_IR M -> Is_IR (delete m M).
Proof. unfold Is_IR. eauto. Qed.
Lemma IR_UM_matchable (M:list fill_type)(b:Bid)(a:Ask):
Is_IR M -> Uniform M -> In a (asks_of M) -> In b (bids_of M)->b>=a.
Proof. { intros H1 H2 Ha Hb.
assert (Hm1: exists m1, (In m1 M) /\ a=(ask_of m1)).
eauto. assert (Hm2: exists m2, (In m2 M) /\ b=(bid_of m2)).
eauto. destruct Hm1 as [m1 Hm1]. destruct Hm2 as [m2 Hm2].
assert (Ht:tp m1 = tp m2).
destruct Hm1 as [Hm1m Hm1a]. destruct Hm2 as [Hm2m Hm2b].
eapply Uniform_elim. eauto. all: auto. assert (Hbm: b>= tp m2).
{ destruct Hm1 as [Hm1m Hm1a]. destruct Hm2 as [Hm2m Hm2b]. subst b.
eapply H1. exact. } assert (Ham: a<= tp m1).
{ destruct Hm1 as [Hm1m Hm1a]. destruct Hm2 as [Hm2m Hm2b]. subst a.
eapply H1. exact. } omega. } Qed.
Lemma M'_unifom_ir (M : list fill_type) (m1 m2: fill_type):
(Is_IR M /\ Uniform M) -> In m1 M -> In m2 M ->
Is_IR (({|bid_of:= bid_of m1 ; ask_of:= ask_of m2 ; tp:=(tp m1)|}::delete m1 (delete m2 M))) /\
Uniform (({|bid_of:= bid_of m1 ; ask_of:= ask_of m2 ; tp:=(tp m1)|}::delete m1 (delete m2 M))).
Proof. { intros H0 H1 H2.
split.
{ destruct H0 as [H0ir H0uni].
set (M'':= delete m1 (delete m2 M)). assert (H_irM'':Is_IR M'').
{ subst M''. unfold Is_IR. intros. apply H0ir. eapply delete_elim1.
simple eapply delete_elim1. exact H. }
{ assert (Htp: tp m1 = tp m2). eapply Uniform_elim.
exact H0uni. exact H1. exact H2.
assert (Hrationalm2: rational m2).
eauto. unfold rational in Hrationalm2.
assert (Htpm2: tp m2 >= ask_of m2). eapply Hrationalm2.
set (m:={| bid_of := bid_of m1; ask_of := ask_of m2; tp := tp m1 |}).
assert (mrat:rational m).
{ unfold rational. subst m. simpl.
assert (Hrationalm1: rational m1). eauto.
unfold rational in Hrationalm1.
assert (Htpm1: bid_of m1 >= tp m1). eapply Hrationalm1.
split. eauto. omega. } eauto. } }
{ destruct H0 as [H0ir H0uni].
set (M'':= delete m1 (delete m2 M)). assert (H_uniM'':Uniform M'').
subst M''. eauto. case M'' eqn: HM''. constructor.
assert (HeM'': In e M''). rewrite HM''. auto. assert (HeM: In e M).
eapply delete_elim1. eapply delete_elim1. exact HeM''.
assert (H_e: tp e = tp m1).
eapply Uniform_elim. exact H0uni.
exact HeM. exact H1. rewrite <- H_e. eauto. } } Qed.
Lemma IR_UM_matchable_m (M:list fill_type)(m1 m2:fill_type):
Is_IR M -> Uniform M -> In m1 M -> In m2 M-> bid_of m1 >=ask_of m2.
Proof. { intros H1 H2 H3 H4. assert (Htp: tp m1 = tp m2).
eapply Uniform_elim. exact H2. exact H3. exact H4.
assert (Htpm1b: tp m1 <= bid_of m1).
{ unfold Is_IR in H1. unfold rational in H1. eapply H1. exact. }
assert (Htpm1a: tp m1 >= ask_of m1).
{ unfold Is_IR in H1. unfold rational in H1. eapply H1. exact. }
assert (Htpm2b: tp m2 <= bid_of m2).
{ unfold Is_IR in H1. unfold rational in H1. eapply H1. exact. }
assert (Htpm2a: tp m2 >= ask_of m2).
{ unfold Is_IR in H1. unfold rational in H1. eapply H1. exact. }
omega. } Qed.
Lemma UM_pair_fair_on_bids (B:list Bid)(A:list Ask):
Sorted by_dbp B -> Sorted by_sp A -> fair_on_bids (pair_uniform B A) B.
Proof. { revert A. induction B as [|b].
{ intros. unfold fair_on_bids. intros. simpl in H3. inversion H3. }
{ intros. unfold fair_on_bids. intros b0 b0' H2 H3 H4.
destruct A eqn: Ha.
{ simpl. inversion H4. }
{ assert (case1: b0' = b \/ b0' <> b). eauto.
destruct H2 as [H2 H2a].
assert (case3: b = b0' \/ In b0' (bids_of (pair_uniform B l))).
{ destruct case1. left. exact. right. simpl in H4.
destruct (a <=? b) eqn:Hab. simpl in H4. destruct H4.
symmetry in H4. contradiction. eauto. destruct H4.
}
destruct case1 as [c1a | c1b].
{ subst b0'. assert (H5: b0 <= b).
{ apply Sorted_elim2 with (x:= b0) in H as H0a.
apply /leP. auto. unfold by_dbp.
unfold reflexive. auto. auto. } omega. }
{ assert (H5: In b0' B).
{ eapply in_inv2. exact H2a. exact c1b. }
assert (case2: b0=b \/ In b0 B).
{ auto. }
destruct case2 as [c2a | c2b].
{ subst b0. simpl. case (a <=? b) eqn: Hab. simpl. left. auto.
simpl in H4. rewrite Hab in H4. destruct H4. }
{ destruct case3 as [c3a | c3b].
{ subst b. contradiction. }
{ simpl. case (a <=? b) eqn: Hab. simpl. right. eapply IHB.
{ eauto. }
{ eauto. }
{ simpl in H2. split. auto. exact H5. }
{ exact. }
{ simpl in H4. rewrite Hab in H4. simpl in H4.
destruct H4. eauto. exact. }
{ simpl in H4. rewrite Hab in H4. simpl in H4. auto. } } } } } } } Qed.
Lemma UM_pair_fair_on_asks (B:list Bid) (A:list Ask):
(Sorted by_dbp B) -> (Sorted by_sp A) -> fair_on_asks (pair_uniform B A) A.
Proof. { revert B. induction A as [|a].
{ intros. unfold fair_on_asks. intros.
destruct B eqn: Hb. simpl in H3. inversion H3.
simpl in H3. inversion H3. }
{ intros. unfold fair_on_asks. intros s s' H2 H3 H4.
destruct B eqn: Hb.
{ simpl. inversion H4. }
{ assert (case1: s' = a \/ s' <> a). eauto.
destruct H2 as [H2 H2a].
assert (case3: a = s' \/ In s' (asks_of (pair_uniform l A))).
{ destruct case1. left. exact. right. simpl in H4.
destruct (a <=? b) eqn:Hab. simpl in H4. destruct H4.
symmetry in H4. contradiction. eauto.
destruct H4. }
destruct case1 as [c1a | c1b].
{ subst s'. assert (H5: s >= a).
{ simpl in H2. destruct H2. subst a. auto.
assert (Hb0: by_sp a s). eauto.
unfold by_sp in Hb0. move /leP in Hb0. omega. } omega. }
{ assert (H5: In s' A).
{ eapply in_inv2. exact H2a. exact c1b. }
assert (case2: a=s \/ In s A).
{ auto. }
destruct case2 as [c2a | c2b].
{ subst s. simpl. case (a <=? b) eqn: Hab. simpl. left. auto.
simpl in H4. rewrite Hab in H4. destruct H4. }
{ destruct case3 as [c3a | c3b].
{ subst a. contradiction. }
{ simpl. case (a <=? b) eqn: Hab. simpl. right. eapply IHA.
{ eauto. }
{ eauto. }
{ simpl in H2. split. auto. exact H5. }
{ exact. }
{ simpl in H4. rewrite Hab in H4. simpl in H4.
destruct H4. eauto. exact. }
{ simpl in H4. rewrite Hab in H4. simpl in H4. auto. } } } } } } } Qed.
Lemma UM_pair_fair (B: list Bid) (A:list Ask)(m: fill_type):
Sorted by_dbp B -> Sorted by_sp A-> Is_fair (pair_uniform B A ) B A.
Proof. { intros H1 H2. unfold Is_fair.
split. apply UM_pair_fair_on_asks. all:eauto.
apply UM_pair_fair_on_bids. all:eauto. } Qed.
Theorem UM_fair (B: list Bid) (A:list Ask):
Sorted by_dbp B -> Sorted by_sp A-> Is_fair (produce_UM B A) B A.
Proof. { intros H1 H2. unfold produce_UM.
unfold Is_fair.
split.
{ unfold fair_on_asks. intros.
assert (H5: fair_on_asks (pair_uniform B A) A).
apply UM_pair_fair_on_asks. exact. exact.
assert (H6: perm (asks_of ((pair_uniform B A)))
(asks_of (replace_column ((pair_uniform B A)) ((uniform_price B A))))).
apply replace_column_asks_perm.
assert (H7: In s' (asks_of (pair_uniform B A))).
{ apply perm_elim with (a:=s') in H6.
assert (H8: (count s'
(asks_of
(replace_column (pair_uniform B A) (uniform_price B A)))) >=1).
eauto. assert (H9: (count s' (asks_of (pair_uniform B A)))>=1).
omega. apply countP1b in H9. exact. }
unfold fair_on_asks in H5.
assert (H8: (In s (asks_of (pair_uniform B A)))).
eapply H5 in H7. exact H7. auto. auto.
apply perm_elim with (a:=s) in H6.
assert (H9: (count s (asks_of (pair_uniform B A)))>=1).
eauto.
assert (H10: (count s
(asks_of
(replace_column (pair_uniform B A) (uniform_price B A))))>=1).
omega. apply countP1b in H10. exact.
}
{ unfold fair_on_bids. intros.
assert (H5: fair_on_bids (pair_uniform B A) B).
apply UM_pair_fair_on_bids. exact. exact.
assert (H6: perm (bids_of ((pair_uniform B A)))
(bids_of (replace_column ((pair_uniform B A)) ((uniform_price B A))))).
apply replace_column_bids_perm.
assert (H7: In b' (bids_of (pair_uniform B A))).
{ apply perm_elim with (a:=b') in H6.
assert (H8: (count b'
(bids_of
(replace_column (pair_uniform B A) (uniform_price B A)))) >=1).
eauto. assert (H9: (count b' (bids_of (pair_uniform B A)))>=1).
omega. apply countP1b in H9. exact. }
unfold fair_on_bids in H5.
assert (H8: (In b (bids_of (pair_uniform B A)))).
eapply H5 in H7. exact H7. auto. auto.
apply perm_elim with (a:=b) in H6.
assert (H9: (count b (bids_of (pair_uniform B A)))>=1).
eauto.
assert (H10: (count b
(bids_of
(replace_column (pair_uniform B A) (uniform_price B A))))>=1).
omega. apply countP1b in H10. exact.
} } Qed.
Lemma UM_size (B: list Bid) (A:list Ask):
|(pair_uniform B A )|=|produce_UM B A|.
Proof. unfold produce_UM. eapply replace_column_size. Qed.
Theorem UM_is_maximal_Uniform (B: list Bid) (A:list Ask)(no_dup_B: NoDup B)(no_dup_A: NoDup A): Sorted by_dbp B -> Sorted by_sp A-> (forall M: list fill_type, Is_uniform M B A-> |M| <= | (produce_UM 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.
{ intros M H1. destruct H1 as [H1 H2].
destruct H2 as [H2 H3]. apply matching_on_nilA in H2. subst M. auto. }
{ intros b l. simpl. intros M H1. destruct H1 as [H1 H2].
destruct H2 as [H2 H3]. apply matching_on_nilA in H2. subst M. auto. } }
{ (* induction step: when A is a::A' *)
intros B hB h h0. case B as [| b B'].
{ simpl. intros M H1. destruct H1 as [H1 H2]. destruct H2 as [H2 H3].
apply matching_on_nilB in H2. subst M. auto. }
{ (*----- 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. } intros M H1.
destruct H1 as [H1 H2]. destruct H2 as [H2 H3].
assert (HM:M=nil). eapply unmatchableAB_nil.
eauto. eauto. eauto. exact. subst M. 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') (pair_uniform (b::B') (a::A'))).
{eauto using UM_is_matching. }
intros M h2. destruct h2 as [h2a h2]. destruct h2 as [h2 h2b].
simpl. replace (a <=? b) with true.
2:{ symmetry. apply /leP. auto. }
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: forall M, Is_uniform M B' A' -> |M| <= |(pair_uniform B' A')|).
{assert (Hpair:(| pair_uniform B' A' |)=(| produce_UM B' A' |)). apply UM_size.
rewrite Hpair. 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 (h5_ir: Is_IR M').
{eapply delete_IR_is_IR. exact. }
assert (h5_unif: Uniform M').
{ subst M'. eauto. }
assert (h5_is_uni:Is_uniform M' B' A').
{unfold Is_uniform. eauto. }
assert (h6: |M| = S (|M'|)).
{ unfold M'. eapply delete_size1a. exact. }
assert (h7: |M'| <= |(pair_uniform B' A')|). apply H0. exact.
simpl.
{ assert (Hpair:(|produce_UM (b::B') (a::A') |)=
(| pair_uniform (b::B') (a::A') |)). symmetry. eapply UM_size.
rewrite Hpair. simpl. destruct (a <=? b) eqn: Hba. simpl. omega.
assert (Hbat:(a <=? b) = true). apply /leP. omega.
rewrite Hba in Hbat. inversion Hbat. } }
{ (*-------- 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:=(tp 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. set t:=tp m1.
assert (h_t1:bid_of m1 >=t).
{ subst t. assert ( Hrationalm1:rational m1). eauto.
unfold rational in Hrationalm1. apply Hrationalm1. }
assert (h_t2: t>=ask_of m2).
{ subst t. assert ( Hrationalm2:rational m2). eauto.
unfold rational in Hrationalm2.
assert (Htpm1m2: tp m1 = tp m2).
eapply Uniform_elim.
exact h2a. exact. exact. rewrite Htpm1m2. apply Hrationalm2. }
simpl. omega. } 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. exact. } } }
{ (*---- 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))).
simple apply matching_elim11. simple eapply matching_in_elim0.
exact h2. exact. 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 H H1. eapply in_inv2. exact H1. exact H. }
{ 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 H H1. eapply in_inv2. exact H1. exact H. }
{ 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 (h5_is_uni: (Is_IR M') /\ (Uniform M')).
subst M'. subst M''. subst m.
assert (h_temp1: (Is_IR M /\ Uniform M) ). auto.
eapply M'_unifom_ir with
(M:=M) (m1:=m1) (m2:=m2). exact. exact. exact.
assert (h5_ir: Is_IR M').
{ apply h5_is_uni. }
assert (h5_unif: Uniform M').
{ apply h5_is_uni. }
(*continue from here*)
assert (h5_is_unif:Is_uniform M' B' A').
{unfold Is_uniform. eauto. }
assert (h7: |M'| <= |(pair_uniform B' A')|). apply H0. exact.
unfold M' in h7. simpl in h7. rewrite h5.
{ assert (Hpair:(|produce_UM (b::B') (a::A') |)=
(| pair_uniform (b::B') (a::A') |)). symmetry. eapply UM_size.
rewrite Hpair. simpl. destruct (a <=? b) eqn: Hba. simpl. omega.
assert (Hbat:(a <=? b) = true). apply /leP. omega.
rewrite Hba in Hbat. inversion Hbat. } } }
{ (* 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. }
assert (h5_ir: Is_IR M').
{ subst M'. eapply Is_IR_elim2. exact. }
assert (h5_unif: Uniform M').
{ subst M'. eauto. }
assert (h5_is_uni:Is_uniform M' B' A').
{unfold Is_uniform. eauto. }
assert (h6: |M'| <= |(pair_uniform B' A')|). apply H0. exact.
{ assert (Hpair:(|produce_UM (b::B') (a::A') |)=
(| pair_uniform (b::B') (a::A') |)). symmetry. eapply UM_size.
rewrite Hpair. simpl. destruct (a <=? b) eqn: Hba. simpl. omega.
assert (Hbat:(a <=? b) = true). apply /leP. omega.
rewrite Hba in Hbat. inversion Hbat. } }
{ (* 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. }
assert (h5_ir: Is_IR M').
{ subst M'. eapply Is_IR_elim2. exact. }
assert (h5_unif: Uniform M').
{ subst M'. eauto. }
assert (h5_is_uni:Is_uniform M' B' A').
{unfold Is_uniform. eauto. }
assert (h6: |M'| <= |(pair_uniform B' A')|). apply H0. exact.
{ assert (Hpair:(|produce_UM (b::B') (a::A') |)=
(| pair_uniform (b::B') (a::A') |)). symmetry. eapply UM_size.
rewrite Hpair. simpl. destruct (a <=? b) eqn: Hba. simpl. omega.
assert (Hbat:(a <=? b) = true). apply /leP. omega.
rewrite Hba in Hbat. inversion Hbat. } }
{ (* 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.
assert (h5_ir: Is_IR M).
{ exact. }
assert (h5_unif: Uniform M).
{exact. }
assert (h5_is_uni:Is_uniform M B' A').
{unfold Is_uniform. eauto. }
cut (|M| <= | pair_uniform B' A'|).
{ assert (Hpair:(|produce_UM (b::B') (a::A') |)=
(| pair_uniform (b::B') (a::A') |)). symmetry. eapply UM_size.
rewrite Hpair. simpl. destruct (a <=? b) eqn: Hba. simpl. omega.
assert (Hbat:(a <=? b) = true). apply /leP. omega.
rewrite Hba in Hbat. inversion Hbat. } apply H0. exact. } } } } Qed.
End UM.