Words.v

Require Import MoreFun MoreList DeltaList GenFib GenG.
Import ListNotations.

(** * Morphic words

    Some theory of infinite words generated by substitutions.
    Hofstadter functions [f q] can be described by such infinite words.
*)

(** letters : here some natural numbers.
    Most of the time, we'll only use 0..q for some parameter q. *)

Notation letter := nat (only parsing).

(** Finite word : list of letters *)

Definition word := list letter.

(** Sequence a.k.a Infinite word : function from nat to letter *)

Definition sequence := nat -> letter.

Definition PrefixSeq (u:word) (f:sequence) := u = take (length u) f.

(** Substitution : function form letter to words *)

Definition subst := letter -> word.

Definition apply : subst -> word -> word := @flat_map _ _.

Fixpoint napply (s:subst) n w :=
  match n with
  | 0 => w
  | S n => napply s n (apply s w)
  end.

Lemma napply_is_iter s n w : napply s n w = (apply s ^^n) w.
Proof.
 revert w.
 induction n; auto. intros. now rewrite iter_S, <- IHn.
Qed.

Lemma napply_1 s u : napply s 1 u = apply s u.
Proof.
 reflexivity.
Qed.

Lemma apply_app s u v : apply s (u++v) = apply s u ++ apply s v.
Proof.
 apply flat_map_app.
Qed.

Lemma apply_alt s w : apply s w = concat (map s w).
Proof.
 apply flat_map_concat_map.
Qed.

Lemma napply_nil s n : napply s n [] = [].
Proof.
 induction n; simpl; auto.
Qed.

Lemma napply_app s n u v : napply s n (u++v) = napply s n u ++ napply s n v.
Proof.
 revert u v. induction n; intros; simpl; auto.
 now rewrite apply_app, IHn.
Qed.

Lemma napply_cons s n a u : napply s n (a::u) = napply s n [a] ++ napply s n u.
Proof.
 apply (napply_app s n [a] u).
Qed.

Lemma napply_alt s n u : napply s (S n) u = apply s (napply s n u).
Proof.
 revert u.
 induction n; intros; simpl; auto.
 now rewrite <- IHn.
Qed.

Lemma napply_add s n m u : napply s (n+m) u = napply s n (napply s m u).
Proof.
 induction n.
 - simpl; auto.
 - now rewrite Nat.add_succ_l, !napply_alt, IHn.
Qed.

Lemma napply_flat_map s n w :
  napply s n w = flat_map (fun a => napply s n [a]) w.
Proof.
 induction w; simpl; auto using napply_nil.
 rewrite napply_cons. now f_equal.
Qed.

Lemma Prefix_apply s u v :
  Prefix u v -> Prefix (apply s u) (apply s v).
Proof.
 intros (w, <-). rewrite apply_app. now eexists.
Qed.

Lemma Prefix_napply s n u v :
  Prefix u v -> Prefix (napply s n u) (napply s n v).
Proof.
 intros (w, <-). rewrite napply_app. now eexists.
Qed.

Definition NoErase (s:subst) := forall a, s a <> [].

Definition Prolong (s:subst) a := exists u, u<>[] /\ s a = a::u.

Lemma noerase_nonnil_apply s u : NoErase s -> u<>[] -> apply s u <> [].
Proof.
 intros NE. destruct u as [|a u]. easy. intros _. simpl.
 specialize (NE a). destruct (s a) as [|b v]; easy.
Qed.

Lemma noerase_nonnil_napply s u n : NoErase s -> u<>[] -> napply s n u <> [].
Proof.
 intros NE. revert u. induction n; simpl; intros; auto.
 apply IHn. apply noerase_nonnil_apply; auto.
Qed.

Lemma noerase_prolong_napply_len s a :
  NoErase s -> Prolong s a -> forall n, n < length (napply s n [a]).
Proof.
 intros NE (u & Hu & PR).
 induction n. simpl; auto.
 simpl. rewrite app_nil_r, PR, napply_cons, app_length.
 assert (length (napply s n u) <> 0).
 { rewrite length_zero_iff_nil. now apply noerase_nonnil_napply. }
 lia.
Qed.

Lemma napply_prefix_S s a n :
 Prolong s a -> Prefix (napply s n [a]) (napply s (S n) [a]).
Proof.
 intros (u & Hu & PR).
 simpl. rewrite app_nil_r, PR. rewrite (napply_cons _ _ _ u).
 now exists (napply s n u).
Qed.

Lemma napply_prefix_mono s a n m : Prolong s a -> n <= m ->
 Prefix (napply s n [a]) (napply s m [a]).
Proof.
 intros PR.
 induction 1.
 - exists []. apply app_nil_r.
 - destruct IHle as (w & E).
   destruct (napply_prefix_S s a m) as (w' & E'); auto.
   exists (w++w'). now rewrite app_assoc, E, E'.
Qed.

Lemma apply_grow s w : NoErase s -> length w <= length (apply s w).
Proof.
 intros NE.
 induction w; simpl; auto.
 rewrite app_length. specialize (NE a). destruct (s a); simpl; lia || easy.
Qed.

Lemma napply_mono s n m w :
 NoErase s -> n <= m -> length (napply s n w) <= length (napply s m w).
Proof.
 induction 2; auto.
 rewrite IHle. clear IHle H0. rewrite napply_alt. now apply apply_grow.
Qed.

(** Any nonerasing prolongeable substitution leads to a unique infinite
    sequence *)

Definition SubstSeq (s:subst) (f:sequence) a :=
  forall n, PrefixSeq (napply s n [a]) f.

Definition subst2seq s a :=
 fun n => nth n (napply s n [a]) a.

Lemma subst2seq_indep s a b n : NoErase s -> Prolong s a ->
  forall m, n <= m -> subst2seq s a n = nth n (napply s m [a]) b.
Proof.
 intros. rewrite nth_indep with (d':=a).
 2:{ apply Nat.le_lt_trans with m; trivial.
     apply noerase_prolong_napply_len; trivial. }
 apply Prefix_nth. apply napply_prefix_mono; auto.
 apply noerase_prolong_napply_len; auto.
Qed.

Lemma substseq_exists s a :
  NoErase s -> Prolong s a -> SubstSeq s (subst2seq s a) a.
Proof.
 intros NE PR n.
 red. symmetry. apply take_carac; auto.
 intros m b Hm.
 unfold subst2seq.
 rewrite (nth_indep _ b a); auto.
 destruct (Nat.le_gt_cases n m).
 - apply Prefix_nth; auto.
   apply napply_prefix_mono; auto.
 - symmetry.
   apply Prefix_nth; auto.
   apply napply_prefix_mono; auto with arith.
   apply noerase_prolong_napply_len; auto.
Qed.

Lemma substseq_unique s a f f' :
  NoErase s -> Prolong s a -> SubstSeq s f a -> SubstSeq s f' a ->
  (forall n, f n = f' n).
Proof.
 intros NE PR Hf Hf' n.
 specialize (Hf (S n)).
 specialize (Hf' (S n)). unfold PrefixSeq in *.
 set (u := napply s (S n) [a]) in *.
 rewrite <- (take_nth f (length u) n a).
 2:{ transitivity (S n); auto. apply noerase_prolong_napply_len; auto. }
 rewrite <- (take_nth f' (length u) n a); auto.
 2:{ transitivity (S n); auto. apply noerase_prolong_napply_len; auto. }
 now rewrite <- Hf, <- Hf'.
Qed.

(** Specific susbstitution for Hofstadter functions.
    Works on letters 0..q *)

Definition qsubst q (n:letter) := if n =? q then [q; 0] else [S n].

(** After the substitution of letters, now the substitution of words *)

Definition qsubstw q : word -> word := apply (qsubst q).

(** Iterated substitution of word *)

Definition qword q n := napply (qsubst q) n [q].

(** The corresponding infinite word (limit of the qword sequence) *)

Definition qseq q := subst2seq (qsubst q) q.

(* Compute take 20 (qseq 2). *)
(* [2; 0; 1; 2; 2; 0; 2; 0; 1; 2; 0; 1; 2; 2; 0; 1; 2; 2; 0; 2] *)

Lemma qsubst_noerase q : NoErase (qsubst q).
Proof.
 red. intros c. unfold qsubst. now case Nat.eqb_spec.
Qed.

Lemma qsubst_prolong q : Prolong (qsubst q) q.
Proof.
 red. exists [0]. split. easy.
 unfold qsubst. now rewrite Nat.eqb_refl.
Qed.

Lemma qseq_SubstSeq q : SubstSeq (qsubst q) (qseq q) q.
Proof.
 apply substseq_exists. apply qsubst_noerase. apply qsubst_prolong.
Qed.

Lemma qsubstw_app q u v : qsubstw q (u++v) = qsubstw q u ++ qsubstw q v.
Proof.
 apply apply_app.
Qed.

Lemma qword_S q n : qword q (S n) = qsubstw q (qword q n).
Proof.
 apply napply_alt.
Qed.

Lemma qseq_q_0 q : qseq q 0 = q.
Proof.
 reflexivity.
Qed.

Lemma qseq_q_1 q : qseq q 1 = 0.
Proof.
 unfold qseq, subst2seq, qsubst. simpl. now rewrite Nat.eqb_refl.
Qed.

Lemma qsubst_q q : qsubst q q = [q;0].
Proof.
 unfold qsubst. now rewrite Nat.eqb_refl.
Qed.

Lemma qsubst_qm1 q : q<>0 -> qsubst q (q-1) = [q].
Proof.
 intros Q. unfold qsubst. case Nat.eqb_spec; intros. lia. f_equal. lia.
Qed.

(** qword letters are always in 0..q *)

Lemma qsubst_letters q w :
 Forall (fun a => a <= q) w ->
 Forall (fun a => a <= q) (qsubstw q w).
Proof.
 induction w; simpl; auto.
 intros H; inversion_clear H. apply Forall_app. split; auto.
 unfold qsubst.
 case Nat.eqb_spec; intro; repeat (constructor; try lia).
Qed.

Lemma napply_qsubst_letters q n w :
 Forall (fun a => a <= q) w ->
 Forall (fun a => a <= q) (napply (qsubst q) n w).
Proof.
 induction n.
 - simpl. trivial.
 - rewrite napply_alt. intros. now apply qsubst_letters, IHn.
Qed.

Lemma qword_letters q n : Forall (fun a => a <= q) (qword q n).
Proof.
 apply napply_qsubst_letters. now constructor.
Qed.

Lemma qseq_letters q n : qseq q n <= q.
Proof.
 unfold qseq, subst2seq.
 set (l := napply _ _ _).
 assert (Forall (fun a => a <= q) l).
 { apply napply_qsubst_letters. now constructor. }
 clearbody l. revert n. induction H; simpl; now destruct n.
Qed.

(** Initial values *)

Lemma qword_0 q : qword q 0 = [q].
Proof.
 reflexivity.
Qed.

Lemma qword_1 q : qword q 1 = [q;0].
Proof.
 cbn. unfold qsubst. now rewrite Nat.eqb_refl.
Qed.

Lemma qsubst_low0 q n : n <= q -> napply (qsubst q) n [0] = [n].
Proof.
 induction n. auto.
 intros LE.
 rewrite napply_alt. rewrite IHn; try lia. simpl.
 unfold qsubst. case Nat.eqb_spec. lia. intros _. apply app_nil_r.
Qed.

Lemma qword_low q n : n <= S q -> qword q n = q :: List.seq 0 n.
Proof.
 induction n.
 - now rewrite qword_0.
 - intros LE.
   rewrite seq_S.
   cbn. unfold qsubst at 2. rewrite Nat.eqb_refl. simpl.
   rewrite napply_cons.
   rewrite qsubst_low0; auto; try lia.
   change (qword q n ++ [n] = q  :: List.seq 0 n ++ [n]).
   rewrite IHn; try lia. auto.
Qed.

(** Alt equation : *)

Lemma qword_eqn q n : q<=n -> qword q (S n) = qword q n ++ qword q (n-q).
Proof.
 induction n.
 - intros. replace q with 0 by lia. simpl; auto.
 - intros LE. apply Nat.lt_eq_cases in LE. destruct LE as [LT|EQ].
   + replace (S n -q) with (S (n-q)) by lia.
     remember (S n) as m eqn:E.
     cbn.
     rewrite app_nil_r.
     unfold qsubst at 2. rewrite Nat.eqb_refl.
     rewrite napply_cons. f_equal.
     replace m with (m-q+q) by lia.
     rewrite napply_add. rewrite qsubst_low0 by lia. simpl.
     replace (m-q) with (S (n-q)) by lia.
     simpl. now rewrite app_nil_r.
   + rewrite <- EQ. replace (q-q) with 0 by lia.
     rewrite qword_0. cbn.
     unfold qsubst at 2. rewrite Nat.eqb_refl, app_nil_r.
     rewrite napply_cons. f_equal. apply qsubst_low0. lia.
Qed.

Lemma qword_len q n : length (qword q n) = A q n.
Proof.
 induction n as [[|n] IH] using lt_wf_ind.
 - now rewrite qword_0.
 - case (Nat.le_gt_cases q n) as [LE|GT].
   + rewrite qword_eqn; auto. rewrite app_length, !IH; try lia.
     simpl; auto.
   + rewrite qword_low by auto. simpl.
     rewrite seq_length. rewrite !A_base; lia.
Qed.

Lemma qword_nz q n : qword q n <> [].
Proof.
 unfold word. rewrite <- length_zero_iff_nil, qword_len.
 generalize (A_nz q n); lia.
Qed.

Lemma qseq_alt q n m a : n < A q m -> qseq q n = nth n (qword q m) a.
Proof.
 intros LE.
 rewrite (qseq_SubstSeq q m).
 change (napply _ _ _) with (qword q m).
 rewrite qword_len, take_nth; auto.
Qed.

(** The qword are indeed prefixes of qseq *)

Lemma qseq_take_A q n : take (A q n) (qseq q) = qword q n.
Proof.
 apply take_carac.
 - apply qword_len.
 - intros. symmetry. now apply qseq_alt.
Qed.

(** Link between [qseq] and Zeckendorf decomposition :
    0 iff rank 0,
    1 iff rank 1,
    ...
    q iff rank >= q (or no rank, ie n=0)

    Hence 0 in [qseq] whenever the [f q] function is flat.
*)

Definition omin (oa:option nat) (b:nat) :=
  match oa with
  | None => b
  | Some a => Nat.min a b
  end.

Definition bounded_rank q n := omin (rank q n) q.

Lemma qseq_bounded_rank q n : qseq q n = bounded_rank q n.
Proof.
 induction n as [n IH] using lt_wf_ind.
 assert (E := decomp_sum q n).
 assert (D := decomp_delta q n).
 set (l := decomp q n) in *.
 destruct (rev l) as [|a rl] eqn:E'; apply rev_switch in E'.
 - rewrite E' in *. simpl in E. rewrite <- E. easy.
 - assert (A q a <= n < A q (S a)).
   { rewrite <- E, E', sumA_rev.
     split.
     + simpl; lia.
     + apply decomp_max. apply Delta_rev. now rewrite <- E'. }
   rewrite (qseq_alt q n (S a) 0) by lia.
   destruct (Nat.lt_ge_cases a q) as [LT|LE].
   + rewrite qword_low by lia.
     destruct n as [|n]; try easy.
     change (nth _ _ _) with (nth n (List.seq 0 (S a)) 0).
     rewrite !A_base in H; try lia.
     replace n with a by lia.
     rewrite seq_nth by lia. simpl.
     unfold bounded_rank, rank. rewrite decomp_low; simpl; lia.
   + rewrite qword_eqn by auto.
     rewrite app_nth2; rewrite qword_len; try lia.
     rewrite <- qseq_alt by (simpl in H; lia).
     rewrite IH by (generalize (@A_nz q a); lia).
     unfold bounded_rank, rank. fold l; rewrite E'; simpl rev.
     replace (decomp _ _) with (rev rl).
     2:{ symmetry; apply decomp_carac.
         - rewrite E' in D. simpl in D. now apply Delta_app_iff in D.
         - revert E. rewrite E'. simpl. rewrite sumA_app. simpl. lia. }
     destruct (rev rl); simpl; lia.
Qed.

(** Projecting qseq to 0 and 1 (i.e. all letters except 0 become 1,
    i.e. applying (min 1) to qseq) gives the sequence of (f q) increments. *)

Lemma min_1_qseq_is_delta_f q n :
  q<>0 -> Nat.min 1 (qseq q n) = f q (S n) - f q n.
Proof.
 intros Hq.
 rewrite qseq_bounded_rank.
 destruct (flat_rank_0 q n) as (_,H).
 destruct (step_rank_nz q n) as (_,H').
 unfold bounded_rank. destruct (rank q n) as [[|r]|]; unfold omin.
 - simpl. rewrite H; trivial. lia.
 - rewrite H'; try easy. lia.
 - rewrite H'; try easy. lia.
Qed.

(** More generally, projecting letters p..q to 1 and letters 0..(p-1) to 0
    gives the sequence of (fs q p) increments. *)

Lemma qseq_above_p_is_delta_fs q p n :
  q<>0 -> p<=q ->
  (if p <=? qseq q n then 1 else 0) = fs q p (S n) - fs q p n.
Proof.
 intros Hq Hp.
 rewrite qseq_bounded_rank.
 destruct (@fs_flat_iff' q p n) as (_,H).
 destruct (@fs_nonflat_iff' q p n) as (_,H').
 unfold bounded_rank. destruct (rank q n) as [r|]; unfold omin.
 - destruct (Nat.lt_decidable r p) as [LT|NLT]; case Nat.leb_spec; lia.
 - simpl in *. case Nat.leb_spec; lia.
Qed.

(** Another description of [qseq q n] :
    sum for p=1..q of [fs q p (n+1) - fs q p n] *)

Definition cumul_diff_fs q n :=
 cumul (fun p => fs q (S p) (S n) - fs q (S p) n) q.

Lemma qseq_is_cumul_diff_fs q n : qseq q n = cumul_diff_fs q n.
Proof.
 rewrite qseq_bounded_rank. unfold bounded_rank.
 destruct (rank q n) as [r|] eqn:E; simpl.
 - rewrite <- (cumul_ltb q r). unfold cumul_diff_fs.
   apply cumul_ext.
   intros m Hm.
   case Nat.ltb_spec; intros L.
   + destruct (@fs_nonflat_iff' q (S m) n) as (_,->); try lia.
     rewrite E; simpl; lia.
   + destruct (@fs_flat_iff' q (S m) n) as (_,->); try lia.
     rewrite E; simpl; lia.
 - rewrite rank_none in E. subst. unfold cumul_diff_fs.
   erewrite cumul_ext, (cumul_cst 1); try lia.
   intros x _. rewrite fs_q_0, fs_q_1. lia.
Qed.

(** Hence the sum of the n first letters of [qseq q] is
    the sum for p=1..q of [fs q p n]. *)

Lemma cumul_qseq_is_cumul_fs q n :
  cumul (qseq q) n = cumul (fun p => fs q (S p) n) q.
Proof.
 induction n; cbn -[fs].
 - erewrite cumul_ext; auto using cumul_0, fs_q_0.
 - rewrite IHn, qseq_is_cumul_diff_fs. unfold cumul_diff_fs.
   rewrite <- cumul_add. apply cumul_ext.
   intros m Hm. generalize (fs_mono_S q (S m) n). lia.
Qed.

(** Counting letter 0 in [qseq q] leads bacq to the [f q] fonction. *)

Lemma f_count_0 q n : q<>0 -> count (qseq q) 0 n + f q n = n.
Proof.
 induction n.
 - easy.
 - simpl. intros Hq.
   rewrite qseq_bounded_rank.
   unfold bounded_rank.
   destruct (f_step q n) as [E|E].
   + rewrite E. rewrite flat_rank_0 in E. rewrite E. simpl. lia.
   + rewrite E. rewrite step_rank_nz in E.
     destruct (rank q n) as [[|r]|]; simpl; try easy;
       destruct q; simpl; auto; try lia.
Qed.

(** Similarly, counting all letters above [p] leads to [fs q p],
    the p-iterate of [f q]. *)

Lemma fs_count_above q p n :
  p <= q -> fs q p n = count_above (qseq q) p n.
Proof.
 intros Hp.
 induction n.
 - simpl. apply fs_q_0.
 - simpl. rewrite qseq_bounded_rank.
   unfold bounded_rank.
   destruct (fs_step q p n) as [E|E].
   + rewrite E. rewrite fs_flat_iff' in E by lia.
     destruct (rank q n); simpl; try easy.
     red in E. case Nat.leb_spec; lia.
   + rewrite E. rewrite fs_nonflat_iff' in E.
     destruct (rank q n); simpl in *; case Nat.leb_spec; lia.
Qed.

(** Particular case : p=q *)

Lemma count_above_qseq_q q n :
  count_above (qseq q) q n = count (qseq q) q n.
Proof.
 induction n; simpl; auto.
 rewrite qseq_bounded_rank. unfold bounded_rank.
 destruct (rank q n); simpl in *; case Nat.leb_spec; case Nat.eqb_spec; lia.
Qed.

Lemma fs_count_q q n : fs q q n = count (qseq q) q n.
Proof.
 rewrite fs_count_above by lia.
 apply count_above_qseq_q.
Qed.

(** Prefixes of qseq *)

Notation qprefix q n := (take n (qseq q)).

Lemma qprefix_length q n : length (qprefix q n) = n.
Proof.
 apply take_length.
Qed.

Lemma qprefix_carac q u :
  PrefixSeq u (qseq q) <-> u = qprefix q (length u).
Proof.
 reflexivity.
Qed.

Lemma qprefix_ok q n : PrefixSeq (qprefix q n) (qseq q).
Proof.
 red. now rewrite qprefix_length.
Qed.

Lemma qprefix_alt q n : qprefix q n = firstn n (qword q (invA_up q n)).
Proof.
 rewrite <- qseq_take_A. symmetry. apply firstn_take. apply invA_up_spec.
Qed.

Lemma qprefix_letters q n : Forall (fun a => a <= q) (qprefix q n).
Proof.
 induction n.
 - constructor.
 - rewrite take_S. apply Forall_app. split; trivial.
   repeat constructor. apply qseq_letters.
Qed.

Lemma qprefix_A_qword q p : qprefix q (A q p) = qword q p.
Proof.
 apply qseq_take_A.
Qed.

Lemma qprefix_prefix_qword q n p :
  n <= A q p -> Prefix (qprefix q n) (qword q p).
Proof.
 intros H. rewrite <- qprefix_A_qword. now apply Prefix_take.
Qed.

Lemma qprefix_firstn_qword q n p :
  n <= A q p -> qprefix q n = firstn n (qword q p).
Proof.
 intros H. rewrite <- (take_length n (qseq q)) at 2.
 apply Prefix_equiv. now apply qprefix_prefix_qword.
Qed.

Lemma qword_prefix q p p' : p <= p' -> Prefix (qword q p) (qword q p').
Proof.
 apply napply_prefix_mono, qsubst_prolong.
Qed.

(** Full decomposition of any prefix of qword, then qseq (used in Lim) *)

Definition qwords q (l:list nat) : word := flat_map (qword q) l.

Lemma qwords_singl q n : qwords q [n] = qword q n.
Proof.
 unfold qwords. simpl. now apply app_nil_r.
Qed.

Lemma qwords_app q l l' : qwords q (l++l') = qwords q l ++ qwords q l'.
Proof.
 apply flat_map_app.
Qed.

Lemma qwords_cons q a l : qwords q (a::l) = qword q a ++ qwords q l.
Proof.
 change (a::l) with ([a]++l). now rewrite qwords_app, qwords_singl.
Qed.

Lemma qsubst_qwords q l :
 qsubstw q (qwords q l) = qwords q (map S l).
Proof.
 induction l; simpl; auto. now rewrite qsubstw_app, IHl, qword_S.
Qed.

Lemma decomp_prefix_qword q w n l :
 Prefix w (qword q n) -> l = rev (decomp q (length w)) -> w = qwords q l.
Proof.
 revert w l. induction n as [n IH] using lt_wf_ind.
 intros w l P.
 destruct (Nat.le_gt_cases n (S q)).
 - clear IH. rewrite qword_low in * by trivial.
   destruct (Prefix_cons_inv _ _ _ P) as [->|(w' & E' & P')].
   + simpl. now intros ->.
   + assert (LE := Prefix_len _ _ P'). rewrite seq_length in LE.
     apply Prefix_seq in P'.
     rewrite E'. simpl length. set (p := length w') in *.
     rewrite decomp_low by lia.
     replace (S _ -1) with p by lia. intros ->. simpl.
     rewrite app_nil_r, qword_low, <-P' by lia. trivial.
 - assert (P' := P). destruct P' as ([|a u] & E).
   + rewrite app_nil_r in E. rewrite E. rewrite qword_len.
     replace (decomp q (A q n)) with [n].
     2:{ symmetry; apply decomp_carac; try constructor; simpl; auto. }
     intros ->. simpl. now rewrite app_nil_r.
   + assert (LT : length w < A q n).
     { rewrite <- qword_len, <- E, app_length. simpl. lia. }
     clear  E.
     destruct n; [lia|].
     rewrite qword_eqn in P by lia.
     apply Prefix_app in P. destruct P as [P|(w' & -> & P)].
     * apply (IH n); auto.
     * rewrite app_length, qword_len in *.
       rewrite Nat.add_comm, decomp_plus_A by (simpl in LT; lia).
       rewrite rev_app_distr. intros ->. rewrite qwords_app.
       simpl. f_equal. now rewrite app_nil_r.
       apply (IH (n-q)); auto. lia.
Qed.

Lemma decomp_prefix_qseq q n :
 take n (qseq q) = qwords q (rev (decomp q n)).
Proof.
 assert (H := invA_spec q n). set (m := invA q n) in *.
 assert (H' : n <= A q (S m)) by lia. clear H. clearbody m.
 apply (decomp_prefix_qword _ _ (S m)).
 - apply Prefix_nth_nat. intros p a. rewrite take_length. intros LT.
   rewrite take_nth by trivial.
   apply qseq_alt; lia.
 - now rewrite take_length.
Qed.

Lemma renorm_qwords q l :
 Delta q l -> qwords q (rev (renorm q l)) = qwords q (rev l).
Proof.
 unfold renorm.
 generalize (Nat.le_refl (length l)). generalize (length l) at 2 3.
 intro n. revert l.
 induction n as [[|n] IH] using lt_wf_ind; intros l Hl D.
 - now destruct l.
 - destruct l as [|i l]; simpl in *; trivial.
   apply Delta_inv in D.
   destruct (renorm_loop q l n) as [|a l'] eqn:E.
   + simpl. rewrite qwords_app.
     rewrite <- (IH n); trivial; try lia. now rewrite E.
   + case Nat.eqb_spec; intros.
     * rewrite IH; try lia.
       2:{ change (length (S a :: l')) with (length (a::l')).
           rewrite <- E. rewrite renorm_loop_length; lia. }
       2:{ apply Delta_S_cons. rewrite <- E.
           apply renorm_loop_delta; trivial. lia. }
       subst a. simpl. rewrite !qwords_app, !qwords_singl.
       rewrite qword_eqn by lia.
       replace (i+q-q) with i by lia. rewrite app_assoc. f_equal.
       rewrite <- (qwords_singl q (i+q)), <- qwords_app.
       change (_++_) with (rev (i+q::l')). rewrite <- E.
       apply IH; trivial; try lia.
     * rewrite <- E. simpl. rewrite !qwords_app. f_equal.
       apply IH; trivial; lia.
Qed.

Lemma prefix_qseq_laxdecomp q n l :
 DeltaRev q l -> sumA q l = n -> take n (qseq q) = qwords q l.
Proof.
 rewrite <- Delta_rev. rewrite <- (rev_involutive l) at 2 3.
 rewrite sumA_rev. intros D E.
 rewrite <- renorm_qwords by trivial.
 rewrite decomp_prefix_qseq. f_equal. f_equal.
 apply decomp_carac. now apply renorm_delta. now rewrite renorm_sum.
Qed.

Lemma count_qseq_decomp q n a :
 count (qseq q) a n =
  list_sum (map (fun m => nbocc a (qword q m)) (decomp q n)).
Proof.
 rewrite count_nbocc, decomp_prefix_qseq. unfold qwords.
 rewrite flat_map_concat_map, nbocc_concat.
  now rewrite map_map, map_rev, list_sum_rev.
Qed.

(** Occurrences of letters when applying qsubst *)

Lemma nbocc_qsubst q : q<>0 ->
 forall w,
 nbocc 0 (qsubstw q w) = nbocc q w /\
 nbocc q (qsubstw q w) = nbocc (q-1) w + nbocc q w /\
 forall p, p<q-1 -> nbocc (S p) (qsubstw q w) = nbocc p w.
Proof.
 induction w; simpl.
 - repeat split; lia.
 - simpl. rewrite !nbocc_app.
   destruct IHw as (IHw0 & IHwq & IHw).
   rewrite IHw0, IHwq. repeat split.
   + unfold qsubst. case Nat.eqb_spec; simpl; try lia.
     case Nat.eqb_spec; simpl; try lia.
   + unfold qsubst. case Nat.eqb_spec; try lia.
     * intros ->. cbn -[Nat.eqb]. rewrite Nat.eqb_refl.
       do 2 (case Nat.eqb_spec; try lia).
     * intros N. case Nat.eqb_spec; try lia.
       { intros ->. replace (S (q-1)) with q by lia. simpl.
         rewrite Nat.eqb_refl. lia. }
       { intros N'. cbn -[Nat.eqb]. case Nat.eqb_spec; try lia. }
   + intros p Hp. rewrite nbocc_app. rewrite (IHw p Hp).
     unfold qsubst. case Nat.eqb_spec; try lia.
     * intros ->. cbn -[Nat.eqb].
       do 3 (case Nat.eqb_spec; try lia).
     * intros N. simpl. lia.
Qed.

(* In [napply] of [qsubst], the initial letter doesn't matter much :
   low letters become [q] after some rounds of [qsubst], while
   unexpected letters stay large. *)

Lemma napply_qsubst_shift q p n : p+n <= q \/ q < p ->
 napply (qsubst q) n [p] = [p+n].
Proof.
 revert p.
 induction n; simpl; intros.
 - f_equal. lia.
 - rewrite app_nil_r. unfold qsubst at 2.
   case Nat.eqb_spec; try lia. intros. rewrite IHn. f_equal; lia. lia.
Qed.

Lemma napply_qsubst_is_qword q p n : p <= q -> q <= n+p ->
 napply (qsubst q) n [p] = qword q (n+p-q).
Proof.
 intros. replace n with ((n+p-q)+(q-p)) by lia.
 rewrite napply_add, napply_qsubst_shift by lia.
 unfold qword; f_equal. lia. f_equal; lia.
Qed.

(** We hence have an easy bound on lengths of n-iterates of qsubst on
   single letters. *)

Definition NapplySizeBound s n N :=
  forall a:letter, length (napply s n [a]) <= N.

Lemma Bound_A q n : NapplySizeBound (qsubst q) n (A q n).
Proof.
 unfold NapplySizeBound. intros.
 destruct (Nat.le_gt_cases a q).
 - destruct (Nat.le_gt_cases q (n+a)).
   + rewrite napply_qsubst_is_qword by lia. rewrite qword_len.
     apply A_mono. lia.
   + rewrite napply_qsubst_shift by lia. simpl. apply A_nz.
 - rewrite napply_qsubst_shift by lia. simpl. apply A_nz.
Qed.

(** Counting occurrences of [q] and [0] in [qword] *)

Lemma nbocc_q_qword q n : nbocc q (qword q n) = A q (n-q).
Proof.
 induction n as [n IH] using lt_wf_ind.
 destruct (Nat.le_gt_cases n q).
 - rewrite qword_low by lia. simpl.
   rewrite Nat.eqb_refl, nbocc_notin.
   2:{ rewrite in_seq; lia. }
   now replace (n-q) with 0 by lia.
 - destruct n; try lia.
   rewrite qword_eqn, nbocc_app by lia.
   rewrite IH by lia.
   rewrite IH by lia.
   now replace (S n - q) with (S (n-q)) by lia.
Qed.

Lemma nbocc_0_qword q n : q<>0 -> nbocc 0 (qword q (S n)) = A q (n-q).
Proof.
 intros Hq.
 induction n as [n IH] using lt_wf_ind.
 destruct (Nat.le_gt_cases (S n) q).
 - rewrite qword_low by lia. simpl.
   rewrite nbocc_notin by (rewrite in_seq; lia).
   case Nat.eqb_spec; try lia.
   now replace (n-q) with 0 by lia.
 - destruct n; try lia.
   rewrite qword_eqn, nbocc_app by lia.
   rewrite IH by lia.
   destruct (Nat.le_gt_cases (S n) q).
   + replace (S n - q) with 0 by lia. replace (n-q) with 0 by lia. simpl.
     case Nat.eqb_spec; try lia.
   + replace (S n - q) with (S (n-q)) by lia.
     rewrite IH by lia. now simpl.
Qed.


(* Special case q=2

 0 -> 1
 1 -> 2
 2 -> 20

 Occurrence matrix :

 001
 100
 011

*)

Lemma nbocc_qsubst2 w :
 nbocc 0 (qsubstw 2 w) = nbocc 2 w /\
 nbocc 1 (qsubstw 2 w) = nbocc 0 w /\
 nbocc 2 (qsubstw 2 w) = nbocc 1 w + nbocc 2 w.
Proof.
 assert (H:2<>0) by lia.
 destruct (nbocc_qsubst 2 H w) as (H0 & H1 & Hp). repeat split; trivial.
 apply Hp; lia.
Qed.

Definition tripleocc w := (nbocc 0 w, nbocc 1 w, nbocc 2 w).

Definition occurmatrix '(x,y,z) : nat*nat*nat := (z,x,y+z).

Lemma nbocc_qsubst2_bis w :
 tripleocc (qsubstw 2 w) = occurmatrix (tripleocc w).
Proof.
 unfold tripleocc.
 now destruct (nbocc_qsubst2 w) as (-> & -> & ->).
Qed.

Lemma len_nbocc_012 w :
  Forall (fun a => a <= 2) w ->
  length w = nbocc 0 w + nbocc 1 w + nbocc 2 w.
Proof.
 intros. rewrite nbocc_total_le with (k:=2); simpl; auto; lia.
Qed.

Lemma len_qsubst q w :
 length (qsubstw q w) = length w + nbocc q w.
Proof.
 induction w; simpl; auto.
 rewrite app_length, IHw.
 unfold qsubst at 1.
 case Nat.eqb_spec; simpl; lia.
Qed.

(* Special case q=3

 0 -> 1
 1 -> 2
 2 -> 3
 3 -> 30

 Occurrence matrix :

 0001
 1000
 0100
 0011

*)

Lemma nbocc_qsubst3 w :
 nbocc 0 (qsubstw 3 w) = nbocc 3 w /\
 nbocc 1 (qsubstw 3 w) = nbocc 0 w /\
 nbocc 2 (qsubstw 3 w) = nbocc 1 w /\
 nbocc 3 (qsubstw 3 w) = nbocc 2 w + nbocc 3 w.
Proof.
 assert (H:3<>0) by lia.
 destruct (nbocc_qsubst 3 H w) as (H0 & H1 & Hp). repeat split; trivial.
 apply Hp; lia.
 apply Hp; lia.
Qed.

Definition fourocc w := (nbocc 0 w, nbocc 1 w, nbocc 2 w, nbocc 3 w).

Definition occurmatrix4 '(x,y,z,t) : nat*nat*nat*nat := (t,x,y,z+t).

Lemma nbocc_qsubst3_bis w :
 fourocc (qsubstw 3 w) = occurmatrix4 (fourocc w).
Proof.
 unfold fourocc.
 now destruct (nbocc_qsubst3 w) as (-> & -> & -> & ->).
Qed.

Lemma len_nbocc_0123 w :
  Forall (fun a => a <= 3) w ->
  length w = nbocc 0 w + nbocc 1 w + nbocc 2 w + nbocc 3 w.
Proof.
 intros. rewrite nbocc_total_le with (k:=3); simpl; auto; lia.
Qed.

(* From a Prefix of napply of a word to a prefix of napply of a letter *)

Lemma napply_prefix s n u v :
  NoErase s -> v<>[] ->
  Prefix u (napply s n v) ->
  exists w t a,
    Prefix (w++[a]) v /\ u = napply s n w ++ t /\ Prefix t (napply s n [a]).
Proof.
 intros NE. revert u.
 induction v; try easy.
 - intros u _. rewrite napply_cons. intros Pr.
   apply Prefix_app in Pr. destruct Pr as [Pr|(u' & E & Pr)].
   + exists [], u, a. rewrite napply_nil. simpl. split; auto. now exists v.
   + destruct (list_eq_dec Nat.eq_dec v []) as [->|NE'].
     * rewrite napply_nil in Pr. apply Prefix_nil in Pr. subst u'.
       rewrite app_nil_r in E.
       exists [], u, a. rewrite napply_nil.
       repeat split; subst; auto using Prefix_id.
     * destruct (IHv u' NE' Pr) as (w & t & b & Hv & E' & Ht).
       exists (a::w), t, b. repeat split; auto.
       { simpl. now apply Prefix_cons. }
       { now rewrite napply_cons, <- app_assoc, <- E', <- E. }
Qed.

(** Saari's Lemma 4 : decomposition of a prefix of s^n(a),
    leaving alone a final part whose size is below a certain threshold *)

Lemma Saari_lemma4 s a n w G M1 MG : G<>0 -> n<>0 ->
 NapplySizeBound s 1 M1 -> NapplySizeBound s G MG ->
 NoErase s ->
 Prefix w (napply s n [a]) ->
 exists l : list (nat * word), exists z,
  w = flat_map (fun '(ni,ui) => napply s ni ui) l ++ z
  /\ Forall (fun '(ni,ui) => length ui <= M1 /\ G <= ni < n) l
  /\ DeltaRev 1 (map fst l)
  /\ length z <= MG.
Proof.
 intros HG. revert a w.
 induction n as [n IH] using lt_wf_ind.
 intros a w Hn B1 BG NE Pr.
 destruct (Nat.le_gt_cases n G).
 - exists []. exists w. simpl. repeat split; auto. constructor.
   apply Prefix_len in Pr.
   etransitivity; [apply Pr|]. red in BG.
   rewrite <- (BG a). now apply napply_mono.
 - destruct n as [|n]; try easy.
   simpl in Pr. rewrite app_nil_r in Pr.
   destruct (napply_prefix s n w (s a) NE (NE a) Pr)
     as (w1 & w2 & b & H1 & H2 & H3).
   destruct (IH n (Nat.lt_succ_diag_r n) b w2)
     as (l & z & EQ & F & D & LE); auto; try lia.
   exists ((n,w1)::l), z; repeat split; auto.
   + simpl. now rewrite <- app_assoc, <-EQ.
   + constructor; try split; auto; try lia.
     * rewrite <- (B1 a). simpl. rewrite app_nil_r.
       apply Prefix_len in H1. rewrite app_length in H1. simpl in H1. lia.
     * clear -F. rewrite Forall_forall in *.
       intros (m,u) IN. apply F in IN. lia.
   + simpl. apply DeltaRev_alt. split; auto.
     intros y. rewrite in_map_iff. intros ((m,y') & <- & IN). simpl.
     rewrite Forall_forall in F. apply F in IN. lia.
Qed.

(* Same idea in a simpler version (decompose in letters instead of words).
   Should be enough for qsubst *)

Definition Reachable s a b := exists n, In b (napply s n [a]).

Lemma Reachable_trans s a b c :
  Reachable s a b -> Reachable s b c -> Reachable s a c.
Proof.
 intros (n,Hb) (m,Hc). exists (m+n). rewrite napply_add.
 destruct (in_split _ _ Hb) as (u & v & ->).
 rewrite napply_app, napply_cons, !in_app_iff. intuition.
Qed.

Lemma Saari_lemma4_bis s a n w G MG : G<>0 -> n<>0 ->
 NapplySizeBound s G MG ->
 NoErase s ->
 Prefix w (napply s n [a]) ->
 exists l : list (nat * letter), exists z,
  w = flat_map (fun '(ni,ui) => napply s ni [ui]) l ++ z
  /\ Forall (fun '(ni,ui) => G <= ni /\ Reachable s a ui) l
  /\ length z <= MG.
Proof.
 intros HG. revert a w.
 induction n as [n IH] using lt_wf_ind.
 intros a w Hn BG NE Pr.
 destruct (Nat.le_gt_cases n G).
 - exists []. exists w. simpl. repeat split; auto.
   apply Prefix_len in Pr.
   etransitivity; [apply Pr|]. red in BG.
   rewrite <- (BG a). now apply napply_mono.
 - destruct n as [|n]; try easy.
   simpl in Pr. rewrite app_nil_r in Pr.
   destruct (napply_prefix s n w (s a) NE (NE a) Pr)
     as (w1 & w2 & b & H1 & H2 & H3).
   destruct (IH n (Nat.lt_succ_diag_r n) b w2)
     as (l & z & EQ & F & LE); auto; try lia. clear IH.
   exists (map (fun u => (n,u)) w1 ++ l), z; repeat split; auto.
   + simpl. rewrite H2, EQ. rewrite app_assoc. f_equal.
     rewrite flat_map_app. f_equal.
     now rewrite flatmap_map, napply_flat_map.
   + apply Forall_app; split.
     * rewrite Forall_forall. intros (p,c).
       rewrite in_map_iff. intros (x & [= <- <-] & IN). split. lia.
       exists 1. simpl. rewrite app_nil_r. destruct H1 as (w3 & <-).
       rewrite !in_app_iff; intuition.
     * rewrite Forall_forall in *. intros (p,c) IN.
       destruct (F (p,c) IN). split; trivial. eapply Reachable_trans; eauto.
       exists 1. simpl. rewrite app_nil_r. destruct H1 as (w3 & <-).
       rewrite !in_app_iff; intuith.
Qed.

Lemma Reachable_qsubst q p :
  p <= q -> forall p', Reachable (qsubst q) p p' <-> p' <= q.
Proof.
 intros Hp p'. split.
 - intros (n,H).
   assert (F : Forall (fun a => a <= q) [p]) by repeat (constructor; try lia).
   apply (napply_qsubst_letters _ n) in F.
   rewrite Forall_forall in F. now apply F.
 - intros Hq.
   apply Reachable_trans with q.
   + exists (q-p). rewrite napply_qsubst_shift by lia.
     replace (p+(q-p)) with q; simpl; lia.
   + apply Reachable_trans with 0.
     * exists 1. simpl. unfold qsubst. rewrite Nat.eqb_refl. simpl; intuition.
     * exists p'. rewrite napply_qsubst_shift by lia. simpl. lia.
Qed.

Lemma Saari_lemma4_qsubst q n w G : G<>0 -> n<>0 ->
 Prefix w (qword q n) ->
 exists l : list nat, exists z,
  w = flat_map (qword q) l ++ z
  /\ Forall (Nat.le G) l
  /\ length z <= A q (q+G).
Proof.
 intros HG Hn Pref.
 destruct (Saari_lemma4_bis (qsubst q) q n w (q+G) (A q (q+G))) as
  (l & z & E & F & LE); trivial; try lia.
 - apply Bound_A.
 - apply qsubst_noerase.
 - exists (map (fun '(ni,ui) => ni+ui-q) l); exists z; repeat split; trivial.
   + rewrite E. f_equal. rewrite !flat_map_concat_map. f_equal.
     rewrite map_map. simpl. apply map_ext_in.
     intros (ni,ui) IN.
     rewrite Forall_forall in F. destruct (F _ IN) as (U,V).
     rewrite Reachable_qsubst in V; try lia.
     rewrite napply_qsubst_is_qword; trivial; try lia.
   + rewrite Forall_map.
     rewrite Forall_forall in *. intros (p,c) IN.
     destruct (F _ IN) as (U,V).
     rewrite Reachable_qsubst in V; try lia.
Qed.

Lemma count_qseq q n p :
  n <= A q p ->
  count (qseq q) 0 n = nbocc 0 (firstn n (qword q p)).
Proof.
 intros LE.
 rewrite count_nbocc. f_equal. now apply qprefix_firstn_qword.
Qed.

(** Is there a 0 at position n in [qseq q] ?
    If so, there's a q at the previous position. *)

Definition is_q0 q n := (qseq q n =? 0).

Lemma rank_0_pred q n : rank q n = Some 0 -> bounded_rank q (pred n) = q.
Proof.
 unfold rank. destruct (decomp q n) as [|r l] eqn:E; try easy.
 intros [= ->].
 unfold bounded_rank, rank.
 assert (D := decomp_delta q n).
 rewrite E in D.
 rewrite (@decomp_carac q (pred n) l).
 2:{ now apply Delta_inv in D. }
 2:{ now rewrite <- (decomp_sum q n), E. }
 destruct l as [|r' l']; trivial. simpl.
 inversion_clear D. lia.
Qed.

Lemma q0_pred_q q n : qseq q n = 0 -> qseq q (pred n) = q.
Proof.
 rewrite !qseq_bounded_rank.
 unfold bounded_rank at 1, omin.
 destruct (Nat.eq_dec q 0) as [->|Hq].
 - unfold bounded_rank, omin. do 2 destruct rank; lia.
 - destruct rank as [r|] eqn:E; try lia. intros Hr.
   replace r with 0 in * by lia. now apply rank_0_pred.
Qed.

(** Given two consecutive prefixes of [qseq], one of the two is
    a [qsubst] of a smaller prefix. *)

Lemma qseq_take_inv q n : q<>0 ->
  qprefix q (n + if is_q0 q n then 1 else 0) =
  qsubstw q (qprefix q (f q n)).
Proof.
 intros Hq.
 set (l := rev (decomp q n)).
 set (l' := map pred l).
 assert (D' : DeltaRev q l').
 { unfold l', l. rewrite map_rev, DeltaRev_rev.
   apply Delta_map with (S q). lia. apply decomp_delta. }
 assert (E : sumA q l' = f q n).
 { unfold l', l. rewrite map_rev, sumA_rev. symmetry. apply f_decomp. }
 rewrite (prefix_qseq_laxdecomp q (f q n) l') by trivial.
 rewrite qsubst_qwords; auto.
 apply prefix_qseq_laxdecomp.
 - unfold l', l. rewrite map_map, map_rev, DeltaRev_rev.
   apply Delta_map with (S q). lia. apply decomp_delta.
 - unfold l', l. clear -Hq. rewrite map_map, map_rev, sumA_rev.
   destruct (decomp q n) as [|r l] eqn:E.
   + simpl. rewrite <- (decomp_sum q n), E. simpl.
     unfold is_q0; rewrite qseq_bounded_rank. unfold bounded_rank.
     replace (rank q 0) with (@None nat).
     2:{symmetry. now rewrite rank_none. }
     simpl. case Nat.eqb_spec; lia.
   + unfold is_q0. rewrite qseq_bounded_rank. unfold bounded_rank.
     unfold rank. rewrite E. simpl omin.
     case Nat.eqb_spec; intros.
     * replace r with 0 in * by lia. simpl.
       rewrite map_ext_in with (g:=id), map_id.
       2:{ intros a Ha. unfold id.
           assert (D := decomp_delta q n).
           rewrite E in D. apply Delta_nz' in D; try lia.
           assert (a<>0); try lia. now intros ->. }
       rewrite <- (decomp_sum q n), E. simpl. lia.
     * rewrite map_ext_in with (g:=id), map_id.
       now rewrite <- E, decomp_sum.
       assert (D := decomp_delta q n).
       rewrite E in D. apply Delta_nz in D; try lia.
       intros a Ha. unfold id. assert (a<>0); try lia. now intros ->.
Qed.

Lemma PrefixSeq_0 u : PrefixSeq u (qseq 0) <-> u = repeat 0 (length u).
Proof.
 assert (E : forall n p, map (qseq 0) (seq p n) = repeat 0 n).
 { induction n; simpl; intros; auto.
   f_equal; auto. generalize (qseq_letters 0 p). lia. }
 split.
 - unfold PrefixSeq, take. now rewrite E.
 - now rewrite <- (E (length u) 0).
Qed.

Lemma apply_qsubst_0 n : qsubstw 0 (repeat 0 n) = repeat 0 (2*n).
Proof.
 induction n; simpl; trivial.
 rewrite Nat.add_succ_r. simpl. now rewrite IHn.
Qed.

Lemma qsubst_prefix_inv q u :
  PrefixSeq u (qseq q) ->
  { v & { w |
      u = qsubstw q v ++ w /\ PrefixSeq v (qseq q) /\ (w=[]\/w=[q]) }}.
Proof.
 destruct (Nat.eq_dec q 0) as [Q|Q].
 { intros P. subst q.
   set (n := length u).
   exists (repeat 0 (n/2)), (repeat 0 (n mod 2)); repeat split.
   - apply PrefixSeq_0 in P. rewrite P.
     rewrite apply_qsubst_0, <- repeat_app. f_equal. apply Nat.div_mod_eq.
   - apply PrefixSeq_0. now rewrite repeat_length.
   - generalize (Nat.mod_upper_bound n 2).
     destruct (n mod 2) as [|[|q]]; try lia; simpl; intuition. }
 intros P.
 assert (E := qseq_take_inv q (length u) Q).
 remember (length u) as n eqn:U.
 unfold is_q0 in *.
 destruct (Nat.eqb_spec (qseq q n) 0) as [N|N].
 - rewrite Nat.add_1_r, take_S in E.
   rewrite N in E.
   destruct n.
   + exfalso. now rewrite qseq_q_0 in N.
   + rewrite take_S, <- app_assoc in E.
     assert (f q (S n) <> 0).
     { intros H. rewrite H in E. simpl in E.
       apply (f_equal (@rev _)) in E. now rewrite rev_app_distr in E. }
     replace (f q (S n)) with (S (f q (S n) - 1)) in E by lia.
     rewrite take_S, qsubstw_app in E. simpl in E. rewrite app_nil_r in E.
     set (m := f q (S n) - 1) in *.
     exists (take m (qseq q)), [q]; repeat split.
     * apply (f_equal (@rev _)) in E. rewrite !rev_app_distr in E.
       simpl in E.
       unfold qsubst in E at 1.
       destruct (Nat.eqb_spec (qseq q m) q) as [M|M]; try easy.
       simpl in E. injection E as N' E. apply rev_inj in E.
       rewrite <- E, P, <- U, take_S. f_equal. now f_equal.
     * red. f_equal. now rewrite take_length.
     * now right.
 - rewrite Nat.add_0_r in E.
   exists (take (f q n) (qseq q)), []; repeat split.
   + rewrite <- E, app_nil_r. rewrite P. now f_equal.
   + red. f_equal. now rewrite take_length.
   + now left.
Qed.

(** The preimage by qsubst is unique if it exists *)

Lemma qsubstw_inv q :
  forall u v, qsubstw q u = qsubstw q v -> u = v.
Proof.
 assert (H : forall u v,
             qsubstw q (rev u) = qsubstw q (rev v) -> u = v).
 { induction u as [|a u]; destruct v as [|b v]; simpl; auto.
   - rewrite qsubstw_app. simpl. rewrite app_nil_r.
     intros E. symmetry in E. apply length_zero_iff_nil in E.
     rewrite app_length in E. unfold qsubst in E.
     destruct (Nat.eqb b q); simpl in E; lia.
   - rewrite qsubstw_app. simpl. rewrite app_nil_r.
     intros E. apply length_zero_iff_nil in E.
     rewrite app_length in E. unfold qsubst in E.
     destruct (Nat.eqb a q); simpl in E; lia.
   - rewrite !qsubstw_app. simpl. rewrite !app_nil_r.
     unfold qsubst. simpl.
     do 2 case Nat.eqb_spec; intros; subst.
     + apply app_inv' in H; trivial. f_equal. apply IHu, H.
     + apply (f_equal (@rev nat)) in H. now rewrite !rev_app_distr in H.
     + apply (f_equal (@rev nat)) in H. now rewrite !rev_app_distr in H.
     + apply app_inv' in H; trivial.
       destruct H as (H,[= ->]). f_equal. apply IHu, H. }
 intros u v. rewrite <- (rev_involutive u), <- (rev_involutive v).
 intros E. apply H in E. now f_equal.
Qed.

(** More on PrefixSeq *)

Lemma PrefixSeq_app_r u v f : PrefixSeq (u++v) f -> PrefixSeq u f.
Proof.
 unfold PrefixSeq, take. rewrite app_length, seq_app, map_app. intros E.
 apply app_inv in E. apply E. now rewrite map_length, seq_length.
Qed.

Lemma Prefix_PrefixSeq u v f : Prefix u v -> PrefixSeq v f -> PrefixSeq u f.
Proof.
 intros (u' & <-). apply PrefixSeq_app_r.
Qed.

Lemma PrefixSeq_incl w u v :
  length u <= length v -> PrefixSeq u w -> PrefixSeq v w -> Prefix u v.
Proof.
 unfold PrefixSeq. intros H -> ->. now apply Prefix_take.
Qed.

Lemma PrefixSeq_unique w u v :
  length u = length v -> PrefixSeq u w -> PrefixSeq v w -> u = v.
Proof.
 intros. apply Prefix_antisym; eapply PrefixSeq_incl; eauto; lia.
Qed.

Lemma PrefixSeq_alt s a :
  NoErase s -> Prolong s a ->
  forall u,
    PrefixSeq u (subst2seq s a) <-> Prefix u (napply s (length u) [a]).
Proof.
 intros NE PR u. unfold PrefixSeq.
 split.
 - generalize (length u). intros n Hu.
   rewrite Prefix_nth_nat. intros m b Hm.
   subst u. rewrite take_length in Hm.
   rewrite take_nth by trivial.
   rewrite <- subst2seq_indep; trivial; lia.
 - set (n := length u). intros Hu.
   symmetry. apply take_carac; trivial.
   intros m b Hm. rewrite Prefix_nth_nat in Hu.
   rewrite Hu by trivial. symmetry. apply subst2seq_indep; trivial. lia.
Qed.

Lemma PrefixSeq_alt' s a :
  NoErase s -> Prolong s a ->
  forall u,
    PrefixSeq u (subst2seq s a) <-> exists m, Prefix u (napply s m [a]).
Proof.
 intros NE PR u. rewrite PrefixSeq_alt by trivial.
 split.
 - intros H. now exists (length u).
 - intros (m,H). destruct (Nat.le_gt_cases m (length u)) as [L|L].
   + eapply Prefix_trans; eauto. apply napply_prefix_mono; trivial.
   + eapply Prefix_Prefix; eauto.
     * apply Nat.lt_le_incl, noerase_prolong_napply_len; trivial.
     * apply napply_prefix_mono; trivial; lia.
Qed.

Lemma PrefixSeq_apply s a :
  NoErase s -> Prolong s a ->
  forall u,
   PrefixSeq u (subst2seq s a) ->
   PrefixSeq (apply s u) (subst2seq s a).
Proof.
  intros NE PR u.
  rewrite !PrefixSeq_alt' by trivial.
  intros (m,(u',E)). exists (S m).
  rewrite napply_alt, <- E, apply_app. now exists (apply s u').
Qed.

Lemma PrefixSeq_napply s a n :
  NoErase s -> Prolong s a ->
  forall u,
   PrefixSeq u (subst2seq s a) ->
   PrefixSeq (napply s n u) (subst2seq s a).
Proof.
  intros NE PR.
  induction n; trivial.
  intros u Hu. simpl. apply IHn, PrefixSeq_apply; trivial.
Qed.

Lemma qsubstw_prefix q u :
 PrefixSeq u (qseq q) -> PrefixSeq (qsubstw q u) (qseq q).
Proof.
  apply PrefixSeq_apply. apply qsubst_noerase. apply qsubst_prolong.
Qed.

(** A nonerasing substitution can be applied to an infinite word *)

Definition SubstSeqSeq (s : subst)(f g : sequence) :=
 forall u, PrefixSeq u f -> PrefixSeq (apply s u) g.

Definition applyseq (s : subst) (f : sequence) :=
  fun n => nth n (apply s (take (S n) f)) 0.

Lemma applyseq_ok s f : NoErase s -> SubstSeqSeq s f (applyseq s f).
Proof.
 intros Hs u Hu. unfold PrefixSeq in *.
 symmetry. apply take_carac; trivial.
 intros m a Hm. unfold applyseq.
 rewrite nth_indep with (d' := 0); trivial.
 destruct (Nat.le_gt_cases (length u) (S m)) as [LE|GT].
 - assert (PR: Prefix u (take (S m) f)).
   { rewrite Hu. now apply Prefix_take. }
   destruct PR as (v & <-).
   rewrite apply_app, app_nth1; trivial.
 - assert (PR: Prefix (take (S m) f) u).
   { rewrite Hu. apply Prefix_take; lia. }
   destruct PR as (v & E). rewrite <- E.
   rewrite apply_app, app_nth1; trivial.
   red. rewrite <- (take_length (S m) f) at 1.
   now apply apply_grow.
Qed.

Lemma subst_seq_exists (s : subst)(f : sequence) :
 NoErase s -> exists g, SubstSeqSeq s f g.
Proof.
 intros Hs. exists (applyseq s f). now apply applyseq_ok.
Qed.

Lemma subst_seq_unique s f g g' :
 NoErase s -> SubstSeqSeq s f g -> SubstSeqSeq s f g' ->
 forall n, g n = g' n.
Proof.
 intros Hs Hg Hg' n.
 set (u := take (S n) f).
 assert (Hu : PrefixSeq u f).
 { red. unfold u. now rewrite take_length. }
 assert (n < length (apply s u)).
 { apply Nat.lt_le_trans with (length u).
   - unfold u. rewrite take_length; lia.
   - now apply apply_grow. }
 specialize (Hg u Hu).
 specialize (Hg' u Hu). red in Hg, Hg'.
 rewrite <- (take_nth g (length (apply s u)) n 0); auto.
 rewrite <- (take_nth g' (length (apply s u)) n 0); auto.
 now rewrite <- Hg, <- Hg'.
Qed.

Lemma qseq_fixpoint q n : applyseq (qsubst q) (qseq q) n = qseq q n.
Proof.
 apply (subst_seq_unique (qsubst q) (qseq q)).
 - apply qsubst_noerase.
 - apply applyseq_ok, qsubst_noerase.
 - intro u. apply qsubstw_prefix.
Qed.

(** Letters in qseq, what's before, what's after *)

Definition next_letter q a := if a =? q then 0 else S a.
Definition prev_letter q a := if a =? 0 then q else pred a.

Lemma next_letter_le q a : a <= q -> next_letter q a <= q.
Proof.
 intros Ha. unfold next_letter. case Nat.eqb_spec; lia.
Qed.

Lemma next_letter_q q : next_letter q q = 0.
Proof.
 unfold next_letter. now rewrite Nat.eqb_refl.
Qed.

Lemma prev_letter_le q a : a <= q -> prev_letter q a <= q.
Proof.
 intros Ha. unfold prev_letter. case Nat.eqb_spec; lia.
Qed.

Lemma next_letter_alt q a : a <= q -> next_letter q a = (S a) mod (S q).
Proof.
 intros Ha. unfold next_letter.
 case Nat.eqb_spec.
 - intros ->. symmetry. apply Nat.mod_same; lia.
 - intros. symmetry. apply Nat.mod_small. lia.
Qed.

Lemma prev_letter_alt q a : a <= q -> prev_letter q a = (a+q) mod (S q).
Proof.
 intros Ha. unfold prev_letter.
 case Nat.eqb_spec.
 - intros ->. symmetry. apply Nat.mod_small. lia.
 - intros. replace (a+q) with (a-1 + 1*(S q)) by lia.
   rewrite Nat.mod_add, Nat.mod_small; lia.
Qed.

Lemma next_prev_letter q a : a <= q -> next_letter q (prev_letter q a) = a.
Proof.
 intros Ha. unfold prev_letter.
 case Nat.eqb_spec.
 - intros ->. apply next_letter_q.
 - intros. unfold next_letter. case Nat.eqb_spec; lia.
Qed.

Lemma prev_next_letter q a : a <= q -> prev_letter q (next_letter q a) = a.
Proof.
 intros Ha. unfold next_letter.
 case Nat.eqb_spec; trivial.
 intros ->. unfold prev_letter. now rewrite Nat.eqb_refl.
Qed.

Lemma qsubst_next_letter q a : a<>q -> qsubst q a = [next_letter q a].
Proof.
 intros A. unfold qsubst, next_letter. case Nat.eqb_spec; auto; lia.
Qed.

Lemma qseq_prev_letter q p :
  qseq q p <> q -> qseq q (p-1) = prev_letter q (qseq q p).
Proof.
 intros Ha.
 assert (Ha' := qseq_letters q p).
 remember (qseq q p) as a eqn:Ea in *.
 rewrite qseq_bounded_rank in *.
 unfold bounded_rank, omin, rank in *.
 set (l := decomp q p) in *.
 destruct l as [|r l'] eqn:Hl; try lia.
 replace r with a in * by lia.
 rewrite decomp_pred. fold l. rewrite Hl. simpl.
 destruct a as [|a]; unfold prev_letter; simpl.
 - assert (D := decomp_delta q p). fold l in D. rewrite Hl in D.
   destruct l'; simpl; trivial. inversion_clear D. lia.
 - replace (a-q) with 0 by lia. simpl. lia.
Qed.

Lemma qseq_next_letter q p :
  qseq q (S p) <> q -> qseq q (S p) = next_letter q (qseq q p).
Proof.
 intros Ha. replace p with (S p-1) at 2 by lia.
 rewrite qseq_prev_letter; trivial. rewrite next_prev_letter; trivial.
 apply qseq_letters.
Qed.

Lemma qseq_next_qm1 q p : qseq q p = q-1 -> qseq q (S p) = q.
Proof.
 intros E.
 destruct (Nat.eq_dec (qseq q (S p)) q) as [E'|E']; trivial.
 rewrite qseq_next_letter, E; trivial.
 unfold next_letter.
 case Nat.eqb_spec; lia.
Qed.

Lemma all_letters_occur q a : a <= q -> qseq q (S a) = a.
Proof.
 intros Ha. rewrite qseq_bounded_rank. unfold bounded_rank, rank.
 replace (decomp q (S a)) with [a]. simpl. lia.
 symmetry. apply decomp_carac. constructor. simpl. rewrite A_base; lia.
Qed.

Lemma count_le_prev_letter q a n : a < q ->
  count (qseq q) a n <= count (qseq q) (prev_letter q a) n.
Proof.
 intros Ha.
 induction n as [[|n] IH] using lt_wf_ind; simpl; trivial.
 assert (IHn := IH n lia).
 do 2 case Nat.eqb_spec; intros E2 E1; try lia. clear IHn.
 destruct n; simpl.
 - rewrite qseq_q_0 in *. unfold prev_letter in *.
   destruct (Nat.eqb_spec a 0) as [->|E3]; lia.
 - specialize (IH n lia).
   assert (E3 := qseq_prev_letter q (S n) lia).
   rewrite E1 in E3.
   replace (S n -1) with n in E3 by lia. do 2 case Nat.eqb_spec; lia.
Qed.

Lemma count_le_lower_letter q a b n : a <= b < q ->
 count (qseq q) b n <= count (qseq q) a n.
Proof.
 intros (AB,BQ). induction AB; trivial.
 etransitivity; [ | apply IHAB; lia ].
 replace m with (prev_letter q (S m)) at 2 by easy.
 apply count_le_prev_letter; trivial.
Qed.

Lemma count_le_count_q q a n : count (qseq q) a n <= count (qseq q) q n.
Proof.
 destruct (Nat.eq_dec a q) as [->|Ha]; trivial.
 destruct (Nat.ltb_spec q a) as [Ha'|Ha'].
 - replace (count (qseq q) a n) with 0; try lia. symmetry. apply count_0.
   intros x _. generalize (qseq_letters q x); lia.
 - transitivity (count (qseq q) 0 n).
   + apply count_le_lower_letter; lia.
   + replace q with (prev_letter q 0) at 3 by easy.
     apply count_le_prev_letter; lia.
Qed.