coqbooks/src/thue_morse2.v

Require Import thue_morse.

Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Bool.

Import ListNotations.


(**
   The following lemmas and theorems are all related to
   squares of odd length in the Thue-Morse sequence.
   All squared factors of odd length have length 1 or 3.
*)

Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
Proof.
  intros n hd a tl. intros H I.
  assert (J: 4 < length a \/ length a <= 4).
  apply Nat.lt_ge_cases. destruct J.
  assert (exists b c d, a = b ++ [d;d] ++ c).
  generalize H0. generalize H. apply tm_step_consecutive_identical_length.
  destruct H1. destruct H1. destruct H1. rewrite H1 in H.

  replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
    with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
  apply tm_step_consecutive_identical' in H.

  assert (J: even (length (x0 ++ x)) = false).
  rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
  rewrite Nat.add_shuffle3 in I. rewrite Nat.add_comm in I.
  rewrite Nat.odd_add_even in I.
  rewrite app_length. rewrite Nat.add_comm. rewrite <- Nat.negb_odd.
  rewrite I. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT.
  reflexivity. rewrite H in J. inversion J.

  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
  rewrite <- app_assoc. apply app_inv_head_iff.
  reflexivity.

  apply Nat.le_lteq in H0. destruct H0. assumption.
  rewrite H0 in I. inversion I.
Qed.


(**
   New following lemmas and theorems are related to the size
   of squares in the Thue-Morse sequence, namely lengths of
   2^n or 3 * 2^n only.
*)

Lemma tm_step_shift_odd_prefix_even_squares :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> even (length a) = true
  -> odd (length hd) = true
  -> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
          /\ even (length hd') = true /\ length a = length b.
Proof.
  intros n hd a tl. intros H I J.

  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
  destruct W. rewrite e in J. simpl in J. rewrite Nat.odd_0 in J.
  inversion J.

  assert (Z: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
  destruct Z.
  exists (removelast hd). exists nil. exists ((last hd true)::nil++tl).
  split. rewrite app_nil_l. rewrite app_nil_l. rewrite app_nil_l.
  replace ((last hd true)::tl) with ([last hd true] ++ tl).
  rewrite app_assoc. rewrite <- app_removelast_last.
  rewrite H. rewrite e. rewrite app_nil_l. rewrite app_nil_l. reflexivity.
  assumption.
  split. rewrite app_removelast_last with (l := hd) (d := last hd true) in J.
  rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
  rewrite J. split. reflexivity. rewrite e. reflexivity. assumption.

  rewrite app_removelast_last with (l := hd) (d := true) in H.
  rewrite app_removelast_last with (l := a) (d := true) in H.
  rewrite app_assoc_reverse in H.
  rewrite app_removelast_last with (l := hd) (d := true) in J.
  rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
  rewrite app_removelast_last with (l := a) (d := true) in I.
  rewrite app_length in I. rewrite Nat.add_1_r in I.
  exists (removelast hd).
  rewrite app_assoc_reverse in H. rewrite app_assoc_reverse in H.
  replace (
    removelast hd ++ [last hd true] ++
    removelast a ++ [last a true] ++ removelast a ++ [last a true] ++ tl)
    with (
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
    ([last a true] ++ tl)) in H.
  assert (K: count_occ Bool.bool_dec (removelast hd) true
           = count_occ Bool.bool_dec (removelast hd) false).
  generalize J. generalize H. apply tm_step_count_occ.
  assert (L: count_occ Bool.bool_dec (
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) true
    = count_occ Bool.bool_dec (
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) false).
  assert (M: even (length (
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a))) = true).
  rewrite app_length. rewrite Nat.even_add_even. apply J.
  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
  rewrite Nat.even_add_even. rewrite app_length.
  rewrite Nat.add_1_l. assumption.
  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
  rewrite Nat.add_1_l. assumption.
  generalize M.
  replace (
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
    ([last a true] ++ tl))
    with ((
    removelast hd ++
    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) ++
    ([last a true] ++ tl)) in H.
  generalize H. apply tm_step_count_occ.

  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.

  assert (M: count_occ Bool.bool_dec (
    removelast hd ++
    ([last hd true] ++ removelast a)) true
    = count_occ Bool.bool_dec (
    removelast hd ++
    ([last hd true] ++ removelast a)) false).
  assert (N: even (length (
    removelast hd ++
    ([last hd true] ++ removelast a))) = true).
  rewrite app_length. rewrite Nat.even_add_even. assumption.
  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
  rewrite Nat.add_1_l. assumption.
  generalize N.
  rewrite app_assoc in H. generalize H. apply tm_step_count_occ.

  rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M.
  rewrite K in M. rewrite Nat.add_cancel_l in M.

  rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
  rewrite K in L. rewrite Nat.add_cancel_l in L.
  rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
  rewrite M in L. rewrite Nat.add_cancel_l in L.

  assert (O: forall (m: nat), m <> S (S m)).
  induction m. easy. apply not_eq_S. assumption.

  assert (N: last hd true = last a true).
  destruct (last hd true); destruct (last a true).
  reflexivity.
  rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
  rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
  rewrite L in M. apply O in M. contradiction M.
  rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
  rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
  rewrite <- L in M. symmetry in M. apply O in M. contradiction M.
  reflexivity.

  rewrite N in H. exists ([last a true] ++ removelast a).
  exists ([last a true] ++ tl). rewrite H.

  split. reflexivity.
  split. assumption.
  rewrite app_length. rewrite app_removelast_last with (l := a) (d := true).
  rewrite app_length. rewrite last_last. rewrite removelast_app.
  rewrite Nat.add_1_r. rewrite app_nil_r. reflexivity. easy.

  assumption.
  rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
  assumption. assumption. assumption. assumption.
Qed.

Lemma tm_step_normalize_prefix_even_squares :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> even (length a) = true
  -> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
          /\ even (length hd') = true /\ length a = length b.
Proof.
  intros n hd a tl. intros H I.
  assert (odd (length hd) = true \/ odd (length hd) = false).
  destruct (odd (length hd)). left. reflexivity. right. reflexivity.
  destruct H0.
  generalize H0. generalize I. generalize H.
  apply tm_step_shift_odd_prefix_even_squares.
  exists hd. exists a. exists tl.
  split. assumption. split. rewrite <- Nat.negb_odd. rewrite H0.
  reflexivity. reflexivity.
Qed.


Lemma tm_step_square_half : forall (n : nat) (hd a tl : list bool),
  tm_step (S n) = hd ++ a ++ a ++ tl
  -> even (length a) = true
  -> exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
    /\ length a = Nat.double (length a').
Proof.
  intros n hd a tl. intros H I.
  assert (
     exists (hd' b tl': list bool), tm_step (S n) = hd' ++ b ++ b ++ tl'
          /\ even (length hd') = true /\ length a = length b).
  generalize I. generalize H. apply tm_step_normalize_prefix_even_squares.
  destruct H0. destruct H0. destruct H0.
  destruct H0. destruct H1. rewrite H2 in I.
  rewrite <- tm_step_lemma in H0.
  assert (x = tm_morphism (firstn (Nat.div2 (length x)) (tm_step n))).
  apply tm_morphism_app2 with (tl := x0 ++ x0 ++ x1). apply H0.
  assumption.
  assert (x0 ++ x0 ++ x1 = tm_morphism (skipn (Nat.div2 (length x)) (tm_step n))).
  apply tm_morphism_app3. apply H0. assumption.

  assert (Z := H0).

  assert (H7: length (tm_morphism (tm_step n)) = length (tm_morphism (tm_step n))).
  reflexivity. rewrite Z in H7 at 2. rewrite tm_morphism_length in H7.
  rewrite app_length in H7.
  rewrite app_length in H7.
  rewrite Nat.Even_double with (n := length x) in H7.
  rewrite Nat.Even_double with (n := length x0) in H7.
  rewrite Nat.Even_double with (n := length (x0 ++ x1)) in H7.
  rewrite Nat.double_twice in H7.
  rewrite Nat.double_twice in H7.
  rewrite Nat.double_twice in H7.
  rewrite <- Nat.mul_add_distr_l in H7.
  rewrite <- Nat.mul_add_distr_l in H7.
  rewrite Nat.mul_cancel_l in H7.

  assert (x0 = tm_morphism (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n)))).
  apply tm_morphism_app2 with (tl := x0 ++ x1). symmetry. assumption.
  assumption.

  assert (x1 = tm_morphism (skipn (Nat.div2 (length (x0++x0)))
               (skipn (Nat.div2 (length x)) (tm_step n)))).
  apply tm_morphism_app3. symmetry. rewrite app_assoc_reverse. apply H4.
  rewrite app_length. rewrite Nat.even_add_even. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
              
  rewrite H3 in H0. rewrite H5 in H0. rewrite H6 in H0.
  rewrite <- tm_morphism_app in H0.
  rewrite <- tm_morphism_app in H0.
  rewrite <- tm_morphism_app in H0.
  rewrite <- tm_morphism_eq in H0.
  rewrite H0.
  exists (firstn (Nat.div2 (length x)) (tm_step n)).
  exists (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n))).
  exists (skipn (Nat.div2 (length (x0 ++ x0))) (skipn (Nat.div2 (length x)) (tm_step n))).
  split. reflexivity.
  rewrite firstn_length_le. rewrite <- Nat.Even_double. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  rewrite skipn_length.

  rewrite H7. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
  rewrite Nat.add_0_l. rewrite <- Nat.add_0_r at 1.
  rewrite <- Nat.add_le_mono_l.
  apply le_0_n. apply le_n. easy.

  rewrite <- Nat.Even_double in H7. rewrite <- Nat.Even_double in H7.
  rewrite Nat.add_assoc in H7.
  assert (Nat.even (2 * (length (tm_step n))) = true).
  apply Nat.even_mul. rewrite H7 in H5.
  rewrite Nat.even_add in H5.
  rewrite Nat.even_add in H5.
  rewrite I in H5. rewrite H1 in H5.
  apply Nat.EvenT_Even. apply Nat.even_EvenT.
  destruct (Nat.even (length (x0 ++ x1))). reflexivity.
  inversion H5.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
Qed.



Theorem tm_step_square_size : forall (n k j : nat) (hd a tl : list bool),
  tm_step (S n) = hd ++ a ++ a ++ tl
  -> length a = (S (Nat.double k)) * 2^j
  -> (k = 0 \/ k = 1).
Proof.
  intros n k j hd a tl.
  generalize hd. generalize a. generalize tl. induction j.
  - intros tl0 a0 hd0. intros H I. simpl in I. rewrite Nat.mul_1_r in I.
    assert (odd (length a0) = true). rewrite I.
    rewrite Nat.odd_succ. rewrite Nat.double_twice.
    apply Nat.even_mul.
    assert (J: length a0 < 4). generalize H0. generalize H.
    apply tm_step_odd_square.
    rewrite I in J.
    destruct k. left. reflexivity.
    destruct k. right. reflexivity.
    apply Nat.succ_lt_mono in J.
    apply Nat.lt_lt_succ_r in J.
    rewrite Nat.double_twice in J. replace (4) with (2*2) in J.
    rewrite <- Nat.mul_lt_mono_pos_l in J.
    apply Nat.succ_lt_mono in J.
    apply Nat.succ_lt_mono in J.
    apply Nat.nlt_0_r in J. contradiction J.
    apply Nat.lt_0_2. reflexivity.
  - intros tl0 a0 hd0. intros H I.
    assert (exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
          /\ length a0 = Nat.double (length a')).
    assert (even (length a0) = true).
    rewrite I. rewrite Nat.pow_succ_r'. rewrite Nat.mul_comm.
    rewrite <- Nat.mul_assoc. apply Nat.even_mul.
    generalize H0. generalize H. apply tm_step_square_half.
    destruct H0. destruct H0. destruct H0. destruct H0.
    rewrite H1 in I. rewrite Nat.pow_succ_r' in I. rewrite Nat.mul_comm in I.
    rewrite <- Nat.mul_assoc in I. rewrite Nat.double_twice in I.
    rewrite Nat.mul_cancel_l in I. rewrite Nat.mul_comm in I.
    generalize I.
    assert (tm_step (S n) = x ++ x0 ++ x0 ++ x1 ++ (map negb (tm_step n))).
    rewrite tm_build. rewrite H0.
    rewrite <- app_assoc. apply app_inv_head_iff.
    rewrite <- app_assoc. apply app_inv_head_iff.
    rewrite <- app_assoc. reflexivity.
    generalize H2. apply IHj. easy.
Qed.

(**
   This section contains lemmas and theorems related to the length of the
   prefix being odd or even in front of a squared pattern.
*)

Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> odd (length a) = true -> even (length hd) = false.
Proof.
  intros n hd a tl. intros H I.
  assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square.
  destruct a. inversion I. destruct a.
  - rewrite <- negb_true_iff. rewrite Nat.negb_even.
    generalize H. apply tm_step_consecutive_identical.
  - destruct a. inversion I. destruct a.

    assert (J: {b0 = b1} + {b0 <> b1}). apply bool_dec. destruct J.
    rewrite e in H.
    replace (hd ++ [b;b1;b1] ++ [b;b1;b1] ++ tl)
      with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
    assert (K: even (length [b]) = true). generalize H.
    apply tm_step_consecutive_identical'. inversion K.
    rewrite <- app_assoc. reflexivity.
    assert (J: {b = b0} + {b <> b0}). apply bool_dec. destruct J.
    rewrite e in H.
    replace (hd ++ [b0;b0;b1] ++ [b0;b0;b1] ++ tl)
      with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ [b1] ++ tl) in H.
    assert (K: even (length [b1]) = true). generalize H.
    apply tm_step_consecutive_identical'. inversion K.
    reflexivity.
    assert (J: {b = b1} + {b <> b1}). apply bool_dec. destruct J.
    rewrite e in H.

    assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
    apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
    assert (K: count_occ Bool.bool_dec hd true
                 = count_occ Bool.bool_dec hd false).
    generalize H1. generalize H. apply tm_step_count_occ.

    assert (L: count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) true
                  = count_occ Bool.bool_dec (hd ++ [b1;b0;b1;b1]) false).
    assert (M: even (length (hd ++ [b1;b0;b1;b1])) = true).
    rewrite app_length. rewrite Nat.even_add. rewrite H1. reflexivity.
    replace (hd ++ [b1;b0;b1] ++ [b1;b0;b1] ++ tl)
      with ((hd ++ [b1;b0;b1;b1]) ++ [b0;b1] ++ tl) in H.
    generalize M. generalize H. apply tm_step_count_occ.
    rewrite <- app_assoc. reflexivity.
    rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
    rewrite K in L. rewrite Nat.add_cancel_l in L.

    destruct b0; destruct b1; inversion L.
    rewrite <- Nat.negb_odd. rewrite H1. reflexivity.

    destruct b; destruct b0; destruct b1.
    contradiction n0. contradiction n2. contradiction n1. contradiction n2.
    contradiction n0. reflexivity.
    contradiction n0. contradiction n2. reflexivity.
    contradiction n1. reflexivity. contradiction n0. reflexivity.

    simpl in H0.
    rewrite <- Nat.succ_lt_mono in H0.
    rewrite <- Nat.succ_lt_mono in H0.
    rewrite <- Nat.succ_lt_mono in H0.
    rewrite <- Nat.succ_lt_mono in H0.
    apply Nat.nlt_0_r in H0. contradiction H0.
Qed.
 

Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> 0 < length a -> even (length (hd ++ a)) = true.
Proof.
  intros n hd a tl. intros H I.

  rewrite app_length. rewrite Nat.even_add.
  assert (J: Nat.even (length a) || Nat.odd (length a) = true).
  apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
  - rewrite H0.
    assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
    apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
    rewrite H1. reflexivity.

    (* proof that tl is not nil *)
    destruct tl. rewrite app_nil_r in H.
    assert (length (tm_step n) = length (tm_step n)). reflexivity.
    rewrite H in H2 at 2.
    assert (even (length (tm_step n)) = even (length (tm_step n))). reflexivity.
    rewrite H in H3 at 2. rewrite app_length in H3. rewrite app_length in H3.
    rewrite Nat.even_add in H3.
    rewrite Nat.even_add in H3.
    rewrite H0 in H3. symmetry in H3.
    rewrite <- Nat.negb_odd in H3. rewrite H1 in H3. simpl in H3.
    rewrite tm_size_power2 in H3. destruct n.
    assert (1 < length (hd ++ a ++ a)). rewrite app_length.
    apply Nat.lt_lt_add_l. rewrite app_length.
    rewrite <- Nat.le_succ_l in I. rewrite <- Nat.le_succ_l.
    rewrite <- Nat.add_1_r. apply Nat.add_le_mono; assumption.
    rewrite <- H2 in H4. apply Nat.lt_irrefl in H4. contradiction H4.
    rewrite Nat.pow_succ_r' in H3. rewrite Nat.even_mul in H3.
    simpl in H3. inversion H3.

    (* proof that a is not nil *)
    destruct a. inversion I.

    replace (hd ++ (b0 :: a) ++ (b0 :: a) ++ b :: tl)
      with ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl) in H.
    assert (even (length (hd ++ [b0])) = true).
    rewrite app_length. rewrite Nat.add_1_r. rewrite Nat.even_succ.
    assumption.
    assert (L: count_occ Bool.bool_dec (hd ++ [b0]) true
             = count_occ Bool.bool_dec (hd ++ [b0]) false).
    generalize H2. generalize H. apply tm_step_count_occ.

    replace ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl)
      with ((hd ++ [b0] ++ a ++ [b0] ++ a ++ [b]) ++ tl) in H.
    assert (even (length (hd ++ [b0] ++ a ++ [b0] ++ a ++ [b])) = true).
    rewrite <- app_assoc_reverse. rewrite app_length. 
    rewrite Nat.even_add. rewrite H2.
    rewrite app_length. rewrite app_length. rewrite app_length.
    rewrite Nat.add_1_r. rewrite <- Nat.add_succ_comm.
    rewrite Nat.even_add.
    destruct (even (S (length a))); reflexivity.
    assert (M: count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) true
             = count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) false).
    generalize H3. generalize H. apply tm_step_count_occ.
    rewrite app_assoc in M. rewrite count_occ_app in M.
    symmetry in M. rewrite count_occ_app in M. rewrite L in M.
    rewrite Nat.add_cancel_l in M.

    assert (forall x , x + x = 2*x).
    intro x. rewrite <- Nat.mul_1_l with (n := x).
    rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
    rewrite Nat.mul_1_l. reflexivity.
    Opaque even. simpl in H0. Transparent even.
    assert (b = b0). destruct b0; destruct b.
    + reflexivity. 
    + rewrite count_occ_app in M. rewrite count_occ_app in M.
      rewrite count_occ_app in M. rewrite count_occ_app in M.
      rewrite count_occ_app in M. rewrite count_occ_app in M.
      simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
      rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
      inversion M.
      rewrite H4 in H6. rewrite H4 in H6.
      rewrite Nat.mul_cancel_l in H6.
      apply count_occ_bool_list2 in H6.
      rewrite <- H0 in H6. rewrite Nat.even_succ in H6.
      rewrite <- Nat.negb_even in H6.
      destruct (even (length a)); inversion H6. easy.
    + rewrite count_occ_app in M. rewrite count_occ_app in M.
      rewrite count_occ_app in M. rewrite count_occ_app in M.
      rewrite count_occ_app in M. rewrite count_occ_app in M.
      simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
      rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
      inversion M.
      rewrite H4 in H6. rewrite H4 in H6.
      rewrite Nat.mul_cancel_l in H6.
      apply count_occ_bool_list2 in H6.
      rewrite <- H0 in H6. rewrite Nat.even_succ in H6.
      rewrite <- Nat.negb_even in H6.
      destruct (even (length a)); inversion H6. easy.
    + reflexivity.
    + rewrite H5 in H.



    (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
    (* TODO: la taille du facteur divise la taille du préfixe ? *)
    (* TODO : le cas de la taille 2 est un cas pair facile
       grâce à tm_step_factor4_odd_prefix *)

    Admitted.