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

   TODO

*)

Require Import thue_morse.
Require Import thue_morse2.
Require Import thue_morse3.

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

Require Import Arith.
Require Import Lia.

Import ListNotations.


Theorem tm_step_palindrome_power2_inverse :
  forall (m n k : nat) (hd tl : list bool),
    tm_step n = hd ++ tl
    -> length hd = S (Nat.double k) * 2^m
    -> odd m = true
    -> tl <> nil
    -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
Proof.
  intros m n k hd tl. intros H I J K.

  assert (L: 2^m <= length hd). rewrite I. lia.
  assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)).
  rewrite H. reflexivity. rewrite tm_size_power2 in H0.
  rewrite app_length in H0. (* rewrite I in H0. *)
  assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H1.
  apply Nat.pow_le_mono_r with (a := 2) in H1.
  assert (2^n <= length hd). generalize L. generalize H1. apply Nat.le_trans.
  rewrite H0 in H2. rewrite <- Nat.add_0_r in H2.
  rewrite <- Nat.add_le_mono_l in H2. destruct tl. contradiction K.
  reflexivity. simpl in H2. apply Nat.nle_succ_0 in H2. contradiction.
  easy. assumption.

  assert (N: length (tm_step n) mod 2^m = 0). rewrite tm_size_power2.
  apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite <- Nat.pow_sub_r.
  rewrite <- Nat.pow_add_r. rewrite Nat.add_comm. rewrite Nat.sub_add.
  reflexivity. apply Nat.lt_le_incl. assumption. easy.
  apply Nat.lt_le_incl. assumption.

  assert (O: length hd mod 2^m = 0).
  apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite I.
  rewrite Nat.div_mul. rewrite Nat.mul_comm. reflexivity.
  apply Nat.pow_nonzero. easy.

  assert (P: length tl mod 2 ^ m = 0).
  rewrite H in N. rewrite app_length in N.
  rewrite <- Nat.add_mod_idemp_l in N. rewrite O in N. assumption.
  apply Nat.pow_nonzero. easy.

  assert (Q: 2^m <= length tl). apply Nat.div_exact in P. rewrite P.
  destruct (length tl / 2^m). rewrite Nat.mul_0_r in P.
  apply length_zero_iff_nil in P. rewrite P in K. contradiction K.
  reflexivity.
  rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l.
  apply Nat.le_succ_l. apply Nat.lt_0_succ.
  apply Nat.pow_nonzero. easy.

  replace hd
    with (firstn (length hd - 2^m) hd ++ skipn (length hd - 2^m) hd) in H.
  replace tl with (firstn (2^m) tl ++ skipn (2^m) tl) in H.
  rewrite <- app_assoc in H.
  replace (
    skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl ++ skipn (2 ^ m) tl )
    with (
    (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) ++ skipn (2 ^ m) tl )
    in H.
  assert (length (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) = 2^(S m)).
  rewrite app_length. rewrite skipn_length. rewrite firstn_length_le.
  replace (length hd) with (length hd -2^m + 2^m) at 1.
  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. simpl. rewrite Nat.add_0_r.
  reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption.
  assumption.

  assert (length (firstn (length hd - 2^m) hd) mod 2^(S m) = 0).
  rewrite firstn_length_le. replace (2^m) with (2^m * 1).
  rewrite I. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_l.
  rewrite Nat.sub_succ. rewrite Nat.sub_0_r. rewrite Nat.double_twice.
  rewrite Nat.mul_assoc. replace (2^m * 2) with (2^(S m)).
  rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity.
  apply Nat.pow_nonzero. easy.
  rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity.
  apply Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l.

  assert (
    skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m)
    \/
    skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = map negb (tm_step (S m))).
  generalize H1. generalize H0. generalize H. apply tm_step_repeating_patterns2.

  apply tm_step_palindromic_full in J.
  destruct H2; rewrite J in H2.
  - assert (skipn (length hd - 2^m) hd = tm_step m).
    apply app_eq_length_head in H2. assumption.
    rewrite skipn_length.
    replace (length hd) with (length hd -2^m + 2^m) at 1.
    rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite tm_size_power2.
    reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3.
    assert (firstn (2^m) tl = rev (tm_step m)).
    rewrite H3 in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity.
    rewrite H4. rewrite rev_involutive. reflexivity.
  - assert (skipn (length hd - 2^m) hd = map negb (tm_step m)).
    rewrite map_app in H2. apply app_eq_length_head in H2. assumption.
    rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1.
    rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
    rewrite map_length. rewrite tm_size_power2.
    reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3.
    assert (firstn (2^m) tl = map negb (rev (tm_step m))).
    rewrite H3 in H2. rewrite map_app in H2. apply app_inv_head in H2.
    rewrite <- H2. reflexivity.
    rewrite H4. rewrite map_rev. rewrite rev_involutive. reflexivity.
  - rewrite <- app_assoc. reflexivity.
  - rewrite firstn_skipn. reflexivity.
  - rewrite firstn_skipn. reflexivity.
Qed.


Theorem tm_step_palindrome_power2_inverse' :
  forall (m n k : nat) (hd tl : list bool),
    tm_step n = hd ++ tl
    -> length hd = S (Nat.double k) * 2^m
    -> odd m = true
    -> 0 < k
    -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
Proof.
  intros m n k hd tl. intros H I J L.

  assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
  destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H.
  rewrite <- H in I. rewrite tm_size_power2 in I.

  assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0.
  apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0.
  rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0.
  rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0.
  rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0.
  rewrite H0 in L. inversion L. easy.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy.
  replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I.
  rewrite Nat.mul_cancel_r in I.

  assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0.
  apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0.
  rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
  apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1.
  rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1.
  inversion H1. apply Nat.pow_nonzero. easy. lia.

  generalize K. generalize J. generalize I. generalize H.
  apply tm_step_palindrome_power2_inverse.
Qed.


Lemma tm_step_square_even_rev :
  forall (j n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
  -> a = rev a.
Proof.
  intro j. induction j; intros n hd a tl; intros H I.
  - destruct I.
    + destruct a. inversion H0. destruct a. reflexivity. inversion H0.
    + destruct a. inversion H0. destruct a. inversion H0. destruct a.
      inversion H0. destruct a.
      assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
      rewrite e. reflexivity.
      assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
      rewrite e in H.
      replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
        with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
      apply tm_step_consecutive_identical' in H. inversion H.
      rewrite <- app_assoc. reflexivity.
      assert (b = b0). destruct b; destruct b0; destruct b1;
      reflexivity || contradiction n0 || contradiction n1; reflexivity.
      rewrite H1 in H.
      replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
        with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
      apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
      inversion H0.
  - assert (even (length a) = true).
    destruct I; rewrite H0; rewrite Nat.double_S;
    rewrite Nat.pow_succ_r.
    rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
    rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.

    assert (0 < length a). destruct I; rewrite H1.
    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
    apply Nat.mul_pos_pos. lia.
    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

    assert (even (length (hd ++ a)) = true). generalize H1. generalize H.
    apply tm_step_square_pos. 

    assert (even (length hd) = true). rewrite app_length in H2.
    rewrite Nat.even_add in H2. rewrite H0 in H2.
    destruct (even (length hd)). reflexivity. inversion H2.

    assert (2 <= n).
    assert (length (tm_step n) = length (tm_step n)). reflexivity.
    rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4.
    rewrite app_length in H4. destruct I; rewrite H5 in H4;
    rewrite tm_size_power2 in H4; rewrite Nat.double_S in H4;
    symmetry in H4; apply Nat.eq_le_incl in H4.
    assert (2^(S (S (Nat.double j))) <= 2^n).
    assert (2^(S (S (Nat.double j)))
       <= 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd).
    rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4.
    generalize H6. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H6.
    assert (2 <= S (S (Nat.double j))). lia. generalize H6. generalize H7.
    apply Nat.le_trans. apply Nat.lt_1_2.
    assert (3 * 2^(S (S (Nat.double j))) <= 2^n).
    assert (3 * 2^(S (S (Nat.double j)))
       <= 3 * 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd).
    rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4.
    generalize H6. apply Nat.le_trans.
    assert (2^(S (S (Nat.double j))) <= 3 * 2^(S (S (Nat.double j)))).
    rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_pos_r.
    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. lia.
    assert (2^(S (S (Nat.double j))) <= 2^n).
    generalize H6. generalize H7. apply Nat.le_trans.
    rewrite <- Nat.pow_le_mono_r_iff in H8.
    assert (2 <= S (S (Nat.double j))). lia. generalize H8. generalize H9.
    apply Nat.le_trans. apply Nat.lt_1_2.
    destruct n. inversion H4. destruct n. inversion H4. inversion H6.

    assert(
     tm_step (S (S n)) = tm_morphism
      (firstn (Nat.div2 (length hd)) (tm_step (S n)) ++
       firstn (Nat.div2 (length a))
         (skipn (Nat.div2 (length hd)) (tm_step (S n))) ++
       firstn (Nat.div2 (length a))
         (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))) ++
       skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n)))).
    generalize H0. generalize H0. generalize H3. generalize H.
    apply tm_step_morphism4.

    pose (hd' := firstn (Nat.div2 (length hd)) (tm_step (S n))).
    pose (a' := firstn (Nat.div2 (length a))
          (skipn (Nat.div2 (length hd)) (tm_step (S n)))).
    pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n))).
    fold hd' in H5. fold a' in H5. fold tl' in H5.

    assert (length hd' = Nat.div2 (length hd)). unfold hd'.
    rewrite firstn_length_le. reflexivity.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
    rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
    rewrite H. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.

    assert (length hd = length (tm_morphism hd')).
    rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double. reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

    assert (length a' = Nat.div2 (length a)). unfold a'.
    rewrite firstn_length_le. reflexivity. rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H. rewrite app_length. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (length a = length (tm_morphism a')).
    rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double. reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

    rewrite H in H5. rewrite tm_morphism_app in H5.

    assert (hd = tm_morphism hd'). generalize H7. generalize H5.
    apply app_eq_length_head. rewrite <- H10 in H5.
    apply app_inv_head in H5. rewrite tm_morphism_app in H5.

    assert (a = tm_morphism a'). generalize H9. generalize H5.
    apply app_eq_length_head. rewrite <- H11 in H5.
    apply app_inv_head in H5. rewrite tm_morphism_app in H5.

    assert (length a = length (tm_morphism (
        firstn (Nat.div2 (length a))
          (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n)))))).
    rewrite tm_morphism_length. rewrite firstn_length_le.
    rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
    reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H. rewrite app_assoc.
    rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
    rewrite app_length. lia. apply Nat.le_refl.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (a = tm_morphism (
        firstn (Nat.div2 (length a))
          (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))))).
    generalize H12. generalize H5. apply app_eq_length_head.
    rewrite <- H13 in H5. apply app_inv_head in H5.

    assert (H' := H).
    rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'.
    rewrite <- tm_morphism_app in H'.
    rewrite <- tm_morphism_app in H'.
    rewrite <- tm_morphism_app in H'.
    rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'.

    assert (even (length a') = true). unfold a'.
    rewrite firstn_length_le.
    destruct I; rewrite H14; rewrite Nat.double_S.
    rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
    rewrite Nat.div2_double.
    rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l.
    rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
    rewrite <- Nat.mul_assoc.
    rewrite Nat.div2_double.
    rewrite Nat.even_mul. rewrite Nat.even_mul.
    reflexivity. apply Nat.le_0_l. apply Nat.le_0_l.
    rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H. rewrite app_length. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (0 < length a'). unfold a'. rewrite firstn_length_le.
    destruct (length a). destruct I. inversion H1. inversion H1.
    destruct n0. inversion H0. replace (S (S n0)) with (n0 + 1*2).
    rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia.
    easy. lia.
    rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H. rewrite app_length. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (even (length (hd' ++ a')) = true). generalize H15.
    generalize H'. apply tm_step_square_pos.

    assert (even (length hd') = true). rewrite app_length in H16.
    rewrite Nat.even_add in H16. rewrite H14 in H16.
    destruct (even (length hd')). reflexivity. inversion H16.

    assert (
     tm_step (S n) = tm_morphism
      (firstn (Nat.div2 (length hd')) (tm_step n) ++
       firstn (Nat.div2 (length a'))
         (skipn (Nat.div2 (length hd')) (tm_step n)) ++
       firstn (Nat.div2 (length a'))
         (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)) ++
       skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n))).
    generalize H14. generalize H14. generalize H17. generalize H'.
    apply tm_step_morphism4.

    pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)).
    pose (a'' := firstn (Nat.div2 (length a'))
          (skipn (Nat.div2 (length hd')) (tm_step n))).
    pose (tl'' := skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n)).
    fold hd'' in H18. fold a'' in H18. fold tl'' in H18.

    assert (length hd'' = Nat.div2 (length hd')). unfold hd''.
    rewrite firstn_length_le. reflexivity.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
    rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
    rewrite H'. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.

    assert (length hd' = length (tm_morphism hd'')).
    rewrite tm_morphism_length. rewrite H19. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double. reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

    assert (length a'' = Nat.div2 (length a')). unfold a''.
    rewrite firstn_length_le. reflexivity. rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H'. rewrite app_length. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (length a' = length (tm_morphism a'')).
    rewrite tm_morphism_length. rewrite H21. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double. reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

    rewrite H' in H18. rewrite tm_morphism_app in H18.

    assert (hd' = tm_morphism hd''). generalize H20. generalize H18.
    apply app_eq_length_head. rewrite <- H23 in H18.
    apply app_inv_head in H18. rewrite tm_morphism_app in H18.

    assert (a' = tm_morphism a''). generalize H22. generalize H18.
    apply app_eq_length_head. rewrite <- H24 in H18.
    apply app_inv_head in H18. rewrite tm_morphism_app in H18.

    assert (length a' = length (tm_morphism (
        firstn (Nat.div2 (length a'))
          (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n))))).
    rewrite tm_morphism_length. rewrite firstn_length_le.
    rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
    reflexivity.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H'. rewrite app_assoc.
    rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
    rewrite app_length. lia. apply Nat.le_refl.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (a' = tm_morphism (
        firstn (Nat.div2 (length a'))
          (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))).
    generalize H25. generalize H18. apply app_eq_length_head.
    rewrite <- H26 in H18. apply app_inv_head in H18.

    assert (H'' := H').
    rewrite H23 in H''. rewrite H24 in H''. rewrite H18 in H''.
    rewrite <- tm_morphism_app in H''.
    rewrite <- tm_morphism_app in H''.
    rewrite <- tm_morphism_app in H''.
    rewrite <- tm_step_lemma in H''. rewrite <- tm_morphism_eq in H''.

    assert (0 < length a''). unfold a''. rewrite firstn_length_le.
    destruct (length a'). inversion H15. destruct n0. inversion H14.
    replace (S (S n0)) with (n0 + 1*2).
    rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia.
    easy. lia.
    rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
    rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
    rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
    rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
    rewrite <- Nat.Even_double.
    rewrite H'. rewrite app_length. rewrite app_length. lia.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    lia. lia.

    assert (length a = 4 * length a''). rewrite H9. rewrite H24.
    rewrite tm_morphism_length. rewrite tm_morphism_length. lia.

    assert (
      length a'' = 2 ^ Nat.double j \/ length a'' = 3 * 2 ^ Nat.double j ).
    destruct I. left.
    rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28.
    replace 4 with (2*2). rewrite <- Nat.mul_assoc.
    rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r.
    rewrite <- Nat.double_S. assumption. lia. lia. lia. lia.
    right.
    rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28.
    rewrite Nat.mul_assoc. replace (4*3) with (3*2*2).
    rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
    rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
    rewrite <- Nat.double_S. assumption. lia. lia. lia. lia.

    assert (a'' = rev a''). generalize H29. generalize H''. apply IHj.

    assert (Z := H11).
    rewrite H24 in H11. rewrite H30 in H11.
    rewrite <- tm_morphism_twice_rev in H11.
    rewrite <- H24 in H11. rewrite <- Z in H11. assumption.
Qed.


Lemma tm_step_square_odd_rev :
  forall (j n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j))
  -> a = map negb (rev a).
Proof.
  intros j n hd a tl. intros H I.

  assert (even (length a) = true).
  destruct I; rewrite H0; rewrite Nat.pow_succ_r.
  rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
  rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.

  assert (0 < length a). destruct I; rewrite H1.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
  apply Nat.mul_pos_pos. lia.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  assert (even (length (hd ++ a)) = true). generalize H1. generalize H.
  apply tm_step_square_pos. 

  assert (even (length hd) = true). rewrite app_length in H2.
  rewrite Nat.even_add in H2. rewrite H0 in H2.
  destruct (even (length hd)). reflexivity. inversion H2.

  assert (0 < n).
  assert (length (tm_step n) = length (tm_step n)). reflexivity.
  rewrite H in H4 at 2. rewrite app_length in H4.
  rewrite Nat.add_comm in H4.
  destruct a. inversion H1. simpl in H4. rewrite app_length in H4.
  simpl in H4. rewrite Nat.add_succ_r in H4.
  destruct n. inversion H4. lia.
  destruct n. inversion H4.

  assert(
   tm_step (S n) = tm_morphism
    (firstn (Nat.div2 (length hd)) (tm_step n) ++
     firstn (Nat.div2 (length a))
       (skipn (Nat.div2 (length hd)) (tm_step n)) ++
     firstn (Nat.div2 (length a))
       (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
     skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n))).
  generalize H0. generalize H0. generalize H3. generalize H.
  apply tm_step_morphism4.

  pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)).
  pose (a' := firstn (Nat.div2 (length a))
        (skipn (Nat.div2 (length hd)) (tm_step n))).
  pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step n)).
  fold hd' in H5. fold a' in H5. fold tl' in H5.

  assert (length hd' = Nat.div2 (length hd)). unfold hd'.
  rewrite firstn_length_le. reflexivity.
  rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
  rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
  rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
  rewrite H. rewrite app_length. lia.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.

  assert (length hd = length (tm_morphism hd')).
  rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double. reflexivity.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

  assert (length a' = Nat.div2 (length a)). unfold a'.
  rewrite firstn_length_le. reflexivity. rewrite skipn_length.
  rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
  rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
  rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
  rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double.
  rewrite H. rewrite app_length. rewrite app_length. lia.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  lia. lia.

  assert (length a = length (tm_morphism a')).
  rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double. reflexivity.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.

  rewrite H in H5. rewrite tm_morphism_app in H5.

  assert (hd = tm_morphism hd'). generalize H7. generalize H5.
  apply app_eq_length_head. rewrite <- H10 in H5.
  apply app_inv_head in H5. rewrite tm_morphism_app in H5.

  assert (a = tm_morphism a'). generalize H9. generalize H5.
  apply app_eq_length_head. rewrite <- H11 in H5.
  apply app_inv_head in H5. rewrite tm_morphism_app in H5.

  assert (length a = length (tm_morphism (
      firstn (Nat.div2 (length a))
        (skipn (Nat.div2 (length (hd ++ a))) (tm_step n))))).
  rewrite tm_morphism_length. rewrite firstn_length_le.
  rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
  reflexivity.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  rewrite skipn_length.
  rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
  rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
  rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
  rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double.
  rewrite H. rewrite app_assoc.
  rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
  rewrite app_length. lia. apply Nat.le_refl.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
  lia. lia.

  assert (a = tm_morphism (
      firstn (Nat.div2 (length a))
        (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
  generalize H12. generalize H5. apply app_eq_length_head.
  rewrite <- H13 in H5. apply app_inv_head in H5.

  assert (H' := H).
  rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'.
  rewrite <- tm_morphism_app in H'.
  rewrite <- tm_morphism_app in H'.
  rewrite <- tm_morphism_app in H'.
  rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'.

  assert (length a = 2 * length a'). rewrite tm_morphism_length in H9.
  assumption.

  assert (length a' = 2^(Nat.double j) \/ length a' = 3 * 2^(Nat.double j)).
  destruct I; [left | right]; rewrite <- Nat.mul_cancel_l with (p := 2).
  rewrite <- tm_morphism_length. rewrite <- H11.
  rewrite <- Nat.pow_succ_r. assumption. lia. lia.
  rewrite <- tm_morphism_length. rewrite <- H11.
  rewrite Nat.mul_assoc. replace (2*3) with (3*2).
  rewrite <- Nat.mul_assoc.
  rewrite <- Nat.pow_succ_r. assumption. lia. lia. easy.

  assert (Z := H11).
  assert (a' = rev a'). generalize H15. generalize H'.
  apply tm_step_square_even_rev. rewrite H16 in H11.
  rewrite <- tm_morphism_rev2 in H11. rewrite <- Z in H11.
  assumption.
Qed.

Theorem tm_step_square_rev :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> 0 < length a
  -> (  (a = rev a /\ exists j,
         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
     \/ (a = map negb (rev a) /\ exists j,
         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
Proof.
  intros n hd a tl. intros H I.

  assert (exists k j, length a = S (Nat.double k) * 2^j).
  apply trailing_zeros; assumption. destruct H0. destruct H0.

  assert (0 < n).
  assert (length (tm_step n) = length (tm_step n)). reflexivity.
  rewrite H in H1 at 2. rewrite app_length in H1.
  rewrite Nat.add_comm in H1.
  destruct a. inversion I. simpl in H1. rewrite app_length in H1.
  simpl in H1. rewrite Nat.add_succ_r in H1.
  destruct n. inversion H1. lia.
  destruct n. inversion H1.

  assert (x = 0 \/ x = 1). generalize H0. generalize H.
  apply tm_step_square_size.

  assert (Nat.Even x0 \/ Nat.Odd x0). apply Nat.Even_or_Odd.
  destruct H3. apply Nat.Even_double in H3. rewrite H3 in H0.

  assert (length a = 2^(Nat.double (Nat.div2 x0))
    \/ length a = 3 * 2^(Nat.double (Nat.div2 x0))).
  destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia.
  reflexivity.

  left. split.
  generalize H4. generalize H. apply tm_step_square_even_rev.
  exists (Nat.div2 x0). assumption.

  apply Nat.Odd_double in H3. rewrite H3 in H0.

  assert (length a = 2^(S (Nat.double (Nat.div2 x0)))
    \/ length a = 3 * 2^(S (Nat.double (Nat.div2 x0)))).
  destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia.
  reflexivity.

  right. split.
  generalize H4. generalize H. apply tm_step_square_odd_rev.
  exists (Nat.div2 x0). assumption.
Qed.


Lemma tm_step_square_rev_even :
  forall (m n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> length a = 2^m
  -> a = rev a
  -> even m = true.
Proof.
  intros m n hd a tl. intros H I J.

  assert (0 < length a). rewrite I.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  assert (  (a = rev a /\ exists j,
         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
     \/ (a = map negb (rev a) /\ exists j,
         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
  generalize H0. generalize H. apply tm_step_square_rev.
  destruct H1. destruct H1. destruct H2. destruct H2.
  rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2.
  rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia.
  rewrite I in H2.

  assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2.
  rewrite Nat.log2_pow2 in H3.
  rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3.
  rewrite H3 in H2. rewrite Nat.add_succ_r in H2.
  rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2.
  rewrite Nat.mul_cancel_r in H2. inversion H2.
  apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.

  destruct H1. rewrite J in H1 at 1.
  destruct a. inversion H0. simpl in H1.
  rewrite map_app in H1. apply app_inj_tail in H1.
  destruct H1. destruct b. inversion H3. inversion H3.
Qed.


Lemma tm_step_square_rev_odd :
  forall (m n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> length a = 2^m
  -> a = map negb (rev a)
  -> odd m = true.
Proof.
  intros m n hd a tl. intros H I J.

  assert (0 < length a). rewrite I.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  assert (  (a = rev a /\ exists j,
         length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j))
     \/ (a = map negb (rev a) /\ exists j,
         length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))).
  generalize H0. generalize H. apply tm_step_square_rev.
  destruct H1. destruct H1. rewrite J in H1 at 1.
  destruct a. inversion H0. simpl in H1.
  rewrite map_app in H1. apply app_inj_tail in H1.
  destruct H1. destruct b. inversion H3. inversion H3.

  destruct H1. destruct H2. destruct H2.
  rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2.
  rewrite Nat.odd_succ. rewrite Nat.double_twice.
  rewrite Nat.even_mul. reflexivity. lia.
  rewrite I in H2.

  assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2.
  rewrite Nat.log2_pow2 in H3.
  rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3.
  rewrite H3 in H2. rewrite Nat.add_succ_r in H2.
  rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2.
  rewrite Nat.mul_cancel_r in H2. inversion H2.
  apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia.
Qed.


Lemma xxx :
  forall (m n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ a ++ tl
  -> length a = 2^m
  -> a = rev a
  -> length (hd ++ a) mod (2^(S m)) = 0.
Proof.
  intros m n hd a tl. intros H I J.

  assert (0 < length a). rewrite I.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  assert (even m = true). generalize J. generalize I. generalize H.
  apply tm_step_square_rev_even.

  (*
  TODO: voir s'il faut remplacer la dernière implication
  par une équivalence
   *)
Abort.





Theorem tm_step_palindrome_power2' :
  forall (m n : nat) (hd a tl : list bool),
    tm_step n = hd ++ a ++ (rev a) ++ tl
    -> length a = 2^m
    -> 2 < m
    -> length (hd ++ a) mod 2^ (Nat.double (Nat.div2 (S m))) = 2^ (pred (Nat.double (Nat.div2 (S m)))).
Proof.
  intros m n hd a tl. intros H I J.
  assert (K: length (hd ++ a) mod 2^ (pred (Nat.double (Nat.div2 (S m)))) = 0).
  generalize J. generalize I. generalize H. apply tm_step_palindrome_power2.
  rewrite <- Nat.div_exact in K.
  assert (L: Nat.Even 
    (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m))))
    \/ Nat.Odd
    (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m))))).
  apply Nat.Even_or_Odd.
  destruct L.
  - assert (length (hd ++ a) mod 2 ^ Nat.double (Nat.div2 (S m)) = 0).
    rewrite K. apply Nat.Even_double in H0. symmetry in H0.
    rewrite Nat.double_twice in H0. rewrite <- H0. rewrite Nat.mul_assoc.
    rewrite Nat.mul_shuffle0. rewrite Nat.mul_comm. rewrite Nat.mul_assoc.
    rewrite <- Nat.pow_succ_r. rewrite Nat.succ_pred_pos. rewrite Nat.mul_comm.
    apply Nat.mod_mul. apply Nat.pow_nonzero. easy.
    assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd.
    destruct H1.
    apply Nat.Even_double in H1. rewrite <- H1. apply Nat.lt_0_succ.
    apply Nat.Odd_double in H1. apply Nat.succ_inj in H1.
    rewrite <- H1. apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
    assumption. apply Nat.le_0_l.
    (* on cherche une contradiction à partir de H1 *)
    assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd.
    destruct H2.
    + assert (E := H2). apply Nat.Even_double in H2. rewrite <- H2 in H1.
Abort.