-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSpecial.v
1731 lines (1594 loc) · 62.9 KB
/
Special.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
Require Import MoreFun MoreList DeltaList GenFib GenG Words WordFactor.
Import ListNotations.
(** * Study of Left-Special words of [qseq q] *)
(** Especially, for all length p, [qseq q] has a unique left-special word,
namely its initial prefix of length p.
This is a particular case of this article + its Corrigendum :
Complexity of Infinite Words Associated with Beta-expansions,
C. Frougny, Z. Masáková, E. Pelantová, 2004.
*)
Definition LeftExt a u (f:sequence) := SubSeq (a::u) f.
Definition LeftSpecial u (f:sequence) :=
exists a a', a<>a' /\ LeftExt a u f /\ LeftExt a' u f.
Definition RightExt u a (f:sequence) := SubSeq (u++[a]) f.
Definition RightSpecial u (f:sequence) :=
exists a a', a<>a' /\ RightExt u a f /\ RightExt u a' f.
Definition AllLeftExts l u (f:sequence) :=
NoDup l /\ forall a, In a l <-> LeftExt a u f.
Definition AllRightExts u l (f:sequence) :=
NoDup l /\ forall a, In a l <-> RightExt u a f.
Lemma AllLeftExts_unique l l' u f :
AllLeftExts l u f -> AllLeftExts l' u f -> Permutation l l'.
Proof.
intros (ND,IN) (ND',IN').
apply NoDup_Permutation; trivial.
intros. now rewrite IN, IN'.
Qed.
Lemma AllRightExts_unique l l' u f :
AllRightExts u l f -> AllRightExts u l' f -> Permutation l l'.
Proof.
intros (ND,IN) (ND',IN').
apply NoDup_Permutation; trivial.
intros. now rewrite IN, IN'.
Qed.
Lemma LeftExt_letter q a u : LeftExt a u (qseq q) -> a <= q.
Proof.
unfold LeftExt, SubSeq. intros (p, E). unfold subseq in E.
simpl in E. injection E as E _.
generalize (qseq_letters q p). lia.
Qed.
Lemma RightExt_letter q u a : RightExt u a (qseq q) -> a <= q.
Proof.
unfold RightExt, SubSeq. intros (p, E). revert E.
unfold subseq. rewrite app_length. simpl.
rewrite Nat.add_succ_r, seq_S, map_app. simpl. intros E.
apply app_inv' in E; trivial. destruct E as (_,[= ->]).
apply qseq_letters.
Qed.
Lemma LeftExt_Prefix a u v f :
Prefix v u -> LeftExt a u f -> LeftExt a v f.
Proof.
unfold LeftExt. intros PR SU. eapply Sub_SubSeq; eauto.
now apply Prefix_Sub, Prefix_cons.
Qed.
Lemma RightExt_Suffix a u v f :
Suffix v u -> RightExt u a f -> RightExt v a f.
Proof.
unfold RightExt. intros SU SU'. eapply Sub_SubSeq; eauto.
now apply Suffix_Sub, Suffix_app_r.
Qed.
Lemma SubSeq_RightExt u f : SubSeq u f -> exists a, RightExt u a f.
Proof.
unfold RightExt, SubSeq.
intros (q, ->). exists (f (q+length u)), q.
unfold subseq. rewrite app_length, map_length, seq_length. simpl.
rewrite Nat.add_succ_r, seq_S, map_app. simpl. repeat f_equal; lia.
Qed.
Lemma LeftSpecial_Prefix u v f :
Prefix u v -> LeftSpecial v f -> LeftSpecial u f.
Proof.
intros P (a & b & AB & A & B).
exists a, b; repeat split; eauto using LeftExt_Prefix.
Qed.
Lemma RightSpecial_Suffix u v f :
Suffix u v -> RightSpecial v f -> RightSpecial u f.
Proof.
intros P (a & b & AB & A & B).
exists a, b; repeat split; eauto using RightExt_Suffix.
Qed.
Lemma LeftSpecial_SubSeq u f : LeftSpecial u f -> SubSeq u f.
Proof.
intros (a & _ & _ & A & _). eapply Sub_SubSeq; eauto. apply Sub_cons_r.
Qed.
Lemma RightSpecial_SubSeq u f : RightSpecial u f -> SubSeq u f.
Proof.
intros (a & _ & _ & A & _). eapply Sub_SubSeq; eauto.
apply Sub_app_r, Sub_id.
Qed.
(** Computing the left and right extensions, thanks to qfactors
(not meant to be efficient).
The number of extensions is named the (left and right) valence
of the factor. *)
Definition wordmem u l := existsb (listnat_eqb u) l.
Lemma wordmem_spec u l : wordmem u l = true <-> In u l.
Proof.
unfold wordmem. rewrite existsb_exists. split.
- intros (x & IN & E). revert E.
case listnat_eqb_spec. now intros ->. easy.
- intros IN. exists u. split; trivial. now case listnat_eqb_spec.
Qed.
Definition qleftexts q u :=
let l := qfactors0opt q (S (length u)) in
filter (fun a => wordmem (a::u) l) (seq 0 (S q)).
Definition qlvalence q (u:word) := length (qleftexts q u).
Definition qrightexts q u :=
let l := qfactors0opt q (S (length u)) in
filter (fun a => wordmem (u++[a]) l) (seq 0 (S q)).
Definition qrvalence q (u:word) := length (qrightexts q u).
Lemma qleftexts_ok q u : AllLeftExts (qleftexts q u) u (qseq q).
Proof.
split.
- apply NoDup_filter, seq_NoDup.
- intros a.
unfold qleftexts.
rewrite filter_In, in_seq, wordmem_spec, qfactors0opt_in.
split.
+ intros (_ & _ & SU). apply SU.
+ unfold LeftExt. intros SU. split; [|split]; trivial.
red in SU. destruct SU as (p & E). unfold subseq in E. simpl in E.
injection E as E _. generalize (qseq_letters q p); lia.
Qed.
Lemma qrightexts_ok q u : AllRightExts u (qrightexts q u) (qseq q).
Proof.
split.
- apply NoDup_filter, seq_NoDup.
- intros a.
unfold qrightexts.
rewrite filter_In, in_seq, wordmem_spec, qfactors0opt_in.
split.
+ intros (_ & _ & SU). apply SU.
+ unfold RightExt. intros SU. split; [|split]; trivial.
2:{ rewrite app_length; simpl; lia. }
red in SU. destruct SU as (p & E). unfold subseq in E.
rewrite app_length in E. simpl in *.
rewrite Nat.add_succ_r, seq_S, map_app in E. simpl in E.
apply app_inv' in E; trivial. destruct E as (_,E).
injection E as E. generalize (qseq_letters q (p+(length u+0))); lia.
Qed.
Lemma qlvalence_ok q l u :
AllLeftExts l u (qseq q) -> qlvalence q u = length l.
Proof.
intros A. rewrite (@Permutation_length _ l (qleftexts q u)); try easy.
eapply AllLeftExts_unique; eauto using qleftexts_ok.
Qed.
Lemma qrvalence_ok q u l :
AllRightExts u l (qseq q) -> qrvalence q u = length l.
Proof.
intros A. rewrite (@Permutation_length _ l (qrightexts q u)); try easy.
eapply AllRightExts_unique; eauto using qrightexts_ok.
Qed.
Lemma qword_ls q p a : a <= q -> LeftExt a (qword q p) (qseq q).
Proof.
intros Ha.
set (r := a + p + S q - p mod S q).
assert (p <= r).
{ generalize (Nat.mod_upper_bound p (S q)). lia. }
assert (E : r mod S q = a).
{ unfold r. replace (a+p+S q) with (a+S q+p) by lia.
rewrite (Nat.div_mod_eq p (S q)) at 1 by lia.
rewrite Nat.add_assoc, Nat.add_sub.
rewrite Nat.mul_comm, Nat.mod_add by lia.
replace (S q) with (1 * S q) at 1 by lia. rewrite Nat.mod_add by lia.
apply Nat.mod_small; lia. }
apply LeftExt_Prefix with (qword q (r+2)).
- apply qword_le_prefix; lia.
- assert (SU : SubSeq (qword q (r+2+S q)) (qseq q)).
{ rewrite SubSeq_qseq_alt. exists (r+2+S q). apply Sub_id. }
rewrite Nat.add_succ_r, qword_eqn in SU by lia.
replace (r+2+q-q) with (r+2) in SU by lia.
rewrite (@app_removelast_last _ (qword q (r+2+q)) 0) in SU.
2:{ apply qword_nz. }
rewrite <- app_assoc in SU.
rewrite WordSuffix.qword_last in SU.
replace (r+2+q+q) with (r+2*(S q)) in SU by lia.
rewrite Nat.mod_add, E in SU by lia.
red. eapply Sub_SubSeq; eauto. apply Sub_app_l, Sub_id.
Qed.
Lemma qprefix_leftext q n a : a <= q -> LeftExt a (qprefix q n) (qseq q).
Proof.
intros Ha.
rewrite qprefix_alt.
set (p := invA_up q n).
apply LeftExt_Prefix with (qword q p).
- rewrite Prefix_equiv. f_equal. rewrite firstn_length_le; trivial.
rewrite qword_len. apply invA_up_spec.
- now apply qword_ls.
Qed.
Lemma qprefix_allleftexts q n :
AllLeftExts (seq 0 (S q)) (qprefix q n) (qseq q).
Proof.
split.
- apply seq_NoDup.
- intros a. rewrite in_seq. split.
+ intros Ha. apply qprefix_leftext. lia.
+ intros Ha. apply LeftExt_letter in Ha. lia.
Qed.
Lemma qprefix_qlvalence q n : qlvalence q (qprefix q n) = S q.
Proof.
rewrite <- (seq_length (S q) 0). apply qlvalence_ok.
apply qprefix_allleftexts.
Qed.
Lemma qseq_leftext q u : SubSeq u (qseq q) -> exists a, LeftExt a u (qseq q).
Proof.
rewrite SubSeq_qseq_alt; intros (n, (v & w & E)).
rewrite <- (rev_involutive v) in E.
destruct (rev v) as [|a v']; simpl in E.
- exists 0. replace u with (qprefix q (length u)).
+ apply qprefix_leftext; lia.
+ symmetry. change (PrefixSeq u (qseq q)).
eapply Prefix_PrefixSeq.
* now exists w.
* rewrite E. apply qword_prefixseq.
- exists a. red. rewrite SubSeq_qseq_alt. exists n.
rewrite <- E, <- !app_assoc. simpl. now do 2 eexists.
Qed.
Lemma qlvalence_nz q u : SubSeq u (qseq q) -> qlvalence q u <> 0.
Proof.
intros Hu.
unfold qlvalence. rewrite length_zero_iff_nil.
destruct (qseq_leftext q u Hu) as (a & Ha).
destruct (qleftexts_ok q u) as (ND,H). rewrite <- H in Ha.
intros E. now rewrite E in Ha.
Qed.
Lemma qrvalence_nz q u : SubSeq u (qseq q) -> qrvalence q u <> 0.
Proof.
intros Hu.
unfold qrvalence. rewrite length_zero_iff_nil.
destruct (SubSeq_RightExt u _ Hu) as (a & Ha).
destruct (qrightexts_ok q u) as (ND,H). rewrite <- H in Ha.
intros E. now rewrite E in Ha.
Qed.
Lemma qlvalence_le_Sq q u : qlvalence q u <= S q.
Proof.
unfold qlvalence, qleftexts.
rewrite <- (seq_length (S q) 0) at 2. apply filter_length_le.
Qed.
Lemma qrvalence_le_Sq q u : qrvalence q u <= S q.
Proof.
unfold qrvalence, qrightexts.
rewrite <- (seq_length (S q) 0) at 2. apply filter_length_le.
Qed.
Lemma prefix_incl_allleftexts q u u' l l' :
Prefix u u' -> AllLeftExts l u (qseq q) -> AllLeftExts l' u' (qseq q) ->
incl l' l.
Proof.
intros P (ND,Hu) (ND',Hu') a Ha. rewrite Hu' in Ha. apply Hu.
eapply LeftExt_Prefix; eauto.
Qed.
Lemma prefix_qlvalence q u v : Prefix u v -> qlvalence q v <= qlvalence q u.
Proof.
intros P. unfold qlvalence. apply NoDup_incl_length.
- apply qleftexts_ok.
- eapply prefix_incl_allleftexts; eauto using qleftexts_ok.
Qed.
Lemma suffix_incl_allrightexts q u u' l l' :
Suffix u u' -> AllRightExts u l (qseq q) -> AllRightExts u' l' (qseq q) ->
incl l' l.
Proof.
intros P (ND,Hu) (ND',Hu') a Ha. rewrite Hu' in Ha. apply Hu.
eapply RightExt_Suffix; eauto.
Qed.
Lemma suffix_qrvalence q u v : Suffix u v -> qrvalence q v <= qrvalence q u.
Proof.
intros P. unfold qrvalence. apply NoDup_incl_length.
- apply qrightexts_ok.
- eapply suffix_incl_allrightexts; eauto using qrightexts_ok.
Qed.
Lemma ls_val q u : LeftSpecial u (qseq q) <-> 2 <= qlvalence q u.
Proof.
split.
- intros (a & b & NE & Ha & Hb).
unfold qlvalence.
assert (H := qleftexts_ok q u). destruct H as (_,H).
rewrite <- H in Ha, Hb. eapply lengthge2_carac; eauto.
- unfold qlvalence.
assert (H := qleftexts_ok q u). destruct H as (ND,H).
destruct (qleftexts q u) as [|a [|b l]] eqn:E; simpl; try lia.
intros _. exists a, b; repeat split.
+ inversion_clear ND; simpl in *; intuition.
+ apply H; simpl; intuition.
+ apply H; simpl; intuition.
Qed.
Lemma rs_val q u : RightSpecial u (qseq q) <-> 2 <= qrvalence q u.
Proof.
split.
- intros (a & b & NE & Ha & Hb).
unfold qrvalence.
assert (H := qrightexts_ok q u). destruct H as (_,H).
rewrite <- H in Ha, Hb. eapply lengthge2_carac; eauto.
- unfold qrvalence.
assert (H := qrightexts_ok q u). destruct H as (ND,H).
destruct (qrightexts q u) as [|a [|b l]] eqn:E; simpl; try lia.
intros _. exists a, b; repeat split.
+ inversion_clear ND; simpl in *; intuition.
+ apply H; simpl; intuition.
+ apply H; simpl; intuition.
Qed.
(** Valence of letters *)
Lemma all_letters_subseq q a : a <= q <-> SubSeq [a] (qseq q).
Proof.
split.
- intros Ha. exists (S a). simpl. unfold subseq. simpl.
now rewrite all_letters_occur.
- apply LeftExt_letter.
Qed.
Lemma ls_head_q q a u : LeftSpecial (a::u) (qseq q) -> a = q.
Proof.
intros (b & c & N & (p,Hb) & (r,Hc)).
unfold subseq in *. simpl in *.
injection Hb as Hb Hb' _.
injection Hc as Hc Hc' _.
destruct (Nat.eq_dec a q) as [A|A]; trivial. exfalso.
assert (b = prev_letter q a).
{ rewrite Hb, Hb'. rewrite <- (qseq_prev_letter q (S p)) by lia.
f_equal; lia. }
assert (c = prev_letter q a).
{ rewrite Hc, Hc'. rewrite <- (qseq_prev_letter q (S r)) by lia.
f_equal; lia. }
lia.
Qed.
Lemma ls_qnz q u : LeftSpecial u (qseq q) -> q<>0.
Proof.
intros (a & b & AB & A & B). apply LeftExt_letter in A,B. lia.
Qed.
Lemma ls_head_nz q a u : LeftSpecial (a::u) (qseq q) -> a <> 0.
Proof.
intros LS. rewrite (ls_head_q _ _ _ LS). now apply ls_qnz in LS.
Qed.
Lemma AllRightExts_qm1 q : AllRightExts [q-1] [q] (qseq q).
Proof.
split.
- repeat constructor. intuition.
- intros a. simpl. split; [intros [<-|[ ]] | intros R; left].
+ exists q. unfold subseq. simpl. symmetry. f_equal.
* destruct (Nat.eq_dec q 0) as [->|Q]. easy.
replace q with (S (q-1)) at 2 by lia.
apply all_letters_occur; lia.
* f_equal. now apply all_letters_occur.
+ destruct R as (p,R). unfold subseq in R. simpl in R.
injection R as R ->. symmetry. now apply qseq_next_qm1.
Qed.
Lemma qrvalence_qm1 q : qrvalence q [q-1] = 1.
Proof.
change 1 with (length [q]) at 2. apply qrvalence_ok. apply AllRightExts_qm1.
Qed.
Lemma qrvalence_last_qm1 q u :
u<>[] -> SubSeq u (qseq q) -> last u 0 = q-1 -> qrvalence q u = 1.
Proof.
intros U U' L.
assert (SU : Suffix [q-1] u).
{ exists (removelast u). symmetry. rewrite <- L.
now apply app_removelast_last. }
generalize (suffix_qrvalence q _ _ SU) (qrvalence_nz q u U').
rewrite qrvalence_qm1. lia.
Qed.
Lemma letters_LeftExt q a b : b<q ->
LeftExt a [b] (qseq q) <-> a = prev_letter q b.
Proof.
intros B. split.
- intros (p, E). unfold subseq in E. simpl in E. injection E as Ea Eb.
subst. replace p with (S p - 1) at 1 by lia. apply qseq_prev_letter; lia.
- intros ->. exists b. unfold subseq. simpl. f_equal; symmetry.
+ unfold prev_letter.
case Nat.eqb_spec.
* intros ->. apply qseq_q_0.
* intros B'. replace b with (S (pred b)) at 1 by lia.
apply all_letters_occur. lia.
+ f_equal. apply all_letters_occur. lia.
Qed.
Lemma letters_RightExt q a b :
RightExt [a] b (qseq q) -> b = next_letter q a \/ b = q.
Proof.
intros (p, E). unfold subseq in E. simpl in E. injection E as Ea Eb.
case (Nat.eq_dec b q) as [Eb'|Eb']. now right. left. subst.
now apply qseq_next_letter.
Qed.
Lemma letters_AllLeftExts q a l : a<q ->
AllLeftExts l [a] (qseq q) <-> l = [prev_letter q a].
Proof.
split.
- intros (ND,A).
assert (IC :incl l [prev_letter q a]).
{ intros x Hx. rewrite A in Hx. apply letters_LeftExt in Hx; try lia.
simpl; intuition. }
assert (length l <= 1).
{ change 1 with (length [prev_letter q a]).
apply NoDup_incl_length; auto. }
destruct l as [|x [|y l]]; simpl in *; try lia.
+ destruct (qseq_leftext q [a]) as (b & B).
{ apply all_letters_subseq; lia. }
now rewrite <- A in B.
+ f_equal. specialize (IC x). simpl in *; intuition.
- intros ->. split.
+ now repeat constructor.
+ intros b. rewrite letters_LeftExt; trivial. simpl; intuition.
Qed.
Lemma letters_AllRightExts_incl q a l :
AllRightExts [a] l (qseq q) -> incl l [next_letter q a; q].
Proof.
intros (_,A) x Hx. rewrite A in Hx. apply letters_RightExt in Hx.
simpl; intuition.
Qed.
Lemma qlvalence_letter q a : a<q -> qlvalence q [a] = 1.
Proof.
intros A. unfold qlvalence.
replace (qleftexts q [a]) with [prev_letter q a]; trivial.
symmetry. apply letters_AllLeftExts; auto using qleftexts_ok.
Qed.
Lemma qlvalence_letter_q q : qlvalence q [q] = S q.
Proof.
change [q] with (qprefix q 1). apply qprefix_qlvalence.
Qed.
Lemma qrvalence_letter_le q a : qrvalence q [a] <= 2.
Proof.
unfold qrvalence. change 2 with (length [next_letter q a; q]).
apply NoDup_incl_length. apply qrightexts_ok.
apply letters_AllRightExts_incl. apply qrightexts_ok.
Qed.
(** We'll prove later that actually all letters have qrvalence of 2
except (q-1) whose qrvalence is 1 (see qrvalence_qm1). *)
Lemma qrvalence_le_2 q u : u<>[] -> qrvalence q u <= 2.
Proof.
intros Hu. transitivity (qrvalence q [last u 0]).
- apply suffix_qrvalence.
exists (removelast u). symmetry. now apply app_removelast_last.
- apply qrvalence_letter_le.
Qed.
(** Lemmas from the article by Frougny et al. *)
Lemma lemma_3_7_i q u a :
LeftExt a u (qseq q) ->
LeftExt (next_letter q a) (qsubstw q u) (qseq q).
Proof.
intros Ha. assert (Ha' := LeftExt_letter _ _ _ Ha).
unfold LeftExt in *. rewrite SubSeq_qseq_alt in *.
destruct Ha as (n, (v & w & E)). exists (S n).
rewrite qword_S, <- E, !qsubstw_app. cbn. clear E.
unfold qsubst, next_letter.
case Nat.eqb_spec; intros.
- subst. exists (qsubstw q v ++ [q]), (qsubstw q w).
now rewrite <- !app_assoc.
- now exists (qsubstw q v), (qsubstw q w).
Qed.
Lemma lemma_3_7_i_ls q u :
LeftSpecial u (qseq q) ->
LeftSpecial (qsubstw q u) (qseq q).
Proof.
intros (a & b & AB & A & B).
assert (A' := LeftExt_letter _ _ _ A).
assert (B' := LeftExt_letter _ _ _ B).
apply lemma_3_7_i in A, B.
exists (next_letter q a), (next_letter q b); repeat split; trivial.
contradict AB.
rewrite <- (prev_next_letter q a), <- (prev_next_letter q b) by trivial.
now rewrite AB.
Qed.
Lemma PrefixSeq_substlength_prefix q u v :
PrefixSeq u (qseq q) -> PrefixSeq v (qseq q) ->
length (qsubstw q u) <= length (qsubstw q v) ->
Prefix u v.
Proof.
intros U V L.
destruct (Nat.le_gt_cases (length u) (length v)).
- eapply PrefixSeq_incl; eauto.
- assert (P : Prefix v u) by (eapply PrefixSeq_incl; eauto; lia).
destruct P as (w & <-).
rewrite qsubstw_app, app_length in L.
assert (L' : length (qsubstw q w) = 0) by lia.
apply length_zero_iff_nil in L'.
apply (qsubstw_inv q w []) in L'. subst w. rewrite app_nil_r.
apply Prefix_id.
Qed.
Lemma lemma_3_7_ii_aux q u a :
hd 0 u <> 0 -> last u 0 <> q ->
LeftExt a u (qseq q) ->
exists v, qsubstw q v = u /\
LeftExt (prev_letter q a) v (qseq q).
Proof.
intros HD LA Ha. assert (Ha' := LeftExt_letter _ _ _ Ha).
unfold LeftExt in *. rewrite SubSeq_alt0 in Ha.
destruct Ha as (w & (u1 & E) & P).
destruct (qsubst_prefix_inv _ _ P) as (w' & r & E' & P' & [->|Hr]).
- rewrite app_nil_r in E'.
assert (Pu1 : PrefixSeq (u1++[a]) (qseq q)).
{ apply Prefix_PrefixSeq with w; trivial.
exists u. now rewrite <- app_assoc. }
destruct (qsubst_prefix_inv _ _ Pu1) as (u1' & r' & E1 & Pu1' & [->|Hr']).
+ rewrite app_nil_r in E1.
assert (PR : Prefix u1' w').
{ eapply PrefixSeq_substlength_prefix; eauto.
rewrite <- E1, <- E', <- E, !app_length. simpl. lia. }
destruct PR as (u' & PR).
exists u'. split.
* rewrite <- PR in E'. rewrite qsubstw_app, <- E, <- E1 in E'.
change (a::u) with ([a]++u) in E'. rewrite app_assoc in E'.
now apply app_inv_head in E'.
* rewrite <- (rev_involutive u1') in *.
destruct (rev u1') as [|a' u2']; simpl in E1.
{ now destruct u1. }
{ rewrite SubSeq_alt0. exists w'. split; trivial.
exists (rev u2'). simpl in PR. rewrite <- app_assoc in PR.
replace (prev_letter q a) with a'; trivial.
revert E1. rewrite qsubstw_app. simpl. rewrite app_nil_r.
unfold qsubst.
case Nat.eqb_spec.
- intros ->. change [q;0] with ([q]++[0]).
rewrite app_assoc. intros E1. apply app_inv' in E1; trivial.
now destruct E1 as (_,[= ->]).
- intros NE E1. apply app_inv' in E1; trivial.
now destruct E1 as (_,[= ->]). }
+ subst r'. apply app_inv' in E1; trivial. destruct E1 as (E1,[= ->]).
assert (PR : Prefix u1' w').
{ eapply PrefixSeq_substlength_prefix; eauto.
rewrite <- E1, <- E', <- E, !app_length. simpl. lia. }
destruct PR as ([|a' u'] & PR).
{ rewrite app_nil_r in PR. exfalso.
apply (f_equal (@length nat)) in E. rewrite app_length in E.
simpl in E. subst. lia. }
rewrite <- PR in E'. rewrite E1, E' in E.
rewrite qsubstw_app in E. apply app_inv_head in E. simpl in E.
unfold qsubst in E at 1. destruct (Nat.eqb_spec a' q).
* injection E as E. now rewrite E in HD.
* injection E as E2 E3. exists u'. split. symmetry. apply E3.
unfold prev_letter. rewrite E2 at 1. simpl. rewrite E2 at 1. simpl.
rewrite SubSeq_alt0. exists w'. split; trivial.
now exists u1'.
- subst r. rewrite E' in E.
assert (u=[]).
{ destruct (list_eq_dec Nat.eq_dec u []) as [U|U]; trivial.
change (a::u) with ([a]++u) in E.
rewrite (@app_removelast_last _ u 0 U) in E.
rewrite !app_assoc in E.
apply app_inv' in E; trivial. now destruct E as (_,[= E]). }
now subst u.
Qed.
Lemma lemma_3_7_ii_cor q u : hd 0 u <> 0 -> last u 0 <> q ->
SubSeq u (qseq q) ->
exists v : word, qsubstw q v = u /\ SubSeq v (qseq q).
Proof.
intros U U' SU. destruct (qseq_leftext _ _ SU) as (a & LE).
destruct (lemma_3_7_ii_aux q u a U U' LE) as (v & V & V').
exists v. split; trivial. eapply Sub_SubSeq; eauto using Sub_cons_r.
Qed.
Lemma lemma_3_7_ii_all' q u l :
SubSeq u (qseq q) -> hd 0 u <> 0 -> last u 0 <> q ->
AllLeftExts l u (qseq q) ->
exists v, qsubstw q v = u /\
AllLeftExts (map (prev_letter q) l) v (qseq q).
Proof.
intros SU U U' (ND,A).
destruct l as [|a l].
{ destruct (qseq_leftext q u SU) as (a & Ha). now rewrite <- A in Ha. }
destruct (lemma_3_7_ii_aux q u a) as (v & Hv & Ha); trivial.
{ rewrite <- A. simpl; intuition. }
exists v; split; auto. split.
+ apply NoDup_map_inv with (f:=next_letter q).
rewrite map_map, map_ext_in with (g:=id), map_id; auto.
intros c Hc. apply next_prev_letter. rewrite A in Hc.
now apply LeftExt_letter in Hc.
+ intros c. rewrite in_map_iff. split.
* intros (x & <- & IN). rewrite A in IN.
destruct (lemma_3_7_ii_aux q u x) as (v' & Hv' & Hx); trivial.
replace v' with v in *; auto.
{ apply (qsubstw_inv q). now rewrite Hv, Hv'. }
* intros Hc. exists (next_letter q c). split.
{ apply prev_next_letter. eapply LeftExt_letter; eauto. }
rewrite A, <- Hv. now apply lemma_3_7_i.
Qed.
Lemma lemma_3_7_ii_val' q u :
SubSeq u (qseq q) -> hd 0 u <> 0 -> last u 0 <> q ->
exists v, qsubstw q v = u /\ qlvalence q v = qlvalence q u.
Proof.
intros SU U U'.
destruct (lemma_3_7_ii_all' q u (qleftexts q u) SU U U') as (v & Hv & H);
auto using qleftexts_ok.
exists v; split; auto.
unfold qlvalence at 2.
rewrite <- (map_length (prev_letter q) (qleftexts q u)).
now apply qlvalence_ok.
Qed.
Lemma lemma_3_7_ii_all q u l :
last u 0 <> q ->
AllLeftExts l u (qseq q) -> 2 <= length l ->
exists v, qsubstw q v = u /\
AllLeftExts (map (prev_letter q) l) v (qseq q).
Proof.
intros U (ND,A) L.
destruct (list_eq_dec Nat.eq_dec u []).
- subst. simpl in *. exists []. repeat split; trivial.
+ apply NoDup_map_inv with (f:=next_letter q).
rewrite map_map, map_ext_in with (g:=id), map_id; auto.
intros a Ha. apply next_prev_letter. rewrite A in Ha.
now apply LeftExt_letter in Ha.
+ rewrite in_map_iff.
intros (x & E & IN). rewrite A in IN. apply LeftExt_letter in IN.
red. apply all_letters_subseq. subst a. now apply prev_letter_le.
+ rewrite in_map_iff. intros Ha. apply LeftExt_letter in Ha.
exists (next_letter q a). split.
* now apply prev_next_letter.
* rewrite A. now apply all_letters_subseq, next_letter_le.
- assert (hd 0 u <> 0).
{ destruct u as [|x u]; try easy.
simpl. apply (ls_head_nz q x u).
destruct l as [|a [|b l]]; simpl in L; try lia.
exists a, b; repeat split.
- inversion ND; simpl in *; intuition.
- apply A; simpl; intuition.
- apply A; simpl; intuition. }
apply lemma_3_7_ii_all'; auto. 2:now red.
destruct l as [|a l]; simpl in L; try lia.
assert (SU : SubSeq (a::u) (qseq q)). { apply A. simpl; intuition. }
eapply Sub_SubSeq; eauto using Sub_cons_r.
Qed.
Lemma lemma_3_7_ii_val q u :
last u 0 <> q -> 2 <= qlvalence q u ->
exists v, qsubstw q v = u /\ qlvalence q v = qlvalence q u.
Proof.
intros U L.
destruct (lemma_3_7_ii_all q u (qleftexts q u) U) as (v & Hv & H);
auto using qleftexts_ok.
exists v; split; auto.
unfold qlvalence.
rewrite <- (map_length (prev_letter q) (qleftexts q u)).
now apply qlvalence_ok.
Qed.
Lemma lemma_3_7_ii_ls q u :
last u 0 <> q -> LeftSpecial u (qseq q) ->
exists v, qsubstw q v = u /\ LeftSpecial v (qseq q).
Proof.
rewrite ls_val. intros U L.
destruct (lemma_3_7_ii_val q u U L) as (v & V & E).
exists v; split; auto. apply ls_val. lia.
Qed.
Lemma lemma_3_7_i_all_incl q u l l' :
AllLeftExts l u (qseq q) ->
AllLeftExts l' (qsubstw q u) (qseq q) ->
incl (map (next_letter q) l) l'.
Proof.
intros (ND,A) (ND',A') a. rewrite in_map_iff. intros (x & <- & Hx).
rewrite A in Hx. rewrite A'. now apply lemma_3_7_i.
Qed.
Lemma lemma_3_7_i_val_le q u :
qlvalence q u <= qlvalence q (qsubstw q u).
Proof.
unfold qlvalence.
rewrite <- (map_length (next_letter q) (qleftexts q u)).
apply NoDup_incl_length.
- apply NoDup_map_inv with (f:=prev_letter q).
rewrite map_map, map_ext_in with (g:=id), map_id; auto.
apply qleftexts_ok.
intros a Ha. apply prev_next_letter.
assert (H := qleftexts_ok q u). destruct H as (_,H).
rewrite H in Ha. now apply LeftExt_letter in Ha.
- eapply lemma_3_7_i_all_incl; eauto using qleftexts_ok.
Qed.
(** Note: [q-1] has qlvalence of 1 since it could only come after
(prev_letter q (q-1)). But (qsubstw q [q-1])=[q] has
qlvalence of (S q).
Hence the qlvalence is preserved by qsubst only when it is at least 2
(i.e. for left-special words). *)
(* /!\ Problem with the last line of the proof of Lemma 3.7 :
\tilde{p} = p cannot be obtained in general, since (ii) needs
last letter to be different from q.
No big issue, since eventually the only LeftSpecial words
(the qprefix) have qlvalence (S q), hence the same for their image
by qsubst. And this precise part of Lemma 3.7 (i) doesn't seem
to be used in the rest of the article / corrigendum. *)
Definition MaxLeftSpecial u (f:sequence) :=
LeftSpecial u f /\ forall a, ~LeftSpecial (u++[a]) f.
Lemma observation_4_2_contra u f : MaxLeftSpecial u f -> RightSpecial u f.
Proof.
intros ((a & b & AB & A & B),H).
destruct (SubSeq_RightExt (a::u) f A) as (c & C).
destruct (SubSeq_RightExt (b::u) f B) as (d & D).
destruct (Nat.eq_dec c d).
- subst d. destruct (H c). exists a, b. repeat split; auto.
- exists c, d; repeat split; auto.
+ eapply RightExt_Suffix; eauto. now exists [a].
+ eapply RightExt_Suffix; eauto. now exists [b].
Qed.
Lemma observation_4_2 u f :
LeftSpecial u f -> ~RightSpecial u f -> ~MaxLeftSpecial u f.
Proof.
intros H H'. contradict H'. now apply observation_4_2_contra.
Qed.
Lemma lemma_4_4 q n a : n<>0 ->
last (qword q n) 0 = a -> Suffix [prev_letter q a; a] (qword q n).
Proof.
induction n as [n IH] using lt_wf_ind.
intros Hn Ha. destruct (Nat.le_gt_cases n (S q)).
- clear IH. rewrite qword_low in * by lia.
destruct n as [|[|n]]; try easy.
+ simpl in *. subst a. now exists [].
+ rewrite seq_S in Ha. simpl "+" in Ha.
change (q::_++[S n]) with ((q::seq 0 (S n))++[S n]) in Ha.
rewrite last_last in Ha. subst a.
rewrite !seq_S. exists (q::seq 0 n). simpl. f_equal.
now rewrite <- app_assoc.
- destruct n; try easy. rewrite qword_eqn in * by lia.
rewrite last_app in Ha.
2:{ apply qword_nz. }
destruct (IH (n-q)) as (u & <-); trivial; try lia.
exists (qword q n ++ u). now rewrite app_assoc.
Qed.
Lemma Sub_app {A} (u1 u2 v1 v2 : list A) :
Suffix u1 v1 -> Prefix u2 v2 -> Sub (u1++u2) (v1++v2).
Proof.
intros (u0, <-) (u3, <-). exists u0, u3. now rewrite !app_assoc.
Qed.
Lemma Suffix_last {A} (l:list A) (a:A) : l<>[] -> Suffix [last l a] l.
Proof.
exists (removelast l). symmetry. now apply app_removelast_last.
Qed.
Lemma lemma_4_5 q r a b : a<>q -> b<>q ->
SubSeq ([a] ++ repeat q r ++ [b]) (qseq q) <->
(r=0 /\ a = b-1 /\ 0 < b < q) \/
(r=1 /\ a < q /\ b = 0) \/
(r=2 /\ a = q-1 /\ b = 0).
Proof.
intros A B. split.
- rewrite SubSeq_qseq_alt. intros (n,SU). revert SU.
induction n as [n IH] using lt_wf_ind.
destruct (Nat.le_gt_cases n q) as [LE|GT].
+ clear IH. rewrite qword_low by lia. intros (u & v & E). left.
rewrite <- !app_assoc in E.
destruct u; simpl in E; injection E as -> E; try easy.
assert (length u < n).
{ rewrite <- (seq_length n 0). rewrite <- E. rewrite app_length.
simpl. lia. }
replace n with (length u + (n-length u)) in E by lia.
rewrite seq_app in E.
apply app_inv in E. destruct E as (_,E).
2:{ now rewrite seq_length. }
destruct (n-length u) as [|n'] eqn:N'; try lia.
simpl in E. injection E as E1 E2.
destruct r; destruct n'; simpl in E2; try easy;
injection E2 as E2 _; lia.
+ destruct n; try easy.
rewrite qword_eqn by lia. intros SU. apply Sub_app_inv in SU.
destruct SU as [SU|[SU|(u1 & u2 & U1 & U2 & E & SU & PR)]].
* apply (IH n); auto.
* apply (IH (n-q)); auto. lia.
* clear IH. right.
destruct u1 as [|x1 u1]; try easy. clear U1. simpl in E.
injection E as <- E.
rewrite <- (rev_involutive u2) in *.
destruct (rev u2) as [|x2 u2']; try easy. clear U2. simpl in *.
clear u2.
rewrite app_assoc in E.
apply app_inv' in E; trivial. destruct E as (E & [= <-]).
destruct (Nat.eq_dec n q) as [->|N].
{ rewrite Nat.sub_diag, qword_0 in PR.
destruct PR as (u2, PR).
assert (L := f_equal (@length nat) PR).
rewrite !app_length, rev_length in L. simpl in L.
assert (length u2' = 0) by lia.
rewrite length_zero_iff_nil in *. subst u2'.
simpl in PR. now injection PR as -> _. }
{ assert (PR' : 1 <= n-q) by lia.
apply (qword_le_prefix q) in PR'. rewrite qword_1 in PR'.
destruct (rev u2') as [|x [|y u2]]; simpl in PR.
- assert (PR2 : Prefix [b] [q;0]).
{ eapply Prefix_Prefix; simpl; eauto. }
now destruct PR2 as (v & [= -> _]).
- clear u2'. destruct PR as (v & PR).
destruct PR' as (v' & PR').
rewrite <- PR' in PR. apply app_inv in PR; auto.
destruct PR as ([= -> ->],_). clear PR'.
destruct r as [|r]; [now destruct u1| ].
rewrite <- Nat.add_1_r, repeat_app in E. simpl in E.
apply app_inv' in E; auto. destruct E as (<-,_). clear v v'.
destruct r as [|[|r]].
+ left; repeat split; auto.
simpl in SU. destruct SU as (w & SU).
generalize (qword_letters q n). rewrite <- SU, Forall_app.
intros (_,F). inversion_clear F. lia.
+ right; repeat split; auto.
simpl in SU.
destruct SU as (u & SU).
assert (N' : n <> 0) by lia.
assert (L : last (qword q n) 0 = q).
{ now rewrite <- SU, last_app. }
assert (SU' := lemma_4_4 q n q N' L).
destruct SU' as (u' & SU'). rewrite <- SU' in SU.
apply app_inv' in SU; auto. destruct SU as (_,[= ->]).
unfold prev_letter. case Nat.eqb_spec; lia.
+ exfalso.
replace (S (S r)) with (r+2) in SU by lia.
rewrite repeat_app in SU. simpl in SU.
destruct SU as (u & SU).
change (a::_ ++ _) with ((a::repeat q r)++[q;q]) in SU.
rewrite app_assoc in SU.
assert (N' : n <> 0) by lia.
assert (L : last (qword q n) 0 = q).
{ now rewrite <- SU, last_app. }
assert (SU' := lemma_4_4 q n q N' L).
destruct SU' as (u' & SU'). rewrite <- SU' in SU.
apply app_inv' in SU; auto. destruct SU as (_,[= E]).
revert E. unfold prev_letter. case Nat.eqb_spec; lia.
- exfalso.
assert (IN : In a (qword q n)).
{ destruct SU as (u & <-). rewrite in_app_iff; right.
simpl; intuition. }
assert (LT : a < q).
{ generalize (qword_letters q n). rewrite Forall_forall.
intros F. specialize (F a IN). lia. }
clear IN.
assert (PR2 : Prefix [q;0] (x::y::u2++[b])).
{ eapply Prefix_Prefix; simpl; eauto; try lia. }
destruct PR2 as (u & [= <- <- PR2]).
assert (IN : In 0 (repeat q r)).
{ rewrite E. rewrite in_app_iff. right. simpl; intuition. }
apply repeat_spec in IN. lia. }
- intros [(-> & -> & B')|[(-> & A' & ->)|(-> & -> & ->)]].
+ simpl. exists b. unfold subseq. simpl.
assert (E : b = qseq q (S b)).
{ symmetry. apply all_letters_occur. lia. }
f_equal; [|now f_equal].
symmetry. replace b with ((S b)-1) at 1 by lia.
rewrite qseq_prev_letter by lia. rewrite <- E.
unfold prev_letter. case Nat.eqb_spec; lia.
+ simpl. apply SubSeq_qseq_alt. exists (S (q+a+2)).
rewrite qword_eqn by lia.
assert (E : last (qword q (q+a+2)) 0 = a).
{ rewrite WordSuffix.qword_last.
replace (q+a+2+q) with (a+2*(S q)) by lia.
rewrite Nat.mod_add, Nat.mod_small; lia. }
change [a;q;0] with ([a]++[q;0]).
apply Sub_app.
* rewrite <- E at 1. apply Suffix_last. apply qword_nz.
* replace [q;0] with (qword q 1).
2:{ rewrite qword_low; simpl; trivial; lia. }
apply qword_le_prefix; lia.
+ simpl. apply SubSeq_qseq_alt. exists (S (q+1)).
rewrite qword_eqn by lia.
assert (E : last (qword q (q+1)) 0 = q).
{ rewrite WordSuffix.qword_last.
replace (q+1+q) with (q+1*(S q)) by lia.
rewrite Nat.mod_add, Nat.mod_small; lia. }
change [q-1;q;q;0] with ([q-1;q]++[q;0]).
apply Sub_app.
* replace (q-1) with (prev_letter q q).
apply lemma_4_4; try lia.
unfold prev_letter. case Nat.eqb_spec; lia.
* replace [q;0] with (qword q 1).
2:{ rewrite qword_low; simpl; trivial; lia. }
apply qword_le_prefix; lia.
Qed.
Lemma infinitly_many_0_letters q :
forall n, { m | n <= m /\ qseq q m = 0 }.
Proof.
intros n.
destruct (Nat.eq_dec q 0) as [->|Q].
- exists n. split; trivial. generalize (qseq_letters 0 n). lia.
- set (p := invA_up q n).
exists (S (Nat.max (q+2) (A q p))). split.
+ generalize (invA_up_spec q n). unfold p. lia.
+ apply Nat.max_case_strong; intros LE.
* rewrite qseq_bounded_rank. unfold bounded_rank, rank.
rewrite decomp_S.
replace (decomp q (q+2)) with [S q].
2:{ symmetry. apply decomp_carac.
- constructor.
- replace (q+2) with (S (S q)) by lia.
rewrite <- (@A_base q (S q)) by lia. simpl; lia. }
unfold next_decomp. case Nat.leb_spec; simpl; lia.
* rewrite qseq_bounded_rank. unfold bounded_rank, rank.
replace (decomp q (S (A q p))) with [0;p]; trivial.
symmetry. apply decomp_carac; simpl; try lia.
constructor. 2:constructor. simpl. apply (A_le_inv q).
rewrite A_base; lia.
Qed.
Lemma lemma_4_5_bis q r a :
q<>0 -> a<>q -> SubSeq ([a] ++ repeat q r) (qseq q) -> r <= 2.
Proof.
intros Q A (p,E).
rewrite app_length, repeat_length in E. simpl in E.
destruct (infinitly_many_0_letters q (p+S r)) as (n,(N,N')).
remember (n-(p+S r)) as m eqn:M.
revert r E N N' M.
induction m; intros.
- replace n with (p+S r) in N' by lia.
assert (SU : SubSeq ([a] ++ repeat q r ++ [0]) (qseq q)).
{ exists p. rewrite !app_length, repeat_length, Nat.add_1_r. simpl.
unfold subseq in *. now rewrite seq_S, map_app, <- E, <- N'. }
apply lemma_4_5 in SU; trivial; lia.
- destruct (Nat.eq_dec (qseq q (p+S r)) q) as [E'|E'].
+ assert (S r <= 2); try lia.
apply IHm; try lia. clear IHm.
rewrite <- (Nat.add_1_r r), repeat_app at 1. simpl.
unfold subseq in *. rewrite seq_S, map_app, <- E. simpl.
now repeat f_equal.
+ set (b := qseq q (p+S r)) in *.
assert (SU : SubSeq ([a] ++ repeat q r ++ [b]) (qseq q)).
{ exists p. rewrite !app_length, repeat_length, Nat.add_1_r. simpl.
unfold subseq in *. now rewrite seq_S, map_app, <- E. }
apply lemma_4_5 in SU; trivial; lia.
Qed.
Lemma lemma_4_5_ter q r : q<>0 -> SubSeq (repeat q r) (qseq q) -> r <= 2.
Proof.
intros Q (p,E). rewrite repeat_length in E. revert r E.
induction p; intros.
- unfold subseq in E. destruct r as [|[|r]]; try lia.
simpl in E. rewrite qseq_q_1 in E. now injection E as [= E _].
- destruct (Nat.eq_dec (qseq q p) q) as [E'|E'].
+ assert (S r <= 2); try lia.
{ apply IHp. unfold subseq in *. simpl. now rewrite E', E. }
+ eapply lemma_4_5_bis; eauto. exists p.
rewrite app_length, repeat_length. simpl. now rewrite E.
Qed.
Lemma lemma_4_5_qq q a b :