Require Import thue_morse.

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

Import ListNotations.


(**
   The following lemma, while not of truly general use, is
    used in several proofs and has therefore its own dedicated
   section here.
*)

Lemma tm_step_consecutive_identical :
  forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
  tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
  -> even (length a) = true.
Proof.
  intros n hd a tl b1 b2. intros H.
  assert (I: even (length hd) = false).
  assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
  apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
  assert (K: count_occ Bool.bool_dec hd true
           = count_occ Bool.bool_dec hd false).
  generalize n0. generalize H. apply tm_step_count_occ.
  rewrite app_assoc in H.
  assert (L: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
           = count_occ Bool.bool_dec (hd ++ [b1;b1]) false).
  assert (even (length (hd ++ [b1;b1])) = true).
  rewrite app_length. rewrite Nat.even_add_even. assumption.
  simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
  generalize H0. generalize H. apply tm_step_count_occ.
  rewrite count_occ_app in L. rewrite count_occ_app in L.
  rewrite K in L. rewrite Nat.add_cancel_l in L.
  destruct b1. simpl in L. inversion L. simpl in L. inversion L.

  assert (J: {even (length (hd ++ [b1;b1] ++ a))
            = false} + { ~ (even (length (hd ++ [b1;b1] ++ a))) = false}).
  apply bool_dec. destruct J.

  rewrite app_length in e. rewrite app_length in e.
  rewrite Nat.add_assoc in e. rewrite Nat.add_shuffle0 in e.
  rewrite Nat.even_add_even in e. rewrite Nat.even_add in e.
  rewrite I in e. destruct (Nat.even (length a)). reflexivity.
  simpl in e. inversion e. simpl.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.

  apply not_false_is_true in n0.
  assert (K: even (length (hd ++ [b1;b1] ++ a ++ [b2;b2])) = true).
  replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]).
  rewrite app_length. rewrite Nat.even_add.
  rewrite n0. reflexivity.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.

  assert (N: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) true
    = count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) false).
  replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
    with ((hd ++ [b1;b1] ++ a ++ [b2;b2]) ++ tl) in H.
  generalize K. generalize H. apply tm_step_count_occ.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.

  assert (M: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) true
    = count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) false).
  replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2] ++ tl) in H.
  generalize n0. generalize H. apply tm_step_count_occ.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.

  replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]) in N.
  rewrite count_occ_app in N. symmetry in N.
  rewrite count_occ_app in N. rewrite M in N.
  rewrite Nat.add_cancel_l in N.
  destruct b2. simpl in N. inversion N. simpl in N. inversion N.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.
Qed.


(**
   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.
*)

Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl -> length a = 5
  -> a <> [ true; false; true; false; true].
Proof.
  intros n hd a tl. intros H I.

  destruct n.
  assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
  rewrite H in H0 at 2. simpl in H0.
  rewrite app_length in H0. rewrite app_length in H0.
  rewrite I in H0. rewrite Nat.add_shuffle3 in H0.
  apply Nat.succ_inj in H0. inversion H0.

  assert (even (length (tm_step (S n))) = true).
  rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul.
  apply Nat.le_0_l.

  assert (J: even (length hd) = negb (even (length tl))).
  rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
  rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0.
  destruct (even (length hd)); destruct (even (length tl)).
  inversion H0. reflexivity. reflexivity. inversion H0.

  assert (K: {a=[true; false; true; false; true]}
           + {~ a=[ true; false; true; false; true]}).
  apply list_eq_dec. apply bool_dec. destruct K.

  assert ({even (length hd) = true} + {even (length hd) <> true}).
  apply bool_dec. destruct H1.

  (* case length hd is even *)
  rewrite e0 in J. rewrite Nat.negb_even in J.
  destruct tl. inversion J.
  destruct b.

  assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
  generalize e0. generalize H. apply tm_step_count_occ.

  assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true
        = count_occ Bool.bool_dec (hd ++ a ++ [true]) false).
  assert (even (length (hd ++ a ++ [true])) = true).
  rewrite app_length. rewrite app_length.
  rewrite Nat.even_add. rewrite Nat.even_add.
  rewrite e0. rewrite e. reflexivity.
  replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H.
  generalize H2. generalize H. apply tm_step_count_occ.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.

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

  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
  rewrite e in H2. simpl in H2. inversion H2.

  replace (hd ++ a ++ false::tl)
    with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  simpl. apply Nat.lt_0_2.

  rewrite e. reflexivity.

  (* case length hd is odd *)
  apply not_true_is_false in n0.
  rewrite app_removelast_last with (l := hd) (d := true) in H.
  rewrite app_removelast_last with (l := hd) (d := true) in n0.
  rewrite app_length in n0. simpl in n0.
  rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0.
  rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0.

  destruct (last hd true).
  rewrite <- app_assoc in H.
  assert (count_occ Bool.bool_dec (removelast hd) true
        = count_occ Bool.bool_dec (removelast hd) false).
  generalize n0. generalize H. apply tm_step_count_occ.
  replace (removelast hd ++ [true] ++ a ++ tl)
    with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H.
  assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true
        = count_occ Bool.bool_dec (removelast hd ++ [true;true]) false).
  assert (even (length (removelast hd ++ [true;true])) = true).
  rewrite app_length. rewrite Nat.even_add_even. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
  generalize H2. generalize H. apply tm_step_count_occ.

  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
  rewrite H1 in H2. rewrite Nat.add_cancel_l in H2.
  simpl in H2. inversion H2.

  rewrite e. rewrite app_assoc_reverse. reflexivity.

  replace ((removelast hd ++ [false]) ++ a ++ tl)
    with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  simpl. apply Nat.lt_0_2.

  rewrite e. rewrite app_assoc_reverse. reflexivity.

  assert (length hd <> 0). destruct hd. inversion n0.
  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
  assert (length hd <> 0). destruct hd. inversion n0.
  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.

  assumption.
Qed.

Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl -> length a = 5
  -> a <> [ false; true; false; true; false].
Proof.
  intros n hd a tl. intros H I.
  assert (K: {a=[false; true; false; true; false]}
           + {~ a=[false; true; false; true; false]}).
  apply list_eq_dec. apply bool_dec. destruct K.
  assert (tm_step (S n) = hd ++ a ++ tl
          ++ (map negb hd) ++ [ true; false; true; false; true ]
          ++ (map negb tl)).
  rewrite tm_build. rewrite H.
  rewrite map_app. rewrite map_app.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. rewrite e. reflexivity.
  rewrite app_assoc in H0. rewrite app_assoc in H0.
  rewrite app_assoc in H0. apply tm_step_factor5 in H0.
  contradiction H0. reflexivity.
  reflexivity. assumption.
Qed.


Lemma tm_step_consecutive_identical_length :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl -> length a = 5
  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
Proof.
  intros n hd a tl. intros H I.
  destruct a. inversion I. destruct a. inversion I.
  destruct a. inversion I. destruct a. inversion I.
  destruct a. inversion I.

  assert (a = nil). simpl in I.
  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
  apply Nat.succ_inj in I.
  apply length_zero_iff_nil in I. assumption.
  rewrite H0. rewrite H0 in H. rewrite H0 in I.

  destruct b; destruct b0; destruct b1; destruct b2; destruct b3.

  exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity.
  exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity.
  exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity.
  exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity.
  exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity.
  exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity.
  exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity.
  exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity.

  exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
  exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
  apply tm_step_factor5 in H. contradiction H. reflexivity. reflexivity.
  exists (true::false::true::nil). exists (nil). exists false. simpl. reflexivity.
  exists (true::false::false::nil). exists (nil). exists true. simpl. reflexivity.
  exists (true::nil). exists (true::false::nil). exists false. simpl. reflexivity.
  exists (true::nil). exists (false::true::nil). exists false. simpl. reflexivity.
  exists (true::false::nil). exists (false::nil). exists false. simpl. reflexivity.
  exists (false::nil). exists (true::true::nil). exists true. simpl. reflexivity.
  exists (false::nil). exists (true::false::nil). exists true. simpl. reflexivity.
  exists (false::nil). exists (false::true::nil). exists true. simpl. reflexivity.
  exists (false::nil). exists (false::false::nil). exists true. simpl. reflexivity.
  exists (false::true::false::nil). exists (nil). exists true. simpl. reflexivity.
  apply tm_step_factor5' in H. contradiction H. reflexivity. reflexivity.
  exists (false::true::nil). exists (true::nil). exists false. simpl. reflexivity.
  exists (false::true::nil). exists (false::nil). exists false. simpl. reflexivity.
  exists (false::false::nil). exists (true::nil). exists true. simpl. reflexivity.
  exists (false::false::nil). exists (false::nil). exists true. simpl. reflexivity.
  exists (nil). exists (true::false::true::nil). exists false. simpl. reflexivity.
  exists (nil). exists (true::false::false::nil). exists false. simpl. reflexivity.
  exists (nil). exists (false::true::true::nil). exists false. simpl. reflexivity.
  exists (nil). exists (false::true::false::nil). exists false. simpl. reflexivity.
  exists (nil). exists (false::false::true::nil). exists false. simpl. reflexivity.
  exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
Qed.

Lemma tm_step_consecutive_identical_length' :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl -> 4 < length a
  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
Proof.
  intros n hd a tl. intros H I.
  rewrite <- firstn_skipn with (l := a) (n := 5).
  assert (length (firstn 5 a) = 5).
  apply firstn_length_le. apply Nat.le_succ_l. apply I.
  rewrite <- firstn_skipn with (l := a) (n := 5) in H.
  rewrite <- app_assoc in H.
  assert (exists (b1 c1 : list bool) (d1 : bool),
    firstn 5 a = b1 ++ [d1; d1] ++ c1).
  generalize H0. generalize H. apply tm_step_consecutive_identical_length.
  destruct H1. destruct H1. destruct H1. rewrite H1.
  exists x. exists (x0 ++ (skipn 5 a)). exists x1.
  rewrite <- app_assoc. apply app_inv_head_iff.
  rewrite <- app_assoc. reflexivity.
Qed.


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.