-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathBindings.v
1938 lines (1779 loc) · 61.1 KB
/
Bindings.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
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2015-2016 IBM Corporation
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*)
(** This module provides support for bindings, which are association
lists for which the keys are ordered and without duplicates.
Bindings are used as a representation for records and environments. *)
Require Import List.
Require Import Sumbool.
Require Import Arith.
Require Import Bool.
Require Import Permutation.
Require Import Equivalence.
Require Import EquivDec.
Require Import RelationClasses.
Require Import Orders.
Require Import Permutation.
Require Import CoqLibAdd.
Require Import ListAdd.
Require Import SortingAdd.
Require Import Assoc.
Require Import Sublist.
Require Import Compat.
Require Import String.
Require Import StringAdd.
Section Bindings.
Class ODT {K:Type}
:= mkODT { ODT_eqdec:>EqDec K eq;
ODT_lt:K -> K -> Prop;
ODT_lt_strorder:>StrictOrder ODT_lt;
ODT_lt_dec: forall (a b:K), {ODT_lt a b} + {~ODT_lt a b};
ODT_compare:K -> K -> comparison;
ODT_compare_spec: forall x y : K,
CompareSpec (eq x y) (ODT_lt x y) (ODT_lt y x) (ODT_compare x y) }.
Generalizable Variables K.
Context `{odt:@ODT K}.
Lemma ODT_lt_irr (k:K) :
~(ODT_lt k k).
Proof.
apply irreflexivity.
Qed.
Ltac dest_strlt :=
match goal with
| [|- context [ODT_lt_dec ?x ?y]] => destruct (ODT_lt_dec x y); simpl
| [H:ODT_lt ?x ?x|- _] => (assert False by (apply (ODT_lt_irr x); auto); contradiction)
end.
(* trichotemy *)
Lemma trichotemy a b : {ODT_lt a b} + {eq a b} + {ODT_lt b a}.
Proof.
generalize (ODT_compare_spec a b); intros nc.
destruct (ODT_compare a b); [left; right|left;left|right]; inversion nc; trivial.
Defined.
Lemma compare_refl_eq a: ODT_compare a a = Eq.
Proof.
destruct (ODT_compare_spec a a);[reflexivity|dest_strlt|dest_strlt].
Qed.
Lemma compare_eq_iff x y : (ODT_compare x y) = Eq <-> x=y.
Proof.
case ODT_compare_spec; intro H; split; try easy; intro EQ;
contradict H;rewrite EQ; apply irreflexivity.
Qed.
Lemma ODT_lt_contr (x y : K) : ~ ODT_lt x y -> ~ ODT_lt y x -> x = y.
Proof.
destruct (trichotemy x y) as [[?|?]|?]; intuition.
Qed.
(* Starting here ... *)
Definition rec_field_lt {A} (a b:K*A) :=
ODT_lt (fst a) (fst b).
Global Instance rec_field_lt_strict {A} : StrictOrder (@rec_field_lt A).
Proof.
unfold rec_field_lt.
inversion odt.
constructor.
+ unfold Irreflexive, Reflexive, complement in *; intros.
destruct x; simpl in odt.
apply (StrictOrder_Irreflexive k H).
+ unfold Transitive in *; intros.
destruct x; destruct y; destruct z; simpl in *.
apply (StrictOrder_Transitive k k0 k1 H H0).
Qed.
Lemma rec_field_lt_dec {A} (a b:K*A) :
{rec_field_lt a b} + {~rec_field_lt a b}.
Proof.
destruct a.
destruct b.
unfold rec_field_lt; simpl.
apply ODT_lt_dec.
Defined.
Lemma rec_field_lt_irr {A} (a:K*A) :
~(rec_field_lt a a).
Proof.
apply StrictOrder_Irreflexive.
Qed.
Lemma Forall_rec_field_lt {A} (a:K*A) l :
Forall (rec_field_lt a) l <-> Forall (ODT_lt (fst a)) (domain l).
Proof.
destruct a; simpl.
induction l; simpl.
- intuition.
- destruct IHl as [H1 H2].
split; inversion 1; subst; constructor; eauto.
Qed.
Definition rec_cons_sort {A} :=
@insertion_sort_insert (K*A) rec_field_lt rec_field_lt_dec.
Definition rec_sort {A} :=
@insertion_sort (K*A) rec_field_lt rec_field_lt_dec.
Definition rec_concat_sort {A} (l1 l2:list (K*A)) : (list (K*A)) :=
rec_sort (l1++l2).
(* Lifted from SortingAdd *)
Lemma sorted_rec_nil {A} :
is_list_sorted ODT_lt_dec (@domain K A nil) = true.
Proof.
reflexivity.
Qed.
Lemma sort_rec_single_type {A} (k:K) (a:A):
is_list_sorted ODT_lt_dec (domain ((k,a)::nil)) = true.
Proof.
reflexivity.
Defined.
Lemma field_less_is_neq (a1 a2:K) :
ODT_lt a1 a2 -> a1 <> a2.
Proof.
unfold not; intros.
subst; dest_strlt.
Qed.
Lemma field_less_is_not_more (a1 a2:K) :
ODT_lt a1 a2 -> ~(ODT_lt a2 a1).
Proof.
elim ODT_lt_strorder; intros.
unfold Transitive, Irreflexive, Reflexive, complement in *.
unfold not; intros.
specialize (StrictOrder_Transitive a1 a2 a1 H H0).
specialize (StrictOrder_Irreflexive a1 StrictOrder_Transitive).
assumption.
Qed.
Lemma field_not_less_and_neq_is_more (a1 a2:K) :
~(ODT_lt a1 a2) -> ~(eq a1 a2) -> ODT_lt a2 a1.
Proof.
unfold not; intros.
generalize (ODT_compare_spec a1 a2).
intros.
inversion H1.
congruence.
assert False.
apply H.
assumption.
contradiction.
assumption.
Qed.
Lemma rec_cons_lt {A} (l1:list (K*A)) (a1 a2:K*A) :
is_list_sorted ODT_lt_dec (domain (a2 :: l1)) = true ->
ODT_lt (fst a1) (fst a2) ->
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l1)) = true.
Proof.
simpl; intros.
revert H0; elim (ODT_lt_dec (fst a1) (fst a2)); intros.
assumption.
contradiction.
Qed.
Lemma rec_sorted_skip_first {A} (l1:list (K*A)) (a:K*A) :
is_list_sorted ODT_lt_dec (domain (a :: l1)) = true ->
is_list_sorted ODT_lt_dec (domain l1) = true.
Proof.
simpl.
intros.
revert H; elim (domain l1); intros.
reflexivity.
destruct (ODT_lt_dec (fst a) a0); congruence.
Qed.
Lemma rec_sorted_skip_second {A} (l:list (K*A)) (a1 a2:K*A) :
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true ->
is_list_sorted ODT_lt_dec (domain (a1 :: l)) = true.
Proof.
intros; simpl in *.
revert H; destruct l; try reflexivity; simpl.
elim (ODT_lt_dec (fst a1) (fst a2));
elim (ODT_lt_dec (fst a2) (fst p));
elim (ODT_lt_dec (fst a1) (fst p));
intros; try congruence.
assert (ODT_lt (fst a1) (fst p))
by (apply transitivity with (y := (fst a2)); assumption).
contradiction.
Qed.
Lemma rec_sorted_skip_third {A} (l:list (K*A)) (a1 a2 a3:K*A) :
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: a3 :: l)) = true ->
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true.
Proof.
intros; simpl in *.
revert H; destruct l; simpl.
- simpl.
elim (ODT_lt_dec (fst a1) (fst a2));
elim (ODT_lt_dec (fst a2) (fst a3));
elim (ODT_lt_dec (fst a1) (fst a3)); intros; try congruence.
- elim (ODT_lt_dec (fst a1) (fst a2));
elim (ODT_lt_dec (fst a2) (fst a3));
elim (ODT_lt_dec (fst a3) (fst p));
elim (ODT_lt_dec (fst a2) (fst p));
intros; try congruence.
assert (ODT_lt (fst a2) (fst p))
by (apply transitivity with (y := (fst a3)); assumption).
contradiction.
Qed.
Lemma rec_sorted_distinct {A} (l:list (K*A)) (a1 a2:K*A) :
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true ->
(fst a1) <> (fst a2).
Proof.
intros.
induction l.
simpl in *.
revert H.
elim (ODT_lt_dec (fst a1) (fst a2)); intros.
apply field_less_is_neq ; assumption.
congruence.
apply IHl; clear IHl.
apply (rec_sorted_skip_third l a1 a2 a); assumption.
Qed.
Lemma rec_sorted_lt {A} (l:list (K*A)) (a1 a2:K*A) :
is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true ->
ODT_lt (fst a1) (fst a2).
Proof.
simpl.
elim (ODT_lt_dec (fst a1) (fst a2)); intros.
assumption.
congruence.
Qed.
Lemma sorted_cons_in {A} (l:list (K*A)) (a a':K*A) :
is_list_sorted ODT_lt_dec (domain (a :: l)) = true ->
In a' l ->
ODT_lt (fst a) (fst a').
Proof.
intros.
induction l.
- simpl in H0; contradiction.
- simpl in H0.
elim H0; clear H0; intros.
+ rewrite H0 in *; clear H0 a0.
simpl in H.
destruct (ODT_lt_dec (fst a) (fst a')); try congruence.
+ assert (is_list_sorted ODT_lt_dec (domain (a :: l)) = true)
by (apply rec_sorted_skip_second with (a2 := a0); assumption).
apply (IHl H1 H0).
Qed.
(* Back here... *)
Lemma rec_cons_lt_first {A} (l1:list (K*A)) (a1 a2:K*A) :
is_list_sorted ODT_lt_dec (domain (a2 :: l1)) = true ->
ODT_lt (fst a1) (fst a2) ->
rec_cons_sort a1 (a2 :: l1) = (a1 :: a2 :: l1).
Proof.
simpl; intros.
elim (rec_field_lt_dec a1 a2); intros.
reflexivity.
unfold rec_field_lt in *.
congruence.
Qed.
Lemma sort_sorted_is_id {A} (l:list (K*A)) :
is_list_sorted ODT_lt_dec (domain l) = true ->
rec_sort l = l.
Proof.
induction l; intros; simpl in *.
reflexivity.
assert (is_list_sorted ODT_lt_dec (domain l) = true).
destruct l; simpl in *; try reflexivity.
destruct (ODT_lt_dec (fst a) (fst p)); congruence.
specialize (IHl H0).
rewrite IHl; clear IHl.
destruct l; simpl in *; try reflexivity.
revert H.
destruct (ODT_lt_dec (fst a) (fst p)); intros.
destruct (rec_field_lt_dec a p); intros.
reflexivity.
unfold rec_field_lt in n.
congruence.
congruence.
Qed.
Lemma rec_concat_sort_concats {A} (l1 l2:list (K*A)) :
rec_concat_sort l1 l2 = rec_sort (l1++l2).
Proof.
reflexivity.
Qed.
Lemma rec_cons_sorted_id {A} (l:list (K*A)) (a:K*A) :
is_list_sorted ODT_lt_dec (domain (a :: l)) = true ->
rec_cons_sort a l = a::l.
Proof.
intros.
destruct l.
reflexivity.
assert (ODT_lt (fst a) (fst p))
by (apply (rec_sorted_lt l a p); assumption).
apply (rec_cons_lt_first l a p).
apply (rec_sorted_skip_first (p::l) a); assumption.
assumption.
Qed.
Lemma rec_sorted_id {A} (l:list (K*A)) :
is_list_sorted ODT_lt_dec (domain l) = true ->
rec_sort l = l.
Proof.
induction l.
reflexivity.
simpl; intros.
assert (is_list_sorted ODT_lt_dec (domain l) = true).
revert H.
destruct l; try reflexivity.
simpl.
destruct (ODT_lt_dec (fst a) (fst p)); congruence.
specialize (IHl H0); clear H0.
rewrite IHl.
simpl.
assert (is_list_sorted ODT_lt_dec (domain (a :: l)) = true).
unfold is_list_sorted.
simpl.
revert H.
destruct l; try reflexivity.
intros.
simpl in *; revert H.
destruct (ODT_lt_dec (fst a) (fst p)); intros.
- revert H; destruct (domain l); try reflexivity.
destruct (ODT_lt_dec (fst p) k); try congruence.
intros.
simpl in H.
assumption.
- congruence.
- generalize (rec_cons_sorted_id l a H0); intros.
unfold rec_cons_sort in H1.
assumption.
Qed.
Lemma rec_cons_gt_first {A} (l' l:list (K*A)) (a1 a2:K*A) :
rec_cons_sort a1 l = l' ->
is_list_sorted ODT_lt_dec (domain (a2 :: l)) = true ->
ODT_lt (fst a2) (fst a1) ->
(exists a3, exists l'', rec_cons_sort a1 l = (a3 :: l'')
/\ ODT_lt (fst a2) (fst a3)).
Proof.
revert a1 a2 l'.
induction l; intros.
- simpl in *; intros; exists a1, nil; split; [reflexivity|assumption].
- simpl in *.
revert H; elim (rec_field_lt_dec a1 a); intros.
inversion H.
exists a1,(a::l).
split; [reflexivity|assumption].
revert H; elim (rec_field_lt_dec a a1); intros.
destruct l'; try congruence.
rewrite H in *.
exists p,l'.
+ split; try reflexivity.
inversion H.
rewrite <- H3 in *; clear H3.
revert H0.
elim (ODT_lt_dec (fst a2) (fst a)); intros.
assumption.
congruence.
+ exists a,l.
split. reflexivity.
revert H0.
elim (ODT_lt_dec (fst a2) (fst a)); intros.
assumption.
congruence.
Qed.
Lemma rec_cons_sorted {A} (l1 l2:list (K*A)) (a:K*A) :
is_list_sorted ODT_lt_dec (domain l1) = true ->
rec_cons_sort a l1 = l2 ->
is_list_sorted ODT_lt_dec (domain l2) = true.
Proof.
revert l2 a.
induction l1; intros.
simpl in *; rewrite <- H0; reflexivity.
simpl in *.
assert (is_list_sorted ODT_lt_dec (domain (a::l1)) = true)
by assumption.
revert H0.
elim (rec_field_lt_dec a0 a); intros.
rewrite <- H0.
apply rec_cons_lt; assumption.
rewrite <- H0.
destruct (rec_field_lt_dec a a0); intros. clear b.
- assert (exists a3, exists l'', rec_cons_sort a0 l1 = (a3 :: l'')
/\ ODT_lt (fst a) (fst a3)).
apply (rec_cons_gt_first (rec_cons_sort a0 l1) l1).
reflexivity.
assumption.
assumption.
elim H2; clear H2; intros.
elim H2; clear H2; intros.
elim H2; clear H2; intros.
destruct l2; try congruence.
inversion H0.
rewrite <- H5 in *; clear H5.
specialize (IHl1 l2 a0).
assert (is_list_sorted ODT_lt_dec (domain l1) = true).
apply (rec_sorted_skip_first l1 a); assumption.
specialize (IHl1 H4 H6).
rewrite H2 in *.
rewrite <- H6 in *.
apply rec_cons_lt; assumption.
- assumption.
Qed.
Lemma rec_sort_sorted {A} (l1 l2:list (K*A)) :
rec_sort l1 = l2 -> is_list_sorted ODT_lt_dec (domain l2) = true.
Proof.
revert l2.
induction l1; intros.
simpl; inversion H; reflexivity.
simpl in *.
assert (exists l'', rec_sort l1 = l'').
revert H.
elim (rec_sort l1); intros.
exists nil; reflexivity.
exists (a0::l); reflexivity.
elim H0; intros; clear H0.
rewrite H1 in H.
assert (is_list_sorted ODT_lt_dec (domain x) = true).
apply (IHl1 x H1); assumption.
apply (rec_cons_sorted x l2 a); assumption.
Qed.
Lemma rec_sort_pf {A} {l1: list (K*A)} :
is_list_sorted ODT_lt_dec (domain (rec_sort l1)) = true.
Proof.
exact (rec_sort_sorted _ _ (eq_refl _)).
Qed.
Lemma rec_concat_sort_sorted {A} (l1 l2 x:list (K*A)) :
rec_concat_sort l1 l2 = x ->
is_list_sorted ODT_lt_dec (domain x) = true.
Proof.
intros.
assert (rec_sort (l1++l2) = x).
rewrite <- rec_concat_sort_concats; assumption.
apply (rec_sort_sorted (l1++l2) x); assumption.
Qed.
Lemma same_domain_same_sorted {A} {B} (l1:list (K*A)) (l2:list (K*B)) :
domain l1 = domain l2 ->
is_list_sorted ODT_lt_dec (domain l1) = true ->
is_list_sorted ODT_lt_dec (domain l2) = true.
Proof.
intros.
rewrite <- H; assumption.
Qed.
Lemma same_domain_insert {A} {B}
(l1:list (K*A)) (l2:list (K*B))
(a:K*A) (b:K*B):
domain l1 = domain l2 ->
fst a = fst b ->
domain (rec_cons_sort a l1) = domain (rec_cons_sort b l2).
Proof.
intros.
revert l2 H.
induction l1.
induction l2; simpl in *; congruence.
intros; simpl in *.
induction l2; simpl in *; try congruence.
clear IHl2.
inversion H.
elim (rec_field_lt_dec a a0); intros.
elim (rec_field_lt_dec b a1); intros.
simpl.
rewrite H2; rewrite H0; rewrite H3; reflexivity.
unfold rec_field_lt in *.
destruct a; destruct a0; destruct b; destruct a1; simpl in *.
subst. congruence.
unfold rec_field_lt in *.
destruct a; destruct a0; destruct b; destruct a1; simpl in *.
subst.
inversion H.
destruct (ODT_lt_dec k1 k2); try congruence.
destruct (ODT_lt_dec k2 k1); try congruence; simpl.
- rewrite (IHl1 l2 H1); reflexivity.
- rewrite H1; reflexivity.
Qed.
Lemma same_domain_rec_sort {A} {B}
(l1:list (K*A)) (l2:list (K*B)) :
domain l1 = domain l2 ->
domain (rec_sort l1) = domain (rec_sort l2).
Proof.
revert l2; induction l1; simpl; intros.
- symmetry in H; apply domain_nil in H; subst; simpl; trivial.
- destruct l2; simpl in *; try discriminate.
inversion H.
fold (@rec_cons_sort A).
fold (@rec_cons_sort B).
apply same_domain_insert; auto.
Qed.
Lemma insertion_sort_insert_nin_perm {A:Type} l a :
~ In (fst a) (@domain _ A l) ->
Permutation (a::l) (insertion_sort_insert rec_field_lt_dec a l).
Proof.
induction l; simpl; auto.
intuition.
destruct (rec_field_lt_dec a a0); trivial.
generalize (field_not_less_and_neq_is_more _ _ n).
destruct (rec_field_lt_dec a0 a); intuition.
rewrite perm_swap.
rewrite Permutation_cons; try eassumption; trivial.
Qed.
Lemma insertion_sort_perm_proper {A:Type} (l l':list (K*A)) a :
~ In (fst a) (domain l) ->
Permutation l l' ->
Permutation
(insertion_sort_insert rec_field_lt_dec a l)
(insertion_sort_insert rec_field_lt_dec a l').
Proof.
revert l l'.
induction l; simpl; intros.
- apply Permutation_nil in H0; subst; auto.
- assert (inl:In a0 l')
by (apply (Permutation_in _ H0); simpl; intuition).
destruct (in_split _ _ inl) as [l1 [l2 ?]]; subst.
rewrite <- Permutation_middle in H0.
apply Permutation_cons_inv in H0.
intuition.
destruct (rec_field_lt_dec a a0).
+ rewrite H0.
rewrite <- insertion_sort_insert_nin_perm.
* apply Permutation_cons; trivial.
apply Permutation_middle.
* intros nin.
apply (@Permutation_in _ (domain (l1 ++ a0 :: l2)) (domain (a0::l))) in nin.
simpl in nin; intuition.
apply dom_perm. rewrite <- Permutation_middle.
rewrite H0; trivial.
+ assert (rec_field_lt a0 a)
by (apply field_not_less_and_neq_is_more; auto).
destruct (rec_field_lt_dec a0 a); intuition.
rewrite (IHl _ H2 H0).
assert (nin:~ In (fst a) (domain l1)).
intro nin; apply H2.
eapply Permutation_in; [apply dom_perm;symmetry;apply H0|].
unfold domain; rewrite map_app; apply in_or_app; intuition.
revert H1 n H nin. clear. revert l2 a a0.
induction l1; simpl; intros.
* destruct (rec_field_lt_dec a a0); intuition.
destruct (rec_field_lt_dec a0 a); intuition.
* intuition.
destruct (rec_field_lt_dec a0 a); intuition.
rewrite perm_swap. apply Permutation_cons; trivial.
rewrite perm_swap. apply Permutation_cons; trivial.
apply Permutation_middle.
assert (rec_field_lt a a0)
by (apply field_not_less_and_neq_is_more; auto).
destruct (rec_field_lt_dec a a0); intuition.
rewrite perm_swap.
rewrite IHl1; auto.
Qed.
Lemma rec_sort_perm {A:Type} l :
NoDup (@domain _ A l) -> Permutation l (rec_sort l).
Proof.
induction l; simpl; auto.
inversion 1; subst.
rewrite insertion_sort_perm_proper; [| |symmetry; auto].
apply insertion_sort_insert_nin_perm; trivial.
intros nin; apply H2.
eapply Permutation_in; [|eapply nin].
symmetry. apply dom_perm.
auto.
Qed.
Lemma insertion_sort_insert_insertion_nin {A} (a:K*A) a0 l :
~ rec_field_lt a0 a ->
~ rec_field_lt a a0 ->
insertion_sort_insert rec_field_lt_dec a0
(insertion_sort_insert rec_field_lt_dec a l)
= insertion_sort_insert rec_field_lt_dec a l.
Proof.
revert a a0. induction l; simpl; intros.
- destruct (rec_field_lt_dec a0 a); intuition.
destruct (rec_field_lt_dec a a0); intuition.
- destruct (rec_field_lt_dec a0 a); intuition.
+ simpl.
destruct (rec_field_lt_dec a1 a0); intuition.
destruct (rec_field_lt_dec a0 a1); intuition.
+ destruct (rec_field_lt_dec a a0); simpl.
* destruct (rec_field_lt_dec a1 a).
rewrite r in r0; intuition.
destruct (rec_field_lt_dec a a1); trivial.
f_equal; eauto.
* (* we crucially need trichotomy *)
destruct (trichotemy (fst a0) (fst a1)) as [[?|?]|?]; intuition.
destruct (trichotemy (fst a) (fst a0)) as [[?|?]|?]; intuition.
destruct a0; destruct a1; destruct a; simpl in *.
subst.
destruct (ODT_lt_dec k0 k0); try congruence.
assert False by (apply (ODT_lt_irr k0); auto).
contradiction.
Qed.
Lemma insertion_sort_insert_cons_app {A} (a:K*A) l l2 :
insertion_sort rec_field_lt_dec (insertion_sort_insert rec_field_lt_dec a l ++ l2) = insertion_sort rec_field_lt_dec (a::l ++ l2).
Proof.
revert a l2.
induction l; simpl; trivial; intros.
destruct (rec_field_lt_dec a0 a); simpl; trivial.
destruct (rec_field_lt_dec a a0); simpl; trivial.
- rewrite IHl; simpl. apply insertion_sort_insert_swap; eauto.
apply rec_field_lt_strict.
- rewrite insertion_sort_insert_insertion_nin; eauto.
Qed.
Lemma insertion_sort_insertion_sort_app1 {A} l1 l2 :
insertion_sort rec_field_lt_dec (insertion_sort (@rec_field_lt_dec A) l1 ++ l2) =
insertion_sort rec_field_lt_dec (l1 ++ l2).
Proof.
revert l2.
induction l1; simpl; trivial; intros.
rewrite insertion_sort_insert_cons_app.
simpl.
rewrite IHl1.
trivial.
Qed.
Lemma insertion_sort_insertion_sort_app {A} l1 l2 l3 :
insertion_sort rec_field_lt_dec (l1 ++ insertion_sort (@rec_field_lt_dec A) l2 ++ l3) =
insertion_sort rec_field_lt_dec (l1 ++ l2 ++ l3).
Proof.
induction l1; simpl.
- apply insertion_sort_insertion_sort_app1.
- rewrite IHl1; trivial.
Qed.
Lemma insertion_sort_eq_app1 {A l1 l1'} l2 :
insertion_sort (@rec_field_lt_dec A) l1 = insertion_sort rec_field_lt_dec l1' ->
insertion_sort rec_field_lt_dec (l1 ++ l2) =
insertion_sort rec_field_lt_dec (l1' ++ l2).
Proof.
intros.
rewrite <- (insertion_sort_insertion_sort_app1 l1 l2).
rewrite <- (insertion_sort_insertion_sort_app1 l1' l2).
rewrite H.
trivial.
Qed.
Lemma rec_sort_rec_sort_app1 {A} l1 l2 :
rec_sort ((@rec_sort A) l1 ++ l2) =
rec_sort (l1 ++ l2).
Proof.
apply insertion_sort_insertion_sort_app1.
Qed.
Lemma rec_sort_rec_sort_app {A} l1 l2 l3 :
rec_sort (l1 ++ (@rec_sort A) l2 ++ l3) =
rec_sort (l1 ++ l2 ++ l3).
Proof.
apply insertion_sort_insertion_sort_app.
Qed.
Lemma rec_sort_rec_sort_app2 {A} l1 l2 :
rec_sort (l1 ++ (@rec_sort A) l2) =
rec_sort (l1 ++ l2).
Proof.
generalize (rec_sort_rec_sort_app l1 l2 nil).
repeat rewrite app_nil_r.
trivial.
Qed.
Lemma rec_sort_eq_app1 {A l1 l1'} l2 :
(@rec_sort A) l1 = rec_sort l1' ->
rec_sort (l1 ++ l2) =
rec_sort (l1' ++ l2).
Proof.
apply insertion_sort_eq_app1.
Qed.
Lemma rec_cons_sort_Forall2 {A B} P l1 l2 a b :
Forall2 P l1 l2 ->
P a b ->
(domain l1) = (domain l2) ->
fst a = fst b ->
Forall2 P
(insertion_sort_insert (@rec_field_lt_dec A) a l1)
(insertion_sort_insert (@rec_field_lt_dec B) b l2).
Proof.
revert a b l2; induction l1; simpl; inversion 1; intros; subst; simpl; [eauto|].
destruct (rec_field_lt_dec a0 a);
destruct (rec_field_lt_dec b y);
unfold rec_field_lt in *; rewrite H7 in *;
simpl in *; inversion H6; rewrite H1 in *; intuition.
destruct (rec_field_lt_dec a a0); unfold rec_field_lt in *;
rewrite H7,H1 in *;
destruct (rec_field_lt_dec y b); unfold rec_field_lt in *; intuition.
Qed.
Lemma rec_sort_Forall2 {A B} P l1 l2 :
(domain l1) = (domain l2) ->
Forall2 P l1 l2 ->
Forall2 P (@rec_sort A l1) (@rec_sort B l2).
Proof.
Hint Constructors Forall2.
revert l2; induction l1; simpl; inversion 2; subst; eauto.
simpl in *; inversion H.
apply rec_cons_sort_Forall2; auto.
apply same_domain_rec_sort; auto.
Qed.
Lemma rec_concat_sort_nil_r {A} g :
@rec_concat_sort A g nil = rec_sort g.
Proof.
unfold rec_concat_sort. rewrite app_nil_r. trivial.
Qed.
Lemma rec_concat_sort_nil_l {A} g :
@rec_concat_sort A nil g = rec_sort g.
Proof.
unfold rec_concat_sort. simpl. trivial.
Qed.
Lemma drec_sort_idempotent {A} l : @rec_sort A (rec_sort l) = rec_sort l.
Proof.
apply rec_sorted_id.
eapply rec_sort_sorted; eauto.
Qed.
Lemma insertion_sort_insert_equiv_domain {A:Type} x a (l:list (K*A)) :
In x
(domain (SortingAdd.insertion_sort_insert rec_field_lt_dec a l)) <->
fst a = x \/ In x (domain l).
Proof.
induction l; simpl; [intuition|].
destruct a; destruct a0; simpl in *.
destruct (ODT_lt_dec k k0); simpl; [intuition|].
destruct (ODT_lt_dec k0 k); simpl; intuition. subst; clear H.
destruct (trichotemy x k0); intuition.
Qed.
Lemma drec_sort_equiv_domain {A} l :
equivlist (domain (@rec_sort A l)) (domain l).
Proof.
unfold equivlist.
induction l; simpl; [intuition|]; intros x.
rewrite <- IHl. apply insertion_sort_insert_equiv_domain.
Qed.
Hint Resolve ODT_lt_strorder.
Lemma insertion_sort_insert_swap_neq {A} a1 (b1:A) a2 b2 l :
~(eq a1 a2) ->
insertion_sort_insert rec_field_lt_dec (a1, b1)
(insertion_sort_insert rec_field_lt_dec
(a2, b2) l) =
insertion_sort_insert rec_field_lt_dec (a2, b2)
(insertion_sort_insert rec_field_lt_dec
(a1, b1) l).
Proof.
revert a1 b1 a2 b2. induction l; simpl; intros.
- destruct (ODT_lt_dec a1 a2);
destruct (ODT_lt_dec a2 a1); trivial.
+ eelim @asymmetry; eauto.
unfold Asymmetric; intros.
apply (@asymmetry _ _ _ x y); assumption.
+ destruct (trichotemy a1 a2) as [[?|?]|?];
intuition.
- destruct a; simpl.
Ltac t := try (solve[eelim @asymmetry; eauto]); intuition.
repeat dest_strlt;
intuition;
try solve[
rewrite o0 in *; t
| destruct (trichotemy a1 a2) as [[?|?]|?]; intuition].
rewrite o0 in o2.
dest_strlt.
rewrite IHl; [reflexivity|assumption].
Qed.
Lemma insertion_sort_insert_middle {A} l1 l2 a (b:A) :
~ In a (domain l1) ->
SortingAdd.insertion_sort_insert rec_field_lt_dec (a, b)
(SortingAdd.insertion_sort rec_field_lt_dec (l1 ++ l2)) =
SortingAdd.insertion_sort rec_field_lt_dec (l1 ++ (a, b) :: l2).
Proof.
revert l2 a b.
induction l1; simpl; trivial; intros.
intuition.
rewrite <- IHl1; auto.
destruct a; simpl in *.
apply insertion_sort_insert_swap_neq; auto.
Qed.
Lemma drec_sort_perm_eq {A} l l' :
NoDup (@domain _ A l) ->
Permutation l l' ->
rec_sort l = rec_sort l'.
Proof.
unfold rec_sort.
revert l'. induction l; simpl; intros.
- apply Permutation_nil in H0; subst; simpl; trivial.
- inversion H; subst.
destruct a as [a b].
assert (inl:In (a,b) l')
by (apply (Permutation_in _ H0); simpl; intuition).
destruct (in_split _ _ inl) as [l1 [l2 ?]]; subst.
rewrite <- Permutation_middle in H0.
apply Permutation_cons_inv in H0.
inversion H; subst.
rewrite (IHl (l1 ++ l2)); auto.
apply insertion_sort_insert_middle.
intros nin; apply H5.
apply dom_perm in H0.
symmetry in H0.
eapply Permutation_in; try eapply H0.
rewrite domain_app, in_app_iff.
intuition.
Qed.
Lemma drec_sorted_perm_eq {A : Type} (l l' : list (K * A)) :
is_list_sorted ODT_lt_dec (domain l) = true ->
is_list_sorted ODT_lt_dec (domain l') = true ->
Permutation l l' ->
l = l'.
Proof.
intros.
assert (rec_sort l = rec_sort l').
- apply drec_sort_perm_eq; trivial.
apply (is_list_sorted_NoDup ODT_lt_dec); trivial.
- repeat rewrite sort_sorted_is_id in H2 by trivial.
trivial.
Qed.
Lemma drec_concat_sort_app_comm {A} l l':
NoDup (@domain _ A (l ++l')) ->
rec_concat_sort l l' = rec_concat_sort l' l.
Proof.
intros.
unfold rec_concat_sort.
apply drec_sort_perm_eq; auto.
apply Permutation_app_comm.
Qed.
Lemma in_dom_rec_sort {B} {l x}:
In x (domain (rec_sort l)) <-> In x (@domain _ B l).
Proof.
intros.
apply drec_sort_equiv_domain; trivial.
Qed.
Lemma drec_sort_sorted {A} l :
SortingAdd.is_list_sorted ODT_lt_dec
(@domain _ A
(rec_sort l)) = true.
Proof.
eapply rec_sort_sorted; eauto.
Qed.
Lemma drec_concat_sort_sorted {A} l l' :
SortingAdd.is_list_sorted ODT_lt_dec
(@domain _ A
(rec_concat_sort l l')) = true.
Proof.
unfold rec_concat_sort.
eapply rec_sort_sorted; eauto.
Qed.
Lemma drec_sort_drec_sort_concat {A} l l' :
(rec_sort (@rec_concat_sort A l l')) = rec_concat_sort l l'.
Proof.
unfold rec_sort, rec_concat_sort.
apply insertion_sort_idempotent.
Qed.
Lemma assoc_lookupr_insertion_sort_insert_neq {B:Type} a x (b:B) l :
~(eq x a)->
assoc_lookupr ODT_eqdec
(SortingAdd.insertion_sort_insert rec_field_lt_dec (a, b) l)
x
= assoc_lookupr ODT_eqdec l x.
Proof.
revert a x b.
induction l; simpl; intros.
- destruct (ODT_eqdec x a); intuition.
- destruct a; simpl.
destruct (ODT_lt_dec a0 k);
destruct (ODT_lt_dec k a0); simpl.
+ destruct (assoc_lookupr ODT_eqdec l x); trivial.
destruct (ODT_eqdec x k); trivial.
destruct (ODT_eqdec x a0); intuition.
+ destruct (assoc_lookupr ODT_eqdec l x); trivial.
destruct (ODT_eqdec x k); trivial.
destruct (ODT_eqdec x a0); intuition.
+ rewrite IHl; trivial.
+ destruct (trichotemy a0 k); intuition.
Qed.
Lemma assoc_lookupr_insertion_sort_fresh {B:Type} x (d:B) b :
~ In x (domain b) ->
assoc_lookupr ODT_eqdec
(SortingAdd.insertion_sort rec_field_lt_dec (b ++ (x, d) :: nil)) x =
Some d.
Proof.
revert x d.
induction b; simpl; intuition.
- destruct (ODT_eqdec x x); intuition.
- rewrite assoc_lookupr_insertion_sort_insert_neq; auto.
Qed.
Lemma is_list_sorted_NoDup_strlt {A} l :
is_list_sorted ODT_lt_dec (@domain _ A l) = true ->
NoDup (domain l).
Proof.
eapply is_list_sorted_NoDup.
eapply ODT_lt_strorder.
Qed.
Lemma rec_sort_self_cons_middle {A} (l:list (K*A)) (a:K*A):
is_list_sorted ODT_lt_dec (domain (a::l)) = true ->
rec_sort (l ++ a :: l) = rec_sort ((a :: l) ++ l).
Proof.
unfold rec_sort; intros.
assert (l ++ a :: l = (l++(a::nil))++l) by apply app_cons_middle.
rewrite H0.
apply insertion_sort_eq_app1.
generalize (drec_sort_perm_eq (a :: l) (l++(a::nil))); intros.
unfold rec_sort in H1.
rewrite H1; try reflexivity.
apply is_list_sorted_NoDup_strlt; assumption.
rewrite Permutation_app_comm.
simpl.
reflexivity.
Qed.
Lemma rec_field_anti {A} a:
~ (@rec_field_lt A) a a.
Proof.
generalize ODT_lt_strorder; intros.
unfold Irreflexive, Reflexive, complement in *.
destruct a; unfold rec_field_lt; simpl.
inversion H. apply StrictOrder_Irreflexive.
Qed.
Lemma lt_not_not k1 k2:
~ODT_lt k1 k2 -> ~ODT_lt k2 k1 -> eq k1 k2.
Proof.
unfold not; intros.
generalize (trichotemy k1 k2); intros.
inversion H1.
elim H2; intros.
congruence.
assumption.
congruence.
Qed.
Lemma rec_concat_sort_self {A} (l:list (K*A)):
is_list_sorted ODT_lt_dec (domain l) = true ->