(** * The Thue-Morse sequence (part 2)

   The following lemmas and theorems are all related to
   squares and cubes in the Thue-Morse sequence.

   Proofs in this file are long; many parts are repeated
   from copy/paste operations. Many ad-hoc lemmas could
   probably be written in a better style.

   But some powerful theorems are provided here:

   - tm_step_cubefree (there is no cube in the sequence)
   - tm_step_square_size (about length of squared factrs)
   - tm_step_square_pos (length of the prefix has the same
     parity than the length of the factor being squared)
*)  

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 related to the sequence being
   cubefree. Only the final theorem is of general interest; all other
   lemmas are defined for the very specific purpose of being used in the
   final proof.
*)

Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
Proof.
  intros n a hd tl. intro H.
  assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd.
  assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd.

  destruct H1.
  - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
  - destruct H0.
    assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
    assert (Nat.even (length hd) = true).
    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
    generalize H2. generalize H. apply tm_step_count_occ.

    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I.
    assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false).
    assert (even (length (hd++a++a)) = true).
    rewrite app_length. rewrite Nat.even_add_even.
    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.

    rewrite app_length. replace (length a) with (1*(length a)).
    rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
    rewrite <- Nat.add_0_l. apply Nat.EvenT_Even.
    apply Nat.even_EvenT.
    rewrite Nat.even_add_mul_2. reflexivity.
    apply Nat.mul_1_l.
    generalize H3. generalize I. apply tm_step_count_occ.

    rewrite count_occ_app in H3. symmetry in H3.
    rewrite count_occ_app in H3. rewrite H2 in H3.
    rewrite Nat.add_cancel_l in H3.

    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    apply app_assoc_reverse.

    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
    assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
    assert (even (length (hd++a)) = true).
    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    generalize H2. generalize I. apply tm_step_count_occ.

    assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J.
    assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false).
    assert (even (length (hd++a++a++a)) = true).
    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
    rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length.
    apply Nat.Even_Even_add.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    generalize H3. generalize J. apply tm_step_count_occ.

    replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3.
    rewrite count_occ_app in H3. symmetry in H3.
    rewrite count_occ_app in H3. rewrite H2 in H3.
    rewrite Nat.add_cancel_l in H3.

    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
    apply app_assoc_reverse.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    apply app_assoc_reverse.
    apply app_assoc_reverse.
Qed.


Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n.
Proof.
  intros n a hd tl. intros H I.
  destruct n.
  - assert (3 <= length (a ++ a ++ a)).
    rewrite app_length. rewrite app_length.
    rewrite <- Nat.le_succ_l in I.
    assert (2 <= length a + length a).
    generalize I. generalize I. apply Nat.add_le_mono.
    generalize H0. generalize I. apply Nat.add_le_mono.
    assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
    rewrite H in H1 at 2.
    assert (0 <= length hd). apply Nat.le_0_l.
    assert (0 + 3 <= length hd + length (a ++ a ++ a)).
    generalize H0. generalize H2. apply Nat.add_le_mono.
    simpl in H3. rewrite <- app_length in H3.
    assert (0 <= length tl). apply Nat.le_0_l.
    assert (3 + 0 <= length (hd ++ a ++ a ++ a) + length (tl)).
    generalize H4. generalize H3. apply Nat.add_le_mono.
    rewrite <- app_length in H5. rewrite Nat.add_0_r in H5.
    replace ((hd++a++a++a)++tl) with (hd++a++a++a++tl) in H5.
    rewrite <- H1 in H5. simpl in H5. apply le_S_n in H5.
    apply Nat.nle_succ_0 in H5. contradiction H5.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.
  - apply Nat.lt_0_succ.
Qed.


Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> even (length hd) = even (length tl).
Proof.
  intros n a hd tl. intros H J.
  assert (K : 0 < n). generalize J. generalize H. apply tm_step_cube2.
  destruct n.
  - apply Nat.lt_irrefl in K. contradiction K.
  - assert (Nat.Even (length (tm_step (S n)))).
    rewrite tm_size_power2. rewrite Nat.pow_succ_r'.
    apply Nat.Even_mul_l. apply Nat.EvenT_Even.
    apply Nat.EvenT_2. apply Nat.EvenT_0.
    rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
    rewrite Nat.add_shuffle3 in H0.
    assert (I := H). apply tm_step_cube1 in I.
    apply Nat.even_EvenT in I. apply Nat.EvenT_Even in I.
    assert (Nat.Even (length hd + length (a ++ a ++ tl))).
    generalize I. generalize H0. apply Nat.Even_add_Even_inv_r.
    rewrite app_length in H1. rewrite Nat.add_shuffle3 in H1.
    assert (Nat.Even (length hd + length (a ++ tl))).
    generalize I. generalize H1. apply Nat.Even_add_Even_inv_r.
    rewrite app_length in H2. rewrite Nat.add_shuffle3 in H2.
    assert (Nat.Even (length hd + length tl)).
    generalize I. generalize H2. apply Nat.Even_add_Even_inv_r.

    apply Nat.Even_EvenT in H3. apply Nat.EvenT_even in H3.
    rewrite Nat.even_add in H3.
    destruct (even (length hd)); destruct (even (length tl)).
    reflexivity. simpl in H3. inversion H3.
    simpl in H3. inversion H3. reflexivity.
Qed.


Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false
  -> 0 < length a
  -> hd_error a = hd_error tl.
Proof.
  intros n a hd tl. intros H I J.
  assert (even (length hd) = even (length tl)).
  generalize J. generalize H. apply tm_step_cube3.
  assert (even (length a) = true). generalize H. apply tm_step_cube1.
  rewrite I in H0.
  destruct a.
  - simpl in J. apply Nat.lt_irrefl in J. contradiction J.
  - destruct tl. simpl in H0. inversion H0.
    simpl. replace (b::a) with ((b::nil) ++ a) in H.
    replace (hd ++ ([b] ++ a) ++ ([b] ++ a) ++ ([b] ++ a) ++ (b0::tl))
    with ((hd ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b0::nil)) ++ tl) in H.

    assert (even (length (hd ++ (b::nil))) = true).
    rewrite last_length.
    rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite I. reflexivity.

    assert (count_occ Bool.bool_dec (hd ++ (b::nil)) true
        = count_occ Bool.bool_dec (hd ++ (b::nil)) false).
    generalize H2. generalize H. apply tm_step_count_occ.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)))) = true).
    rewrite app_length. rewrite Nat.even_add. rewrite H2.
    rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
    reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) true
            = count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) false).
    generalize H4. rewrite app_assoc in H. generalize H. apply tm_step_count_occ.

    assert (K := H5).
    rewrite count_occ_app in H5. symmetry in H5. rewrite count_occ_app in H5.
    rewrite H3 in H5. rewrite Nat.add_cancel_l in H5.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil))  ++ (a++ (b::nil)))) = true).
    rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
    rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
    reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) true
    = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) false).
    generalize H6.
    rewrite app_assoc in H. rewrite app_assoc in H.
    replace (((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b])
      with ((hd ++ [b]) ++ (a ++ [b]) ++ a ++ [b]) in H.
    generalize H. apply tm_step_count_occ.

    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil))  ++ (a++ (b::nil)) ++ (a++ (b0::nil)))) = true).
    rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
    rewrite app_length. rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite Nat.even_add. rewrite H1.
    rewrite last_length. rewrite H1. reflexivity. reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) true
    = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) false).
    generalize H8.

    rewrite app_assoc in H. rewrite app_assoc in H. rewrite app_assoc in H.
    replace ((((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) ++ a ++ [b0])
    with ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) in H.
    generalize H. apply tm_step_count_occ.

    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.

    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H3 in H9. rewrite Nat.add_cancel_l in H9.
    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.

    destruct b; destruct b0.
    + reflexivity.
    + rewrite count_occ_app in H9. rewrite count_occ_app in H9.
      rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
      rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
      rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
      rewrite count_occ_app in H5. rewrite count_occ_app in H5.
      rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
      rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
      rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
      rewrite H5 in H9.
      rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
      rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
      rewrite Nat.add_cancel_l in H9. inversion H9.
      reflexivity. easy. easy. reflexivity.
    + rewrite count_occ_app in H9. rewrite count_occ_app in H9.
      rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
      rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
      rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
      rewrite count_occ_app in H5. rewrite count_occ_app in H5.
      rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
      rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
      rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
      rewrite <- H5 in H9.
      rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
      rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
      rewrite Nat.add_cancel_l in H9. inversion H9.
      easy. reflexivity. reflexivity. easy.
    + reflexivity.
    + rewrite app_assoc_reverse. apply app_inv_head_iff.
      rewrite app_assoc_reverse. rewrite app_assoc_reverse.
      rewrite app_assoc_reverse. rewrite app_assoc_reverse.
      apply app_inv_head_iff. apply app_inv_head_iff.
      rewrite app_assoc_reverse.
      apply app_inv_head_iff. apply app_inv_head_iff.
      rewrite app_assoc_reverse.
      reflexivity.
    + reflexivity.
Qed.


Lemma tm_step_cube5 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
                         /\ length a = length b
                         /\ even (length hd2) = true.
Proof.
  intros n a hd tl. intros H I.
  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
  apply Nat.Even_or_Odd.
  destruct J.
  - exists hd. exists a. exists tl.
    split. assumption. split. reflexivity.
    apply Nat.Even_EvenT in H0.
    apply Nat.EvenT_even in H0. assumption.
  - apply Nat.Odd_OddT in H0.
    apply Nat.OddT_odd in H0.
    rewrite <- Nat.negb_even in H0. rewrite negb_true_iff in H0.
    destruct a.
    + simpl in I. apply Nat.lt_irrefl in I. contradiction I.
    + assert (Nat.even (length hd) = Nat.even (length tl)).
      generalize I. generalize H. apply tm_step_cube3.
      rewrite H0 in H1.
      destruct tl.
      * simpl in H1. inversion H1.
      * assert (hd_error (b::a) = hd_error (b0::tl)).
        generalize I. generalize H0. generalize H. apply tm_step_cube4.
        simpl in H2. inversion H2. rewrite <- H4 in H.
        exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl.
        split. rewrite H.
        rewrite app_assoc_reverse. apply app_inv_head_iff.
        replace (b::a) with ([b] ++ a).
        rewrite app_assoc_reverse. apply app_inv_head_iff.
        rewrite app_assoc_reverse. rewrite app_assoc_reverse.
        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
        rewrite app_assoc_reverse. reflexivity.
        reflexivity.
        split. rewrite last_length. reflexivity.
        rewrite last_length.
        rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite H0.
        reflexivity.
Qed.


Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> exists (hd2 b tl2 : list bool),
       tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b.
Proof.
  intros n a hd tl. intros H I.
  assert(J: exists (hd2 b tl2 : list bool),
              tm_step n = hd2 ++ b ++ b ++ b ++ tl2
                /\ length a = length b /\ even (length hd2) = true).
  generalize I. generalize H. apply tm_step_cube5.
  destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2].
  destruct J2 as [J3 J4]. destruct J4 as [J5 J6].
  assert (J: even (length b) = true). generalize J3. apply tm_step_cube1.
  
  assert (K: 0 < n). generalize I. generalize H. apply tm_step_cube2.
  destruct n.
  - apply Nat.lt_irrefl in K. contradiction K.
  - rewrite <- tm_step_lemma in J3.
    assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))).
    generalize J6. generalize J3. apply tm_morphism_app2.
    assert (M: b ++ b ++ b ++ tl2
                 = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))).
    generalize J6. generalize J3. apply tm_morphism_app3.
    assert (N: b = tm_morphism (firstn (Nat.div2 (length b))
                                       (skipn (Nat.div2 (length hd2))
                                              (tm_step n)))).
    generalize J. symmetry in M. generalize M. apply tm_morphism_app2.
    assert (even (length (b++b++b)) = true).
    rewrite app_length. rewrite app_length.
    rewrite Nat.even_add_even. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT.
    rewrite Nat.even_add_even. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b)))
                                        (skipn (Nat.div2 (length hd2))
                                               (tm_step n)))).
    generalize H0. symmetry in M. generalize M.
    replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3.
    rewrite app_assoc_reverse. apply app_inv_head_iff.
    apply app_assoc_reverse.
    assert (hd2 ++ b ++ b ++ b ++ tl2
      = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n)))
      ++ (tm_morphism (firstn (Nat.div2 (length b))
                              (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (firstn (Nat.div2 (length b))
                              (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (firstn (Nat.div2 (length b))
                              (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b)))
                             (skipn (Nat.div2 (length hd2)) (tm_step n))))).
   rewrite <- L. rewrite <- N. rewrite <- O. reflexivity.
   rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
   rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
   rewrite <- J3 in H1.

   rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1.
   exists (firstn (Nat.div2 (length hd2)) (tm_step n)).
   exists (firstn (Nat.div2 (length b))
                  (skipn (Nat.div2 (length hd2)) (tm_step n))).
   exists (skipn (Nat.div2 (length (b ++ b ++ b)))
                 (skipn (Nat.div2 (length hd2)) (tm_step n))).
   split. assumption.

   assert (2 <= length b). destruct b. simpl in J5. rewrite J5 in I.
   apply Nat.lt_irrefl in I. contradiction I.
   destruct b0. simpl in J. inversion J. simpl. rewrite <- Nat.succ_le_mono.
   rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.

   assert (length (b++b++b++tl2)
             = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
   rewrite M. apply tm_morphism_length.

   assert (2 <= length (b++b++b++tl2)).
   rewrite app_length. rewrite <- Nat.add_0_r at 1.
   apply Nat.add_le_mono. assumption. apply Nat.le_0_l.
   rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1.
   rewrite <- Nat.mul_le_mono_pos_l in H4.
    
   rewrite firstn_length. rewrite <- Nat.le_succ_l.
   assert (1 <= Nat.div2 (length b)).
   rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r.
   replace (2 * Nat.div2 (length b))
     with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))).
   rewrite <- Nat.div2_odd. assumption.
   rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
   apply Nat.lt_0_2.
   generalize H4. generalize H5. apply Nat.min_glb.
   apply Nat.lt_0_2.
Qed.


Lemma tm_step_cube7 : forall (n : nat),
     (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
     /\ 0 < length a)
  -> exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2
     /\ 0 < length b.
Proof.
  intros n. intro H.
  induction n; destruct H; destruct H; destruct H; destruct H.
  - exists x. exists x0. exists x1. split; assumption.
  - assert (J: exists (hd2 b2 tl2 : list bool),
      tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2
      /\ 0 < length b2).
    generalize H0. generalize H. apply tm_step_cube6.
    rewrite Nat.pred_succ in J. apply IHn. apply J.
Qed.


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

  assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
  destruct J.
  - rewrite <- e in H.
    assert (J: exists (hd a tl : list bool),
      tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
    exists hd. exists a. exists tl. split; assumption.
    apply tm_step_cube7 in J. destruct J. destruct H0. destruct H0. destruct H0.
    assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2.
    apply Nat.lt_irrefl in H2. contradiction H2.
  - assumption.
Qed.

(**
   The following lemma is required for the following parts f the file.
*)

Lemma 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.


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

  (* proof that tl is not nil *)
  assert (W: nil <> tl).
  assert (even (length (a++a)) = true). rewrite app_length.
  rewrite Nat.even_add. rewrite K. reflexivity.
  assert (0 < length (a ++ a)). rewrite <- Nat.add_0_r at 1.
  rewrite app_length. apply Nat.add_lt_mono; assumption.
  generalize H0. generalize J. generalize H1.
  replace (hd++a++a++tl) with (hd++(a++a)++tl) in H. generalize H.
  apply tm_step_tail_not_nil_prefix_odd. rewrite <- app_assoc. reflexivity.
  destruct tl. contradiction W. reflexivity.

  (* 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 H0. 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 H0.
  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 H1. 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 K. 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 H2 in H4. rewrite H2 in H4.
    rewrite Nat.mul_cancel_l in H4.
    apply count_occ_bool_list2 in H4.
    rewrite <- K in H4. rewrite Nat.even_succ in H4.
    rewrite <- Nat.negb_even in H4.
    destruct (even (length a)); inversion H4. 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 H2 in H4. rewrite H2 in H4.
    rewrite Nat.mul_cancel_l in H4.
    apply count_occ_bool_list2 in H4.
    rewrite <- K in H4. rewrite Nat.even_succ in H4.
    rewrite <- Nat.negb_even in H4.
    destruct (even (length a)); inversion H4. easy.
  - reflexivity.
  - rewrite H3 in H.
    exists (hd ++ [b0]). exists (a ++ [b0]). exists tl.
    split. rewrite H. rewrite <- app_assoc. rewrite <- app_assoc.
    rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
    rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
    split. apply last_length. apply last_length.
  - rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
    rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
    reflexivity.
  - rewrite <- app_assoc. reflexivity.
Qed.


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

  assert (L: hd = removelast hd ++ last hd false :: nil).
  apply app_removelast_last. destruct hd. inversion J. easy.
  rewrite L in H.

  assert (M: a = removelast a ++ last a false :: nil).
  apply app_removelast_last. destruct a. inversion I. easy.
  rewrite M in H.

  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
  rewrite <- app_assoc in H.

  assert (U: even (length (removelast hd)) = true).
  rewrite L in J. rewrite app_length in J.
  rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
  assumption.

  assert (N: count_occ Bool.bool_dec (removelast hd) true
           = count_occ Bool.bool_dec (removelast hd) false).
  generalize U. generalize H. apply tm_step_count_occ.

  rewrite app_assoc in H. rewrite app_assoc in H.
  assert (V: even (length ((removelast hd ++ [last hd false])
                               ++ removelast a)) = true).
  rewrite app_length. rewrite <- L. rewrite Nat.even_add.
  rewrite <- Nat.negb_odd. rewrite J. rewrite M in K.
  rewrite app_length in K. rewrite Nat.add_1_r in K.
  rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd.
  rewrite K. reflexivity.

  assert (O: count_occ Bool.bool_dec
       ((removelast hd ++ [last hd false]) ++ removelast a) true
           = count_occ Bool.bool_dec
       ((removelast hd ++ [last hd false]) ++ removelast a) false).
  generalize V. generalize H. apply tm_step_count_occ.

  replace ((removelast hd ++ [last hd false]) ++ removelast a)
    with (removelast hd ++ ([last hd false] ++ removelast a)) in O.
  rewrite count_occ_app in O. symmetry in O. rewrite count_occ_app in O.
  rewrite N in O. rewrite Nat.add_cancel_l in O.

  rewrite app_assoc in H. rewrite app_assoc in H.
  assert (W: even (length ((((removelast hd ++ [last hd false])
                               ++ removelast a) ++ [last a false])
                               ++ removelast a)) = true).
  rewrite app_length. rewrite app_length. rewrite Nat.even_add.
  rewrite Nat.even_add. rewrite V.
  assert (even (length (removelast a)) = false).
  rewrite M in K. rewrite app_length in K. rewrite Nat.add_1_r in K.
  rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd. rewrite K.
  reflexivity. rewrite H0. reflexivity.

  assert (P: count_occ Bool.bool_dec
       ((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) true
           = count_occ Bool.bool_dec
       ((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) false).
  generalize W. generalize H. apply tm_step_count_occ.

  rewrite <- app_assoc in P. rewrite <- app_assoc in P.
  rewrite <- app_assoc in P.
  rewrite count_occ_app in P. symmetry in P. rewrite count_occ_app in P.
  rewrite N in P. rewrite Nat.add_cancel_l in P.
  rewrite app_assoc in P. rewrite count_occ_app in P. symmetry in P.
  rewrite count_occ_app in P. rewrite O in P. rewrite Nat.add_cancel_l in P.

  assert (last hd false = last a false).
  destruct (last hd false); destruct (last a false).
  reflexivity.
  simpl in O. simpl in P. rewrite O in P.
  rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
  rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
  inversion P.
  simpl in O. simpl in P. rewrite <- O in P. symmetry in P.
  rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
  rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
  inversion P.
  reflexivity.

  rewrite H0 in H.
  exists (removelast hd). exists ([last a false] ++ removelast a).
  exists ([last a false] ++ tl).
  split. rewrite H.
  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
  reflexivity.
  split.

  assert (X: length hd = length hd). reflexivity.
  rewrite app_removelast_last with (l := hd) (d := false) in X at 2.
  rewrite app_length in X. rewrite Nat.add_1_r in X.
  rewrite <- Nat.succ_pred_pos with (n := length hd) in X.
  apply Nat.succ_inj. rewrite X. reflexivity.

  destruct (length hd). inversion J. apply Nat.lt_0_succ.
  destruct hd. inversion J. easy.
  rewrite app_length. rewrite Nat.add_comm. rewrite <- app_length.
  rewrite <- M. reflexivity.
  rewrite <- app_assoc. reflexivity.
Qed.


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

  assert (L: exists (hd' a' tl' : list bool),
     tm_step n = hd' ++ a' ++ a' ++ tl'
     /\ length hd' = S (length hd) /\ length a' = length a).
  generalize K. generalize J. generalize I. generalize H.
  apply tm_step_square_pos_even.

  assert (M: exists (hd' a' tl' : list bool),
     tm_step n = hd' ++ a' ++ a' ++ tl'
     /\ length hd' = Nat.pred (length hd) /\ length a' = length a).
  generalize K. generalize J. generalize I. generalize H.
  apply tm_step_square_pos_even'.

  destruct L as [hd' L2]. destruct L2 as [a' L3]. destruct L3 as [tl' L].
  destruct M as [hd'' M2]. destruct M2 as [a'' M3]. destruct M3 as [tl'' M].
  destruct L as [L1 L2]. destruct L2 as [L2 L3].
  destruct M as [M1 M2]. destruct M2 as [M2 M3].
  assert (L0 := L1). assert (M0 := M1).

  assert (N: 0 < n).
  generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even.
  destruct n. inversion N.

  assert (L4: even (length hd') = true). rewrite L2. rewrite Nat.even_succ.
  assumption.
  assert (M4: even (length hd'') = true). rewrite M2. rewrite Nat.even_pred.
  assumption. destruct hd. inversion J. easy.

  rewrite <- tm_step_lemma in L1.
  assert (L5: hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))).
  generalize L4. generalize L1. apply tm_morphism_app2.

  rewrite <- tm_step_lemma in M1.
  assert (M5: hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
  generalize M4. generalize M1. apply tm_morphism_app2.
  
  assert (L6: a' ++ a' ++ tl'
      = tm_morphism (skipn (Nat.div2 (length hd')) (tm_step n))).
  generalize L4. generalize L1. apply tm_morphism_app3.
  
  assert (M6: a'' ++ a'' ++ tl''
      = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
  generalize M4. generalize M1. apply tm_morphism_app3.

  assert (L7: even (length a') = true). rewrite L3. assumption.
  assert (L8: a' = tm_morphism (firstn (Nat.div2 (length a'))
         (skipn (Nat.div2 (length hd')) (tm_step n)))).
  generalize L7. symmetry in L6. generalize L6. apply tm_morphism_app2.

  assert (M7: even (length a'') = true). rewrite M3. assumption.
  assert (M8: a'' = tm_morphism (firstn (Nat.div2 (length a''))
         (skipn (Nat.div2 (length hd'')) (tm_step n)))).
  generalize M7. symmetry in M6. generalize M6. apply tm_morphism_app2.

  rewrite app_assoc in L6. symmetry in L6.
  rewrite app_assoc in M6. symmetry in M6.

  assert (L9: even (length (a' ++ a')) = true). rewrite app_length.
  rewrite Nat.even_add. rewrite L7. reflexivity.

  assert (M9: even (length (a'' ++ a'')) = true). rewrite app_length.
  rewrite Nat.even_add. rewrite M7. reflexivity.

  assert (L10: tl' = tm_morphism (skipn (Nat.div2 (length (a' ++ a')))
       (skipn (Nat.div2 (length hd')) (tm_step n)))).
  generalize L9. generalize L6. apply tm_morphism_app3.

  assert (M10: tl'' = tm_morphism (skipn (Nat.div2 (length (a'' ++ a'')))
       (skipn (Nat.div2 (length hd'')) (tm_step n)))).
  generalize M9. generalize M6. apply tm_morphism_app3.

  rewrite L5 in L1. rewrite L8 in L1. rewrite L10 in L1.
  rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_app in L1.
  rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_eq in L1.

  rewrite M5 in M1. rewrite M8 in M1. rewrite M10 in M1.
  rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_app in M1.
  rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_eq in M1.

  (* now we easily discard the case where a'0 would be odd since we
     can freely choose either L1 or M1 to find an even prefix *)
  assert (Nat.Even (Nat.div2 (length a)) \/ Nat.Odd (Nat.div2 (length a))).
  apply Nat.Even_or_Odd. destruct H0 as [Z | Z].
  - (* first case, a'0 is even and we are looking for an odd prefix *)
    assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
    apply Nat.Even_or_Odd. destruct H0.

    + (* case Nat.div2 (length hd'') has an odd length *)
      exists (firstn (Nat.div2 (length hd'')) (tm_step n)).
      exists (firstn (Nat.div2 (length a''))
               (skipn (Nat.div2 (length hd'')) (tm_step n))).
      exists (skipn (Nat.div2 (length (a'' ++ a'')))
               (skipn (Nat.div2 (length hd'')) (tm_step n))).
      split. rewrite <- pred_Sn. rewrite M1 at 1. reflexivity.

      assert (Nat.div2 (length hd'') <= length (tm_step n)).
      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
      rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
      rewrite <- tm_size_power2. rewrite M0.
      rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
      apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
      assumption. apply Nat.lt_0_2.

      split.

      rewrite firstn_length_le.
      rewrite Nat.mul_lt_mono_pos_l with (p := 2).
      rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite M3. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2.
      rewrite skipn_length.
      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.

      split. 
      rewrite firstn_length_le.
      apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
      apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
      rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
      apply Nat.Even_succ in H0. apply Nat.Odd_OddT in H0.
      apply Nat.OddT_odd in H0. apply H0.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
      assumption.
      destruct (length hd). inversion J. apply Nat.lt_0_succ.

      assumption.

      rewrite firstn_length_le.
      rewrite M3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
      assumption. rewrite skipn_length.
      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.

    + (* case Nat.div2 (length hd') has an odd length *)
      exists (firstn (Nat.div2 (length hd')) (tm_step n)).
      exists (firstn (Nat.div2 (length a'))
               (skipn (Nat.div2 (length hd')) (tm_step n))).
      exists (skipn (Nat.div2 (length (a' ++ a')))
               (skipn (Nat.div2 (length hd')) (tm_step n))).
      split. rewrite <- pred_Sn. rewrite L1 at 1. reflexivity.

      assert (Nat.div2 (length hd') <= length (tm_step n)).
      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
      rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
      rewrite <- tm_size_power2. rewrite L0.
      rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
      apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
      assumption. apply Nat.lt_0_2.

      split.

      rewrite firstn_length_le.
      rewrite Nat.mul_lt_mono_pos_l with (p := 2).
      rewrite Nat.mul_0_r. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite L3. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2.
      rewrite skipn_length.
      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.

      split.

      rewrite firstn_length_le.
      apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
      assumption.

      rewrite firstn_length_le.
      rewrite L3. apply Nat.EvenT_even. apply Nat.Even_EvenT.
      assumption. rewrite skipn_length.
      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.
  - (* second case, a'0 is odd and we are looking for an even prefix *)
    assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))).
    apply Nat.Even_or_Odd. destruct H0.
    + assert (Nat.div2 (length hd') <= length (tm_step n)).
      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
      rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
      rewrite <- tm_size_power2. rewrite L0.
      rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
      apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
      assumption. apply Nat.lt_0_2.

      assert (even (length (firstn (Nat.div2 (length hd')) (tm_step n))) = false).
      assert (odd (length (firstn (Nat.div2 (length a'))
             (skipn (Nat.div2 (length hd')) (tm_step n)))) = true).
      rewrite firstn_length_le. rewrite L3.
      apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
      rewrite skipn_length.

      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.
      generalize H2. generalize L1. apply tm_step_odd_prefix_square.

      rewrite firstn_length_le in H2.
      apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
      rewrite H0 in H2. inversion H2. assumption.
    + assert (Nat.div2 (length hd'') <= length (tm_step n)).
      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
      rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'.
      rewrite <- tm_size_power2. rewrite M0.
      rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity.
      apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT.
      assumption. apply Nat.lt_0_2.

      assert (even (length (firstn (Nat.div2 (length hd'')) (tm_step n))) = false).
      assert (odd (length (firstn (Nat.div2 (length a''))
             (skipn (Nat.div2 (length hd'')) (tm_step n)))) = true).
      rewrite firstn_length_le. rewrite M3.
      apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption.
      rewrite skipn_length.

      rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')).
      rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
      rewrite Nat.sub_diag. rewrite Nat.add_0_l.

      rewrite Nat.mul_le_mono_pos_l with (p := 2).
      rewrite tm_size_power2. rewrite Nat.mul_add_distr_l.
      rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
      rewrite <- Nat.Even_double. rewrite <- Nat.Even_double.
      rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0.
      rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1.
      apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl.
      reflexivity.
      apply le_0_n.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity.
      assumption.
      generalize H2. generalize M1. apply tm_step_odd_prefix_square.

      rewrite firstn_length_le in H2.

      apply eq_S in M2. rewrite Nat.succ_pred_pos in M2.
      apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0.
      rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0.
      apply Nat.Even_succ in H0. rewrite Nat.Even_succ_succ in H0.
      apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0.
      rewrite H0 in H2. inversion H2.

      apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
      apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ.
      assumption.
      destruct (length hd). inversion J. apply Nat.lt_0_succ.

      assumption.
Qed.

Lemma tm_step_square_pos_even''' : forall (n : nat),
  (exists (hd a tl : list bool),
      tm_step n = hd ++ a ++ a ++ tl /\ 0 < length a
        /\ odd (length hd) = true /\ even (length a) = true)
    -> (exists (hd' a' tl' : list bool),
      tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
        /\ odd (length hd') = true /\ even (length a') = true).
Proof.
  intro n. intro.
  induction n.
  - destruct H. destruct H. destruct H.
    exists x. exists x0. exists x1. assumption.
  - assert (exists hd' a' tl' : list bool,
         tm_step (Nat.pred (S n)) = hd' ++ a' ++ a' ++ tl' /\
         0 < length a' /\
         odd (length hd') = true /\ even (length a') = true).
    destruct H. destruct H. destruct H.
    destruct H. destruct H0. destruct H1.
    generalize H2. generalize H1. generalize H0. generalize H.
    apply tm_step_square_pos_even''. rewrite <- pred_Sn in H0.
    apply IHn in H0. assumption.
Qed.

Theorem tm_step_square_pos : 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.
  assert (J: Nat.even (length a) || Nat.odd (length a) = true).
  apply Nat.orb_even_odd. apply orb_prop in J.
  assert (K: Nat.even (length hd) || Nat.odd (length hd) = true).
  apply Nat.orb_even_odd. apply orb_prop in K.
  destruct J; destruct K.
  - rewrite app_length. rewrite Nat.even_add. rewrite H0. rewrite H1.
    reflexivity.
  - assert (exists (hd' a' tl' : list bool),
      tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
        /\ odd (length hd') = true /\ even (length a') = true).
    assert (exists (hd' a' tl' : list bool),
      tm_step n = hd' ++ a' ++ a' ++ tl' /\ 0 < length a'
        /\ odd (length hd') = true /\ even (length a') = true).
    exists hd. exists a. exists tl. split. assumption.
    split. assumption. split. assumption. assumption.
    generalize H2. apply tm_step_square_pos_even'''.
    destruct H2. destruct H2. destruct H2.
    destruct H2. destruct H3. destruct H4.

    assert (0 < 0). generalize H5. generalize H3. generalize H2.
    apply tm_step_not_nil_factor_even. inversion H6.
  - assert (even (length hd) = false).
    generalize H0. generalize H. apply tm_step_odd_prefix_square.
    rewrite H1 in H2. inversion H2.
  - rewrite app_length. rewrite Nat.even_add.
    rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd.
    rewrite H0. rewrite H1. reflexivity.
Qed.


Lemma tm_step_square_prefix_not_nil0 :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl -> 0 < length a
  -> hd <> nil
    \/ exists a' tl', tm_step (pred n) = a' ++ a' ++ tl'
       /\ 0 < length a'.
Proof.
  intros n hd a tl. intros H I.
  destruct a. inversion I.

  destruct a.
  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
  destruct W. rewrite e in H.
  assert (1 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (Z : 0 < 2^n). apply Nat.lt_succ_l. assumption.
  assert (nth_error (tm_step n) 0 <> nth_error (tm_step (S n)) (S (2*0))).
  generalize Z. apply tm_step_succ_double_index.
  rewrite tm_step_stable with (k := S (2*0)) (m := n) in H1. rewrite H in H1.
  simpl in H1. contradiction H1. reflexivity. rewrite Nat.pow_succ_r.
  replace (S (2*0)) with (1*1). apply Nat.mul_lt_mono. apply Nat.lt_1_2.
  assumption. reflexivity. apply le_0_n. assumption. left. assumption.

  destruct a.
  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
  destruct W. rewrite e in H.
  assert (2 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (nth_error (tm_step n) 1 = nth_error (tm_step (S n)) (2*1)).
  apply tm_step_double_index.
  rewrite tm_step_stable with (k := (2*1)) (m := n) in H1. rewrite H in H1.
  simpl in H1. inversion H1. rewrite H3 in H.
  replace ([] ++ [b;b] ++ [b;b] ++ tl)
    with ([b] ++ [b] ++ [b] ++ [b] ++ tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_1. reflexivity. rewrite Nat.pow_succ_r.
  apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_succ.
  apply Nat.lt_succ_l. assumption. apply le_0_n. assumption.
  left. assumption.

  destruct a.
  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
  destruct W. rewrite e in H.
  assert (5 < 2^n). rewrite <- tm_size_power2. rewrite H. simpl.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (nth_error (tm_step n) 2 <> nth_error (tm_step (S n)) (S (2*2))).
  apply tm_step_succ_double_index.
  apply Nat.lt_succ_l. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption.
  rewrite tm_step_stable with (k := S (2*2)) (m := n) in H1. rewrite H in H1.
  simpl in H1. contradiction H1. reflexivity. rewrite Nat.pow_succ_r.
  apply Nat.lt_succ_l. replace (S (S (2*2))) with (2*3).
  apply Nat.mul_lt_mono_pos_l. apply Nat.lt_0_2.
  apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. reflexivity.
  apply le_0_n. assumption. left. assumption.

  pose (a' := b::b0::b1::b2::a). fold a' in H.
  assert (J : 4 <= length a'). unfold a'. simpl.
  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply le_0_n.

  assert (K: {odd (length a') = true} + {~ odd (length a') = true}).
  apply bool_dec. destruct K.
  assert (length a' < 4). generalize e. generalize H.
  apply tm_step_odd_square.
  apply Nat.le_ngt in J. apply J in H0. contradiction H0.
  apply not_true_iff_false in n0.
  assert (K: even (length a') = true).
  rewrite <- Nat.negb_odd. rewrite n0. reflexivity.

  (*
  assert (L: even (length (hd ++ a')) = true).
  rewrite Nat.le_succ_l in J. apply Nat.lt_succ_l in J.
  apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
  generalize J. generalize H. apply tm_step_square_pos.

  assert (M: even (length hd) = true).
  rewrite app_length in L. rewrite Nat.even_add_even in L.
  assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  *)

  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
  destruct W. rewrite e in H. right.
  destruct n. inversion H. rewrite app_nil_l in H.

  assert (N: tm_morphism (tm_step n) = tm_morphism
           (firstn (Nat.div2 (length a')) (tm_step n) ++
            firstn (Nat.div2 (length a'))
              (skipn (Nat.div2 (length a')) (tm_step n)) ++
            skipn (Nat.div2 (length a' + length a')) (tm_step n))).
  generalize K. generalize K. generalize H. apply tm_step_morphism3.
  assert (O := N). rewrite tm_step_lemma in N.
  rewrite tm_morphism_app in N. rewrite tm_morphism_app in N.

  assert (length a' + length a' <= 2 * length (tm_step n)).
  rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
  rewrite <- tm_size_power2. rewrite H. rewrite app_assoc.
  rewrite app_length. rewrite <- app_length. apply Nat.le_add_r.
  apply le_0_n. replace (length a' + length a') with (2 * length a') in H0.
  rewrite <- Nat.mul_le_mono_pos_l in H0.

  assert (length a' = length
       (tm_morphism (firstn (Nat.div2 (length a')) (tm_step n)))).
  rewrite tm_morphism_length. rewrite firstn_length_le.
  rewrite <- Nat.add_0_r. replace 0 with (Nat.b2n (Nat.odd (length a'))) at 2.
  rewrite <- Nat.div2_odd. reflexivity. rewrite n0. reflexivity.
  assert (Nat.div2 (length a') < length a').
  apply Nat.lt_div2. apply Nat.lt_succ_l in J.
  apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J. assumption.

  apply Nat.lt_le_incl. generalize H0. generalize H1.
  apply Nat.lt_le_trans.

  assert (Nat.div2 (length a') < length a'). apply Nat.lt_div2.
  apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
  apply Nat.lt_succ_l in J. assumption.

  assert (length a' = length
    (tm_morphism (firstn (Nat.div2 (length a'))
                 (skipn (Nat.div2 (length a')) (tm_step n))))).
  rewrite tm_morphism_length. rewrite firstn_length_le.
  rewrite <- Nat.add_0_r. replace 0 with (Nat.b2n (Nat.odd (length a'))) at 2.
  rewrite <- Nat.div2_odd. reflexivity. rewrite n0. reflexivity.
  rewrite skipn_length.

  rewrite Nat.add_le_mono_r with (p := Nat.div2 (length a')).
  rewrite Nat.sub_add. rewrite Nat.div2_div at 2. rewrite <- Nat.div_add_l.
  rewrite Nat.mul_comm.
  replace (2 * Nat.div2 (length a'))
    with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))).
  rewrite <- Nat.div2_odd. replace (length a' + length a') with (2 * length a').
  replace 2 with (2*1) at 2. rewrite Nat.div_mul_cancel_l.
  rewrite Nat.div_1_r. assumption. easy. easy. reflexivity.
  simpl. rewrite Nat.add_0_r. reflexivity. rewrite n0.
  simpl. rewrite Nat.add_0_r. reflexivity. easy.

  apply Nat.lt_le_incl. generalize H0. generalize H2.
  apply Nat.lt_le_trans.

  assert (a' = tm_morphism (firstn (Nat.div2 (length a')) (tm_step n))).
  generalize H1. rewrite H in N. generalize N. apply app_eq_length_head.
  rewrite <- H4 in N. rewrite H in N. rewrite app_inv_head_iff in N.

  assert (a' = 
    tm_morphism
      (firstn (Nat.div2 (length a'))
         (skipn (Nat.div2 (length a')) (tm_step n)))).
  generalize H3. generalize N. apply app_eq_length_head.

  exists (firstn (Nat.div2 (length a')) (tm_step n)).
  exists (skipn (Nat.div2 (length a' + length a')) (tm_step n)).
  split.
  rewrite tm_morphism_app in O.
  rewrite tm_morphism_app in O.
  rewrite <- H5 in O. rewrite H4 in O at 2.
  rewrite <- tm_morphism_app in O.
  rewrite <- tm_morphism_app in O.
  rewrite <- tm_morphism_eq in O. rewrite <- pred_Sn.
  rewrite O at 1. reflexivity.
  rewrite firstn_length_le.
  apply Nat.div_le_mono with (c := 2) in J.
  rewrite Nat.div2_div. replace (4/2) with 2 in J.
  apply Nat.lt_succ_l in J. assumption. reflexivity. easy.
  apply Nat.lt_le_incl. generalize H0. generalize H2.
  apply Nat.lt_le_trans. apply Nat.lt_0_2.
  simpl. rewrite Nat.add_0_r. reflexivity.
  left. assumption.
Qed.