-
Notifications
You must be signed in to change notification settings - Fork 112
/
path.v
1782 lines (1403 loc) · 64.3 KB
/
path.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
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
(******************************************************************************)
(* The basic theory of paths over an eqType; this file is essentially a *)
(* complement to seq.v. Paths are non-empty sequences that obey a progression *)
(* relation. They are passed around in three parts: the head and tail of the *)
(* sequence, and a proof of a (boolean) predicate asserting the progression. *)
(* This "exploded" view is rarely embarrassing, as the first two parameters *)
(* are usually inferred from the type of the third; on the contrary, it saves *)
(* the hassle of constantly constructing and destructing a dependent record. *)
(* We define similarly cycles, for which we allow the empty sequence, *)
(* which represents a non-rooted empty cycle; by contrast, the "empty" path *)
(* from a point x is the one-item sequence containing only x. *)
(* We allow duplicates; uniqueness, if desired (as is the case for several *)
(* geometric constructions), must be asserted separately. We do provide *)
(* shorthand, but only for cycles, because the equational properties of *)
(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *)
(* We define notations for the common cases of function paths, where the *)
(* progress relation is actually a function. In detail: *)
(* path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we *)
(* have e x_i x_{i+1} for all i < n. The path x :: p starts *)
(* at x and ends at last x p. *)
(* fpath f x p == x :: p is an f-path, where f is a function, i.e., p is of *)
(* the form [:: f x; f (f x); ...]. This is just a notation *)
(* for path (frel f) x p. *)
(* sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p *)
(* is an e-path (this is often used with e = leq or ltn). *)
(* cycle e c == c is an e-cycle: either c = [::], or c = x :: p with *)
(* x :: (rcons p x) an e-path. *)
(* fcycle f c == c is an f-cycle, for a function f. *)
(* traject f x n == the f-path of size n starting at x *)
(* := [:: x; f x; ...; iter n.-1 f x] *)
(* looping f x n == the f-paths of size greater than n starting at x loop *)
(* back, or, equivalently, traject f x n contains all *)
(* iterates of f at x. *)
(* merge e s1 s2 == the e-sorted merge of sequences s1 and s2: this is always *)
(* a permutation of s1 ++ s2, and is e-sorted when s1 and s2 *)
(* are and e is total. *)
(* sort e s == a permutation of the sequence s, that is e-sorted when e *)
(* is total (computed by a merge sort with the merge function *)
(* above). This sort function is also designed to be stable. *)
(* mem2 s x y == x, then y occur in the sequence (path) s; this is *)
(* non-strict: mem2 s x x = (x \in s). *)
(* next c x == the successor of the first occurrence of x in the sequence *)
(* c (viewed as a cycle), or x if x \notin c. *)
(* prev c x == the predecessor of the first occurrence of x in the *)
(* sequence c (viewed as a cycle), or x if x \notin c. *)
(* arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting *)
(* at the first occurrence of x in c, and ending just before *)
(* the next occurrence of y (in cycle order); arc c x y *)
(* returns an unspecified sub-arc of c if x and y do not both *)
(* occur in c. *)
(* ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) *)
(* ufcycle f c <-> c is a simple f-cycle, for a function f. *)
(* shorten x p == the tail a duplicate-free subpath of x :: p with the same *)
(* endpoints (x and last x p), obtained by removing all loops *)
(* from x :: p. *)
(* rel_base e e' h b <-> the function h is a functor from relation e to *)
(* relation e', EXCEPT at points whose image under h satisfy *)
(* the "base" predicate b: *)
(* e' (h x) (h y) = e x y UNLESS b (h x) holds *)
(* This is the statement of the side condition of the path *)
(* functorial mapping lemma map_path. *)
(* fun_base f f' h b <-> the function h is a functor from function f to f', *)
(* except at the preimage of predicate b under h. *)
(* We also provide three segmenting dependently-typed lemmas (splitP, splitPl *)
(* and splitPr) whose elimination split a path x0 :: p at an internal point x *)
(* as follows: *)
(* - splitP applies when x \in p; it replaces p with (rcons p1 x ++ p2), so *)
(* that x appears explicitly at the end of the left part. The elimination *)
(* of splitP will also simultaneously replace take (index x p) with p1 and *)
(* drop (index x p).+1 p with p2. *)
(* - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and *)
(* simultaneously generates an equation x = last x0 p1. *)
(* - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x *)
(* appears explicitly at the start of the right part. *)
(* The parts p1 and p2 are computed using index/take/drop in all cases, but *)
(* only splitP attempts to substitute the explicit values. The substitution *)
(* of p can be deferred using the dependent equation generation feature of *)
(* ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates *)
(* the equation p = p1 ++ p2 instead of performing the substitution outright. *)
(* Similarly, eliminating the loop removal lemma shortenP simultaneously *)
(* replaces shorten e x p with a fresh constant p', and last x p with *)
(* last x p'. *)
(* Note that although all "path" functions actually operate on the *)
(* underlying sequence, we provide a series of lemmas that define their *)
(* interaction with the path and cycle predicates, e.g., the cat_path equation*)
(* can be used to split the path predicate after splitting the underlying *)
(* sequence. *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Paths.
Variables (n0 : nat) (T : Type).
Section Path.
Variables (x0_cycle : T) (e : rel T).
Fixpoint path x (p : seq T) :=
if p is y :: p' then e x y && path y p' else true.
Lemma cat_path x p1 p2 : path x (p1 ++ p2) = path x p1 && path (last x p1) p2.
Proof. by elim: p1 x => [|y p1 Hrec] x //=; rewrite Hrec -!andbA. Qed.
Lemma rcons_path x p y : path x (rcons p y) = path x p && e (last x p) y.
Proof. by rewrite -cats1 cat_path /= andbT. Qed.
Lemma take_path x p i : path x p -> path x (take i p).
Proof. elim: p x i => [//| x p] IHp x' [//| i] /= /andP[-> ?]; exact: IHp. Qed.
Lemma pathP x p x0 :
reflect (forall i, i < size p -> e (nth x0 (x :: p) i) (nth x0 p i))
(path x p).
Proof.
elim: p x => [|y p IHp] x /=; first by left.
apply: (iffP andP) => [[e_xy /IHp e_p [] //] | e_p].
by split; [apply: (e_p 0) | apply/(IHp y) => i; apply: e_p i.+1].
Qed.
Definition cycle p := if p is x :: p' then path x (rcons p' x) else true.
Lemma cycle_path p : cycle p = path (last x0_cycle p) p.
Proof. by case: p => //= x p; rewrite rcons_path andbC. Qed.
Lemma cycle_catC p q : cycle (p ++ q) = cycle (q ++ p).
Proof.
case: p q => [|x p] [|y q]; rewrite /= ?cats0 //=.
by rewrite !rcons_path !cat_path !last_cat /= -!andbA; do !bool_congr.
Qed.
Lemma rot_cycle p : cycle (rot n0 p) = cycle p.
Proof. by rewrite cycle_catC cat_take_drop. Qed.
Lemma rotr_cycle p : cycle (rotr n0 p) = cycle p.
Proof. by rewrite -rot_cycle rotrK. Qed.
Definition sorted s := if s is x :: s' then path x s' else true.
Lemma sortedP s x :
reflect (forall i, i.+1 < size s -> e (nth x s i) (nth x s i.+1)) (sorted s).
Proof. by case: s => *; [constructor|apply: (iffP (pathP _ _ _)); apply]. Qed.
Lemma path_sorted x s : path x s -> sorted s.
Proof. by case: s => //= y s /andP[]. Qed.
Lemma path_min_sorted x s : all (e x) s -> path x s = sorted s.
Proof. by case: s => //= y s /andP [->]. Qed.
Lemma pairwise_sorted s : pairwise e s -> sorted s.
Proof. by elim: s => //= x s IHs /andP[/path_min_sorted -> /IHs]. Qed.
Lemma sorted_cat_cons s1 x s2 :
sorted (s1 ++ x :: s2) = sorted (rcons s1 x) && path x s2.
Proof.
by case: s1 => [ | e1 s1] //=; rewrite -cat_rcons cat_path last_rcons.
Qed.
End Path.
Section PathEq.
Variables (e e' : rel T).
Lemma rev_path x p :
path e (last x p) (rev (belast x p)) = path (fun z => e^~ z) x p.
Proof.
elim: p x => //= y p IHp x; rewrite rev_cons rcons_path -{}IHp andbC.
by rewrite -(last_cons x) -rev_rcons -lastI rev_cons last_rcons.
Qed.
Lemma rev_cycle p : cycle e (rev p) = cycle (fun z => e^~ z) p.
Proof.
case: p => //= x p; rewrite -rev_path last_rcons belast_rcons rev_cons.
by rewrite -[in LHS]cats1 cycle_catC.
Qed.
Lemma rev_sorted p : sorted e (rev p) = sorted (fun z => e^~ z) p.
Proof. by case: p => //= x p; rewrite -rev_path lastI rev_rcons. Qed.
Lemma path_relI x s :
path [rel x y | e x y && e' x y] x s = path e x s && path e' x s.
Proof. by elim: s x => //= y s IHs x; rewrite andbACA IHs. Qed.
Lemma cycle_relI s :
cycle [rel x y | e x y && e' x y] s = cycle e s && cycle e' s.
Proof. by case: s => [|? ?]; last apply: path_relI. Qed.
Lemma sorted_relI s :
sorted [rel x y | e x y && e' x y] s = sorted e s && sorted e' s.
Proof. by case: s; last apply: path_relI. Qed.
End PathEq.
Section SubPath_in.
Variable (P : {pred T}) (e e' : rel T).
Hypothesis (ee' : {in P &, subrel e e'}).
Lemma sub_in_path x s : all P (x :: s) -> path e x s -> path e' x s.
Proof.
by elim: s x => //= y s ihs x /and3P [? ? ?] /andP [/ee' -> //]; apply/ihs/andP.
Qed.
Lemma sub_in_cycle s : all P s -> cycle e s -> cycle e' s.
Proof.
case: s => //= x s /andP [Px Ps].
by apply: sub_in_path; rewrite /= all_rcons Px.
Qed.
Lemma sub_in_sorted s : all P s -> sorted e s -> sorted e' s.
Proof. by case: s => //; apply: sub_in_path. Qed.
End SubPath_in.
Section EqPath_in.
Variable (P : {pred T}) (e e' : rel T).
Hypothesis (ee' : {in P &, e =2 e'}).
Let e_e' : {in P &, subrel e e'}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed.
Let e'_e : {in P &, subrel e' e}. Proof. by move=> ? ? ? ?; rewrite ee'. Qed.
Lemma eq_in_path x s : all P (x :: s) -> path e x s = path e' x s.
Proof. by move=> Pxs; apply/idP/idP; apply: sub_in_path Pxs. Qed.
Lemma eq_in_cycle s : all P s -> cycle e s = cycle e' s.
Proof. by move=> Ps; apply/idP/idP; apply: sub_in_cycle Ps. Qed.
Lemma eq_in_sorted s : all P s -> sorted e s = sorted e' s.
Proof. by move=> Ps; apply/idP/idP; apply: sub_in_sorted Ps. Qed.
End EqPath_in.
Section SubPath.
Variables e e' : rel T.
Lemma sub_path : subrel e e' -> forall x p, path e x p -> path e' x p.
Proof. by move=> ? ? ?; apply/sub_in_path/all_predT; apply: in2W. Qed.
Lemma sub_cycle : subrel e e' -> subpred (cycle e) (cycle e').
Proof. by move=> ee' [] // ? ?; apply: sub_path. Qed.
Lemma sub_sorted : subrel e e' -> subpred (sorted e) (sorted e').
Proof. by move=> ee' [] //=; apply: sub_path. Qed.
Lemma eq_path : e =2 e' -> path e =2 path e'.
Proof. by move=> ? ? ?; apply/eq_in_path/all_predT; apply: in2W. Qed.
Lemma eq_cycle : e =2 e' -> cycle e =1 cycle e'.
Proof. by move=> ee' [] // ? ?; apply: eq_path. Qed.
Lemma eq_sorted : e =2 e' -> sorted e =1 sorted e'.
Proof. by move=> ee' [] // ? ?; apply: eq_path. Qed.
End SubPath.
Section Transitive_in.
Variables (P : {pred T}) (leT : rel T).
Lemma order_path_min_in x s :
{in P & &, transitive leT} -> all P (x :: s) -> path leT x s -> all (leT x) s.
Proof.
move=> leT_tr; elim: s => //= y s ihs /and3P [Px Py Ps] /andP [xy ys].
rewrite xy {}ihs ?Px //=; case: s Ps ys => //= z s /andP [Pz Ps] /andP [yz ->].
by rewrite (leT_tr _ _ _ Py Px Pz).
Qed.
Hypothesis leT_tr : {in P & &, transitive leT}.
Lemma path_sorted_inE x s :
all P (x :: s) -> path leT x s = all (leT x) s && sorted leT s.
Proof.
move=> Pxs; apply/idP/idP => [xs|/andP[/path_min_sorted<-//]].
by rewrite (order_path_min_in leT_tr) //; apply: path_sorted xs.
Qed.
Lemma sorted_pairwise_in s : all P s -> sorted leT s = pairwise leT s.
Proof.
by elim: s => //= x s IHs /andP [Px Ps]; rewrite path_sorted_inE ?IHs //= Px.
Qed.
Lemma path_pairwise_in x s :
all P (x :: s) -> path leT x s = pairwise leT (x :: s).
Proof. by move=> Pxs; rewrite -sorted_pairwise_in. Qed.
Lemma cat_sorted2 s s' : sorted leT (s ++ s') -> sorted leT s * sorted leT s'.
Proof. by case: s => //= x s; rewrite cat_path => /andP[-> /path_sorted]. Qed.
Lemma sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s).
Proof.
by move=> Ps; rewrite !sorted_pairwise_in ?all_mask //; exact: pairwise_mask.
Qed.
Lemma sorted_filter_in a s : all P s -> sorted leT s -> sorted leT (filter a s).
Proof. rewrite filter_mask; exact: sorted_mask_in. Qed.
Lemma path_mask_in x m s :
all P (x :: s) -> path leT x s -> path leT x (mask m s).
Proof. exact/(sorted_mask_in (true :: m)). Qed.
Lemma path_filter_in x a s :
all P (x :: s) -> path leT x s -> path leT x (filter a s).
Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed.
Lemma sorted_ltn_nth_in x0 s : all P s -> sorted leT s ->
{in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}.
Proof. by move=> Ps; rewrite sorted_pairwise_in //; apply/pairwiseP. Qed.
Hypothesis leT_refl : {in P, reflexive leT}.
Lemma sorted_leq_nth_in x0 s : all P s -> sorted leT s ->
{in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.
Proof.
move=> Ps s_sorted x y xs ys; rewrite leq_eqVlt=> /predU1P[->|].
exact/leT_refl/all_nthP.
exact: sorted_ltn_nth_in.
Qed.
End Transitive_in.
Section Transitive.
Variable (leT : rel T).
Lemma order_path_min x s : transitive leT -> path leT x s -> all (leT x) s.
Proof.
by move=> leT_tr; apply/order_path_min_in/all_predT => //; apply: in3W.
Qed.
Hypothesis leT_tr : transitive leT.
Lemma path_le x x' s : leT x x' -> path leT x' s -> path leT x s.
Proof.
by case: s => [//| x'' s xlex' /= /andP[x'lex'' ->]]; rewrite (leT_tr xlex').
Qed.
Let leT_tr' : {in predT & &, transitive leT}. Proof. exact: in3W. Qed.
Lemma path_sortedE x s : path leT x s = all (leT x) s && sorted leT s.
Proof. exact/path_sorted_inE/all_predT. Qed.
Lemma sorted_pairwise s : sorted leT s = pairwise leT s.
Proof. exact/sorted_pairwise_in/all_predT. Qed.
Lemma path_pairwise x s : path leT x s = pairwise leT (x :: s).
Proof. exact/path_pairwise_in/all_predT. Qed.
Lemma sorted_mask m s : sorted leT s -> sorted leT (mask m s).
Proof. exact/sorted_mask_in/all_predT. Qed.
Lemma sorted_filter a s : sorted leT s -> sorted leT (filter a s).
Proof. exact/sorted_filter_in/all_predT. Qed.
Lemma path_mask x m s : path leT x s -> path leT x (mask m s).
Proof. exact/path_mask_in/all_predT. Qed.
Lemma path_filter x a s : path leT x s -> path leT x (filter a s).
Proof. exact/path_filter_in/all_predT. Qed.
Lemma sorted_ltn_nth x0 s : sorted leT s ->
{in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> leT i j}}.
Proof. exact/sorted_ltn_nth_in/all_predT. Qed.
Hypothesis leT_refl : reflexive leT.
Lemma sorted_leq_nth x0 s : sorted leT s ->
{in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> leT i j}}.
Proof. exact/sorted_leq_nth_in/all_predT. Qed.
Lemma take_sorted n s : sorted leT s -> sorted leT (take n s).
Proof. by rewrite -[s in sorted _ s](cat_take_drop n) => /cat_sorted2[]. Qed.
Lemma drop_sorted n s : sorted leT s -> sorted leT (drop n s).
Proof. by rewrite -[s in sorted _ s](cat_take_drop n) => /cat_sorted2[]. Qed.
End Transitive.
End Paths.
Arguments pathP {T e x p}.
Arguments sortedP {T e s}.
Arguments path_sorted {T e x s}.
Arguments path_min_sorted {T e x s}.
Arguments order_path_min_in {T P leT x s}.
Arguments path_sorted_inE {T P leT} leT_tr {x s}.
Arguments sorted_pairwise_in {T P leT} leT_tr {s}.
Arguments path_pairwise_in {T P leT} leT_tr {x s}.
Arguments sorted_mask_in {T P leT} leT_tr {m s}.
Arguments sorted_filter_in {T P leT} leT_tr {a s}.
Arguments path_mask_in {T P leT} leT_tr {x m s}.
Arguments path_filter_in {T P leT} leT_tr {x a s}.
Arguments sorted_ltn_nth_in {T P leT} leT_tr x0 {s}.
Arguments sorted_leq_nth_in {T P leT} leT_tr leT_refl x0 {s}.
Arguments order_path_min {T leT x s}.
Arguments path_sortedE {T leT} leT_tr x s.
Arguments sorted_pairwise {T leT} leT_tr s.
Arguments path_pairwise {T leT} leT_tr x s.
Arguments sorted_mask {T leT} leT_tr m {s}.
Arguments sorted_filter {T leT} leT_tr a {s}.
Arguments path_mask {T leT} leT_tr {x} m {s}.
Arguments path_filter {T leT} leT_tr {x} a {s}.
Arguments sorted_ltn_nth {T leT} leT_tr x0 {s}.
Arguments sorted_leq_nth {T leT} leT_tr leT_refl x0 {s}.
Section HomoPath.
Variables (T T' : Type) (P : {pred T}) (f : T -> T') (e : rel T) (e' : rel T').
Lemma path_map x s : path e' (f x) (map f s) = path (relpre f e') x s.
Proof. by elim: s x => //= y s <-. Qed.
Lemma cycle_map s : cycle e' (map f s) = cycle (relpre f e') s.
Proof. by case: s => //= ? ?; rewrite -map_rcons path_map. Qed.
Lemma sorted_map s : sorted e' (map f s) = sorted (relpre f e') s.
Proof. by case: s; last apply: path_map. Qed.
Lemma homo_path_in x s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
all P (x :: s) -> path e x s -> path e' (f x) (map f s).
Proof. by move=> f_mono; rewrite path_map; apply: sub_in_path. Qed.
Lemma homo_cycle_in s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
all P s -> cycle e s -> cycle e' (map f s).
Proof. by move=> f_mono; rewrite cycle_map; apply: sub_in_cycle. Qed.
Lemma homo_sorted_in s : {in P &, {homo f : x y / e x y >-> e' x y}} ->
all P s -> sorted e s -> sorted e' (map f s).
Proof. by move=> f_mono; rewrite sorted_map; apply: sub_in_sorted. Qed.
Lemma mono_path_in x s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
all P (x :: s) -> path e' (f x) (map f s) = path e x s.
Proof. by move=> f_mono; rewrite path_map; apply: eq_in_path. Qed.
Lemma mono_cycle_in s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
all P s -> cycle e' (map f s) = cycle e s.
Proof. by move=> f_mono; rewrite cycle_map; apply: eq_in_cycle. Qed.
Lemma mono_sorted_in s : {in P &, {mono f : x y / e x y >-> e' x y}} ->
all P s -> sorted e' (map f s) = sorted e s.
Proof. by case: s => // x s; apply: mono_path_in. Qed.
Lemma homo_path x s : {homo f : x y / e x y >-> e' x y} ->
path e x s -> path e' (f x) (map f s).
Proof. by move=> f_homo; rewrite path_map; apply: sub_path. Qed.
Lemma homo_cycle : {homo f : x y / e x y >-> e' x y} ->
{homo map f : s / cycle e s >-> cycle e' s}.
Proof. by move=> f_homo s hs; rewrite cycle_map (sub_cycle _ hs). Qed.
Lemma homo_sorted : {homo f : x y / e x y >-> e' x y} ->
{homo map f : s / sorted e s >-> sorted e' s}.
Proof. by move/homo_path => ? []. Qed.
Lemma mono_path x s : {mono f : x y / e x y >-> e' x y} ->
path e' (f x) (map f s) = path e x s.
Proof. by move=> f_mon; rewrite path_map; apply: eq_path. Qed.
Lemma mono_cycle : {mono f : x y / e x y >-> e' x y} ->
{mono map f : s / cycle e s >-> cycle e' s}.
Proof. by move=> ? ?; rewrite cycle_map; apply: eq_cycle. Qed.
Lemma mono_sorted : {mono f : x y / e x y >-> e' x y} ->
{mono map f : s / sorted e s >-> sorted e' s}.
Proof. by move=> f_mon [] //= x s; apply: mono_path. Qed.
End HomoPath.
Arguments path_map {T T' f e'}.
Arguments cycle_map {T T' f e'}.
Arguments sorted_map {T T' f e'}.
Arguments homo_path_in {T T' P f e e' x s}.
Arguments homo_cycle_in {T T' P f e e' s}.
Arguments homo_sorted_in {T T' P f e e' s}.
Arguments mono_path_in {T T' P f e e' x s}.
Arguments mono_cycle_in {T T' P f e e' s}.
Arguments mono_sorted_in {T T' P f e e' s}.
Arguments homo_path {T T' f e e' x s}.
Arguments homo_cycle {T T' f e e'}.
Arguments homo_sorted {T T' f e e'}.
Arguments mono_path {T T' f e e' x s}.
Arguments mono_cycle {T T' f e e'}.
Arguments mono_sorted {T T' f e e'}.
Section CycleAll2Rel.
Lemma cycle_all2rel (T : Type) (leT : rel T) :
transitive leT -> forall s, cycle leT s = all2rel leT s.
Proof.
move=> leT_tr; elim=> //= x s IHs.
rewrite allrel_cons2 -{}IHs // (path_sortedE leT_tr) /= all_rcons -rev_sorted.
rewrite rev_rcons /= (path_sortedE (rev_trans leT_tr)) all_rev !andbA.
case: (boolP (leT x x && _ && _)) => //=.
case: s => //= y s /and3P[/and3P[_ xy _] yx sx].
rewrite rev_sorted rcons_path /= (leT_tr _ _ _ _ xy) ?andbT //.
by case: (lastP s) sx => //= {}s z; rewrite all_rcons last_rcons => /andP [->].
Qed.
Lemma cycle_all2rel_in (T : Type) (P : {pred T}) (leT : rel T) :
{in P & &, transitive leT} ->
forall s, all P s -> cycle leT s = all2rel leT s.
Proof.
move=> /in3_sig leT_tr _ /all_sigP [s ->].
by rewrite cycle_map allrel_mapl allrel_mapr; apply: cycle_all2rel.
Qed.
End CycleAll2Rel.
Section PreInSuffix.
Variables (T : eqType) (e : rel T).
Implicit Type s : seq T.
Local Notation path := (path e).
Local Notation sorted := (sorted e).
Lemma prefix_path x s1 s2 : prefix s1 s2 -> path x s2 -> path x s1.
Proof. by rewrite prefixE => /eqP <-; exact: take_path. Qed.
Lemma prefix_sorted s1 s2 : prefix s1 s2 -> sorted s2 -> sorted s1.
Proof. by rewrite prefixE => /eqP <-; exact: take_sorted. Qed.
Lemma infix_sorted s1 s2 : infix s1 s2 -> sorted s2 -> sorted s1.
Proof. by rewrite infixE => /eqP <- ?; apply/take_sorted/drop_sorted. Qed.
Lemma suffix_sorted s1 s2 : suffix s1 s2 -> sorted s2 -> sorted s1.
Proof. by rewrite suffixE => /eqP <-; exact: drop_sorted. Qed.
End PreInSuffix.
Section EqSorted.
Variables (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Local Notation path := (path leT).
Local Notation sorted := (sorted leT).
Lemma subseq_path_in x s1 s2 :
{in x :: s2 & &, transitive leT} -> subseq s1 s2 -> path x s2 -> path x s1.
Proof. by move=> tr /subseqP [m _ ->]; apply/(path_mask_in tr). Qed.
Lemma subseq_sorted_in s1 s2 :
{in s2 & &, transitive leT} -> subseq s1 s2 -> sorted s2 -> sorted s1.
Proof. by move=> tr /subseqP [m _ ->]; apply/(sorted_mask_in tr). Qed.
Lemma sorted_ltn_index_in s : {in s & &, transitive leT} -> sorted s ->
{in s &, forall x y, index x s < index y s -> leT x y}.
Proof.
case: s => // x0 s' leT_tr s_sorted x y xs ys.
move/(sorted_ltn_nth_in leT_tr x0 (allss (_ :: _)) s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.
Lemma sorted_leq_index_in s :
{in s & &, transitive leT} -> {in s, reflexive leT} -> sorted s ->
{in s &, forall x y, index x s <= index y s -> leT x y}.
Proof.
case: s => // x0 s' leT_tr leT_refl s_sorted x y xs ys.
move/(sorted_leq_nth_in leT_tr leT_refl x0 (allss (_ :: _)) s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.
Hypothesis leT_tr : transitive leT.
Lemma subseq_path x s1 s2 : subseq s1 s2 -> path x s2 -> path x s1.
Proof. by apply: subseq_path_in; apply: in3W. Qed.
Lemma subseq_sorted s1 s2 : subseq s1 s2 -> sorted s2 -> sorted s1.
Proof. by apply: subseq_sorted_in; apply: in3W. Qed.
Lemma sorted_uniq : irreflexive leT -> forall s, sorted s -> uniq s.
Proof. by move=> irr s; rewrite sorted_pairwise //; apply/pairwise_uniq. Qed.
Lemma sorted_eq : antisymmetric leT ->
forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.
Proof.
by move=> leT_asym s1 s2; rewrite !sorted_pairwise //; apply: pairwise_eq.
Qed.
Lemma irr_sorted_eq : irreflexive leT ->
forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2.
Proof.
move=> leT_irr s1 s2 s1_sort s2_sort eq_s12.
have: antisymmetric leT.
by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm.
by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq.
Qed.
Lemma sorted_ltn_index s :
sorted s -> {in s &, forall x y, index x s < index y s -> leT x y}.
Proof.
case: s => // x0 s' s_sorted x y xs ys /(sorted_ltn_nth leT_tr x0 s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.
Lemma undup_path x s : path x s -> path x (undup s).
Proof. exact/subseq_path/undup_subseq. Qed.
Lemma undup_sorted s : sorted s -> sorted (undup s).
Proof. exact/subseq_sorted/undup_subseq. Qed.
Hypothesis leT_refl : reflexive leT.
Lemma sorted_leq_index s :
sorted s -> {in s &, forall x y, index x s <= index y s -> leT x y}.
Proof.
case: s => // x0 s' s_sorted x y xs ys.
move/(sorted_leq_nth leT_tr leT_refl x0 s_sorted).
by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
Qed.
End EqSorted.
Arguments sorted_ltn_index_in {T leT s} leT_tr s_sorted.
Arguments sorted_leq_index_in {T leT s} leT_tr leT_refl s_sorted.
Arguments sorted_ltn_index {T leT} leT_tr {s}.
Arguments sorted_leq_index {T leT} leT_tr leT_refl {s}.
Section EqSorted_in.
Variables (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Lemma sorted_uniq_in s :
{in s & &, transitive leT} -> {in s, irreflexive leT} ->
sorted leT s -> uniq s.
Proof.
move=> /in3_sig leT_tr /in1_sig leT_irr; case/all_sigP: (allss s) => s' ->.
by rewrite sorted_map (map_inj_uniq val_inj); exact: sorted_uniq.
Qed.
Lemma sorted_eq_in s1 s2 :
{in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} ->
sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2.
Proof.
move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti + + /[dup] s1s2.
have /all_sigP[s1' ->] := allss s1.
have /all_sigP[{s1s2}s2 ->] : all [in s1] s2 by rewrite -(perm_all _ s1s2).
by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->.
Qed.
Lemma irr_sorted_eq_in s1 s2 :
{in s1 & &, transitive leT} -> {in s1, irreflexive leT} ->
sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2.
Proof.
move=> /in3_sig leT_tr /in1_sig leT_irr + + /[dup] s1s2.
have /all_sigP[s1' ->] := allss s1.
have /all_sigP[s2' ->] : all [in s1] s2 by rewrite -(eq_all_r s1s2).
rewrite !sorted_map => ss1' ss2' {}s1s2; congr map.
by apply: (irr_sorted_eq leT_tr) => // x; rewrite -!(mem_map val_inj).
Qed.
End EqSorted_in.
Section EqPath.
Variables (n0 : nat) (T : eqType) (e : rel T).
Implicit Type p : seq T.
Variant split x : seq T -> seq T -> seq T -> Type :=
Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.
Lemma splitP p x (i := index x p) :
x \in p -> split x p (take i p) (drop i.+1 p).
Proof. by rewrite -has_pred1 => /split_find[? ? ? /eqP->]; constructor. Qed.
Variant splitl x1 x : seq T -> Type :=
Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2).
Lemma splitPl x1 p x : x \in x1 :: p -> splitl x1 x p.
Proof.
rewrite inE; case: eqP => [->| _ /splitP[]]; first by rewrite -(cat0s p).
by split; apply: last_rcons.
Qed.
Variant splitr x : seq T -> Type :=
Splitr p1 p2 : splitr x (p1 ++ x :: p2).
Lemma splitPr p x : x \in p -> splitr x p.
Proof. by case/splitP=> p1 p2; rewrite cat_rcons. Qed.
Fixpoint next_at x y0 y p :=
match p with
| [::] => if x == y then y0 else x
| y' :: p' => if x == y then y' else next_at x y0 y' p'
end.
Definition next p x := if p is y :: p' then next_at x y y p' else x.
Fixpoint prev_at x y0 y p :=
match p with
| [::] => if x == y0 then y else x
| y' :: p' => if x == y' then y else prev_at x y0 y' p'
end.
Definition prev p x := if p is y :: p' then prev_at x y y p' else x.
Lemma next_nth p x :
next p x = if x \in p then
if p is y :: p' then nth y p' (index x p) else x
else x.
Proof.
case: p => //= y0 p.
elim: p {2 3 5}y0 => [|y' p IHp] y /=; rewrite (eq_sym y) inE;
by case: ifP => // _; apply: IHp.
Qed.
Lemma prev_nth p x :
prev p x = if x \in p then
if p is y :: p' then nth y p (index x p') else x
else x.
Proof.
case: p => //= y0 p; rewrite inE orbC.
elim: p {2 5}y0 => [|y' p IHp] y; rewrite /= ?inE // (eq_sym y').
by case: ifP => // _; apply: IHp.
Qed.
Lemma mem_next p x : (next p x \in p) = (x \in p).
Proof.
rewrite next_nth; case p_x: (x \in p) => //.
case: p (index x p) p_x => [|y0 p'] //= i _; rewrite inE.
have [lt_ip | ge_ip] := ltnP i (size p'); first by rewrite orbC mem_nth.
by rewrite nth_default ?eqxx.
Qed.
Lemma mem_prev p x : (prev p x \in p) = (x \in p).
Proof.
rewrite prev_nth; case p_x: (x \in p) => //; case: p => [|y0 p] // in p_x *.
by apply mem_nth; rewrite /= ltnS index_size.
Qed.
(* ucycleb is the boolean predicate, but ucycle is defined as a Prop *)
(* so that it can be used as a coercion target. *)
Definition ucycleb p := cycle e p && uniq p.
Definition ucycle p : Prop := cycle e p && uniq p.
(* Projections, used for creating local lemmas. *)
Lemma ucycle_cycle p : ucycle p -> cycle e p.
Proof. by case/andP. Qed.
Lemma ucycle_uniq p : ucycle p -> uniq p.
Proof. by case/andP. Qed.
Lemma next_cycle p x : cycle e p -> x \in p -> e x (next p x).
Proof.
case: p => //= y0 p; elim: p {1 3 5}y0 => [|z p IHp] y /=; rewrite inE.
by rewrite andbT; case: (x =P y) => // ->.
by case/andP=> eyz /IHp; case: (x =P y) => // ->.
Qed.
Lemma prev_cycle p x : cycle e p -> x \in p -> e (prev p x) x.
Proof.
case: p => //= y0 p; rewrite inE orbC.
elim: p {1 5}y0 => [|z p IHp] y /=; rewrite ?inE.
by rewrite andbT; case: (x =P y0) => // ->.
by case/andP=> eyz /IHp; case: (x =P z) => // ->.
Qed.
Lemma rot_ucycle p : ucycle (rot n0 p) = ucycle p.
Proof. by rewrite /ucycle rot_uniq rot_cycle. Qed.
Lemma rotr_ucycle p : ucycle (rotr n0 p) = ucycle p.
Proof. by rewrite /ucycle rotr_uniq rotr_cycle. Qed.
(* The "appears no later" partial preorder defined by a path. *)
Definition mem2 p x y := y \in drop (index x p) p.
Lemma mem2l p x y : mem2 p x y -> x \in p.
Proof.
by rewrite /mem2 -!index_mem size_drop ltn_subRL; apply/leq_ltn_trans/leq_addr.
Qed.
Lemma mem2lf {p x y} : x \notin p -> mem2 p x y = false.
Proof. exact/contraNF/mem2l. Qed.
Lemma mem2r p x y : mem2 p x y -> y \in p.
Proof.
by rewrite -[in y \in p](cat_take_drop (index x p) p) mem_cat orbC /mem2 => ->.
Qed.
Lemma mem2rf {p x y} : y \notin p -> mem2 p x y = false.
Proof. exact/contraNF/mem2r. Qed.
Lemma mem2_cat p1 p2 x y :
mem2 (p1 ++ p2) x y = mem2 p1 x y || mem2 p2 x y || (x \in p1) && (y \in p2).
Proof.
rewrite [LHS]/mem2 index_cat fun_if if_arg !drop_cat addKn.
case: ifPn => [p1x | /mem2lf->]; last by rewrite ltnNge leq_addr orbF.
by rewrite index_mem p1x mem_cat -orbA (orb_idl (@mem2r _ _ _)).
Qed.
Lemma mem2_splice p1 p3 x y p2 :
mem2 (p1 ++ p3) x y -> mem2 (p1 ++ p2 ++ p3) x y.
Proof.
by rewrite !mem2_cat mem_cat andb_orr orbC => /or3P[]->; rewrite ?orbT.
Qed.
Lemma mem2_splice1 p1 p3 x y z :
mem2 (p1 ++ p3) x y -> mem2 (p1 ++ z :: p3) x y.
Proof. exact: mem2_splice [::z]. Qed.
Lemma mem2_cons x p y z :
mem2 (x :: p) y z = (if x == y then z \in x :: p else mem2 p y z).
Proof. by rewrite [LHS]/mem2 /=; case: ifP. Qed.
Lemma mem2_seq1 x y z : mem2 [:: x] y z = (y == x) && (z == x).
Proof. by rewrite mem2_cons eq_sym inE. Qed.
Lemma mem2_last y0 p x : mem2 p x (last y0 p) = (x \in p).
Proof.
apply/idP/idP; first exact: mem2l; rewrite -index_mem /mem2 => p_x.
by rewrite -nth_last -(subnKC p_x) -nth_drop mem_nth // size_drop subnSK.
Qed.
Lemma mem2l_cat {p1 p2 x} : x \notin p1 -> mem2 (p1 ++ p2) x =1 mem2 p2 x.
Proof. by move=> p1'x y; rewrite mem2_cat (negPf p1'x) mem2lf ?orbF. Qed.
Lemma mem2r_cat {p1 p2 x y} : y \notin p2 -> mem2 (p1 ++ p2) x y = mem2 p1 x y.
Proof.
by move=> p2'y; rewrite mem2_cat (negPf p2'y) -orbA orbC andbF mem2rf.
Qed.
Lemma mem2lr_splice {p1 p2 p3 x y} :
x \notin p2 -> y \notin p2 -> mem2 (p1 ++ p2 ++ p3) x y = mem2 (p1 ++ p3) x y.
Proof.
move=> p2'x p2'y; rewrite catA !mem2_cat !mem_cat.
by rewrite (negPf p2'x) (negPf p2'y) (mem2lf p2'x) andbF !orbF.
Qed.
Lemma mem2E s x y :
mem2 s x y = subseq (if x == y then [:: x] else [:: x; y]) s.
Proof.
elim: s => [| h s]; first by case: ifP.
rewrite mem2_cons => ->.
do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=.
by have [->|] := eqVneq; case: eqVneq.
Qed.
Variant split2r x y : seq T -> Type :=
Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2).
Lemma splitP2r p x y : mem2 p x y -> split2r x y p.
Proof.
move=> pxy; have px := mem2l pxy.
have:= pxy; rewrite /mem2 (drop_nth x) ?index_mem ?nth_index //.
by case/splitP: px => p1 p2; rewrite cat_rcons.
Qed.
Fixpoint shorten x p :=
if p is y :: p' then
if x \in p then shorten x p' else y :: shorten y p'
else [::].
Variant shorten_spec x p : T -> seq T -> Type :=
ShortenSpec p' of path e x p' & uniq (x :: p') & {subset p' <= p} :
shorten_spec x p (last x p') p'.
Lemma shortenP x p : path e x p -> shorten_spec x p (last x p) (shorten x p).
Proof.
move=> e_p; have: x \in x :: p by apply: mem_head.
elim: p x {1 3 5}x e_p => [|y2 p IHp] x y1.
by rewrite mem_seq1 => _ /eqP->.
rewrite inE orbC /= => /andP[ey12 {}/IHp IHp].
case: ifPn => [y2p_x _ | not_y2p_x /eqP def_x].
have [p' e_p' Up' p'p] := IHp _ y2p_x.
by split=> // y /p'p; apply: predU1r.
have [p' e_p' Up' p'p] := IHp y2 (mem_head y2 p).
have{} p'p z: z \in y2 :: p' -> z \in y2 :: p.
by rewrite !inE; case: (z == y2) => // /p'p.
rewrite -(last_cons y1) def_x; split=> //=; first by rewrite ey12.
by rewrite (contra (p'p y1)) -?def_x.
Qed.
End EqPath.
(* Ordered paths and sorting. *)
Section SortSeq.
Variables (T : Type) (leT : rel T).
Fixpoint merge s1 :=
if s1 is x1 :: s1' then
let fix merge_s1 s2 :=
if s2 is x2 :: s2' then
if leT x1 x2 then x1 :: merge s1' s2 else x2 :: merge_s1 s2'
else s1 in
merge_s1
else id.
Arguments merge !s1 !s2 : rename.
Fixpoint merge_sort_push s1 ss :=
match ss with
| [::] :: ss' | [::] as ss' => s1 :: ss'
| s2 :: ss' => [::] :: merge_sort_push (merge s2 s1) ss'
end.
Fixpoint merge_sort_pop s1 ss :=
if ss is s2 :: ss' then merge_sort_pop (merge s2 s1) ss' else s1.
Fixpoint merge_sort_rec ss s :=
if s is [:: x1, x2 & s'] then
let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
merge_sort_rec (merge_sort_push s1 ss) s'
else merge_sort_pop s ss.
Definition sort := merge_sort_rec [::].
(* The following definition `sort_rec1` is an auxiliary function for *)
(* inductive reasoning on `sort`. One can rewrite `sort le s` to *)
(* `sort_rec1 le [::] s` by `sortE` and apply the simple structural induction *)
(* on `s` to reason about it. *)
Fixpoint sort_rec1 ss s :=
if s is x :: s then sort_rec1 (merge_sort_push [:: x] ss) s else
merge_sort_pop [::] ss.
Lemma sortE s : sort s = sort_rec1 [::] s.
Proof.
transitivity (sort_rec1 [:: nil] s); last by case: s.
rewrite /sort; move: [::] {2}_.+1 (ltnSn (size s)./2) => ss n.
by elim: n => // n IHn in ss s *; case: s => [|x [|y s]] //= /IHn->.
Qed.
Lemma count_merge (p : pred T) s1 s2 :
count p (merge s1 s2) = count p (s1 ++ s2).
Proof.
rewrite count_cat; elim: s1 s2 => // x s1 IH1.
elim=> //= [|y s2 IH2]; first by rewrite addn0.
by case: leT; rewrite /= ?IH1 ?IH2 !addnA [_ + p y]addnAC [p x + p y]addnC.
Qed.
Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2).
Proof. exact: (count_merge predT). Qed.
Lemma allrel_merge s1 s2 : allrel leT s1 s2 -> merge s1 s2 = s1 ++ s2.
Proof.
elim: s1 s2 => [|x s1 IHs1] [|y s2]; rewrite ?cats0 //=.
by rewrite allrel_consl /= -andbA => /and3P [-> _ /IHs1->].
Qed.
Lemma count_sort (p : pred T) s : count p (sort s) = count p s.
Proof.
rewrite sortE -[RHS]/(sumn [seq count p x | x <- [::]] + count p s).
elim: s [::] => [|x s ihs] ss.
rewrite [LHS]/=; elim: ss [::] => //= s ss ihss t.
by rewrite ihss count_merge count_cat addnCA addnA.
rewrite {}ihs -[in RHS]cat1s count_cat addnA; congr addn; rewrite addnC.
elim: {x s} ss [:: x] => [|[|x s] ss ihss] t //.
by rewrite [LHS]/= add0n ihss count_merge count_cat -addnA addnCA.
Qed.
Lemma pairwise_sort s : pairwise leT s -> sort s = s.
Proof.
pose catss := foldr (fun x => cat ^~ x) (Nil T).
rewrite -{1 3}[s]/(catss [::] ++ s) sortE; elim: s [::] => /= [|x s ihs] ss.
elim: ss [::] => //= s ss ihss t; rewrite -catA => ssst.
rewrite -ihss ?allrel_merge //; move: ssst; rewrite !pairwise_cat.
by case/and4P.
rewrite (catA _ [:: _]) => ssxs.
suff x_ss_E: catss (merge_sort_push [:: x] ss) = catss ([:: x] :: ss).
by rewrite -[catss _ ++ _]/(catss ([:: x] :: ss)) -x_ss_E ihs // x_ss_E.
move: ssxs; rewrite pairwise_cat => /and3P [_ + _].
elim: ss [:: x] => {x s ihs} //= -[|x s] ss ihss t h_pairwise;
rewrite /= cats0 // allrel_merge ?ihss ?catA //.
by move: h_pairwise; rewrite -catA !pairwise_cat => /and4P [].
Qed.
Remark size_merge_sort_push s1 :
let graded ss := forall i, size (nth [::] ss i) \in pred2 0 (2 ^ (i + 1)) in
size s1 = 2 -> {homo merge_sort_push s1 : ss / graded ss}.
Proof.
set n := {2}1; rewrite -[RHS]/(2 ^ n) => graded sz_s1 ss.
elim: ss => [|s2 ss IHss] in (n) graded s1 sz_s1 * => sz_ss i //=.
by case: i => [|[]] //; rewrite sz_s1 inE eqxx orbT.
case: s2 i => [|x s2] [|i] //= in sz_ss *; first by rewrite sz_s1 inE eqxx orbT.
exact: (sz_ss i.+1).
rewrite addSnnS; apply: IHss i => [|i]; last by rewrite -addSnnS (sz_ss i.+1).
by rewrite size_merge size_cat sz_s1 (eqP (sz_ss 0)) addnn expnS mul2n.
Qed.
Section Stability.
Variable leT' : rel T.
Hypothesis (leT_total : total leT) (leT'_tr : transitive leT').
Let leT_lex := [rel x y | leT x y && (leT y x ==> leT' x y)].
Lemma merge_stable_path x s1 s2 :
allrel leT' s1 s2 -> path leT_lex x s1 -> path leT_lex x s2 ->