coqbooks/src/thue_morse3.v

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

   TODO

   tm_step_rev
*)

Require Import thue_morse.
Require Import thue_morse2.

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

Import ListNotations.


Theorem tm_step_rev : forall (n : nat),
  tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n)).
Proof.
  assert (Z: forall l, map (fun x : bool => negb (negb x)) l = l).
  intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
  rewrite IHl. reflexivity.

  intro n. induction n. left. reflexivity.
  rewrite tm_build. destruct IHn ; [right | left];
    rewrite rev_app_distr; rewrite H at 1;
    rewrite H at 2; rewrite <- map_rev.
  rewrite map_app. rewrite map_map. rewrite Z. reflexivity.
  rewrite map_map. rewrite Z. reflexivity.
Qed.


Lemma tm_step_palindromic_odd : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl
  -> a = rev a
  -> odd (length a) = true
  -> length a < 4.
Proof.
  (* end of the lemma *)
  assert (LEMMA: forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ tl
  -> a = rev a
  -> odd (length a) = true
  -> length a <> 5).
  intros n hd a tl. intros H I J.
  destruct a. easy. destruct a. easy.
  destruct a. easy. destruct a. easy.
  destruct a. easy.

  destruct a. (* case of length 5 *)
  assert (exists (u v : list bool) (d: bool),
             b::b0::b1::b2::b3::nil = u ++ [d;d] ++ v).
  assert (4 < length (b::b0::b1::b2::b3::nil)). simpl.
  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. generalize H0. generalize H.
  apply tm_step_consecutive_identical_length.

  destruct H0. destruct H0. destruct H0.

  assert (K: {b=b0} + {~ b=b0}). apply bool_dec.
  assert (L: {b0=b1} + {~ b0=b1}). apply bool_dec.
  assert (M: {b1=b2} + {~ b1=b2}). apply bool_dec.
  assert (N: {b2=b3} + {~ b2=b3}). apply bool_dec.

  destruct K. rewrite e in H. rewrite e in I.
  destruct N. rewrite e0 in H.
  replace ([b0;b0;b1;b3;b3] ++ tl) with ([b0;b0] ++ [b1] ++ [b3;b3] ++ tl) in H.
  apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
  inversion I. rewrite H3 in n0. contradiction n0.

  destruct L. rewrite e in H. rewrite e in I.
  destruct M. rewrite <- e0 in H.
  replace (hd ++ [b; b1; b1; b1; b3] ++ tl)
  with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b1] ++ ([b3] ++ tl)) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_succ. rewrite <- app_assoc. simpl. reflexivity.

  inversion I. rewrite H3 in n1. contradiction n1.

  destruct M. rewrite <- e in I. inversion I.
  rewrite H3 in n1. contradiction n1.
  destruct N. rewrite e in I. inversion I.
  rewrite H2 in n0. rewrite H3 in n0. contradiction n0.

  destruct x. inversion H0.
  rewrite H2 in n0. rewrite H3 in n0. contradiction n0.
  reflexivity.

  destruct x. inversion H0.
  rewrite H3 in n1. rewrite H4 in n1. contradiction n1.
  reflexivity.

  destruct x. inversion H0.
  rewrite H4 in n2. rewrite H5 in n2. contradiction n2.
  reflexivity.

  destruct x. inversion H0.
  rewrite H5 in n3. rewrite H6 in n3. contradiction n3.
  reflexivity.

  assert (length [b;b0;b1;b2;b3] = length [b;b0;b1;b2;b3]).
  reflexivity. rewrite H0 in H1 at 2. simpl in H1.
  apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
  apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
  rewrite app_length in H1. simpl in H1.
  rewrite Nat.add_succ_r in H1. rewrite Nat.add_succ_r in H1.
  apply Nat.succ_inj in H1. apply O_S in H1. contradiction H1.

  simpl. apply not_eq_S. apply not_eq_S. apply not_eq_S.
  apply not_eq_S. apply not_eq_S. apply Nat.neq_succ_0.
  (* end of the lemma *)

  intros n hd a tl. intros H I J.

  assert (length a <= 5 \/ 5 < length a). apply Nat.le_gt_cases.
  destruct H0.
  apply Nat.lt_eq_cases in H0. destruct H0.
  rewrite Nat.lt_succ_r in H0.
  apply Nat.lt_eq_cases in H0. destruct H0. assumption.
  rewrite H0 in J. inversion J.
  assert (length a <> 5). generalize J. generalize I. generalize H.
  apply LEMMA. rewrite H0 in H1. contradiction H1.
  reflexivity.

  (* main part of the proof:
     each odd palindromic factor greater than 5
     contains a palindromic subfactor of length 5 *)
  pose (t := length a - 5). assert (Nat.even t = true).
  unfold t. rewrite Nat.even_sub. rewrite <- Nat.negb_odd.
  rewrite J. reflexivity. generalize H0.
  apply Nat.lt_le_incl.

  pose (u := firstn (Nat.div2 t) a).
  pose (v := firstn 5 (skipn (Nat.div2 t) a)).
  pose (w := skipn (Nat.div2 t + 5) a).

  assert (a = u ++ v ++ w).
  unfold u. unfold v. unfold w.
  rewrite firstn_skipn_comm.
  replace (Nat.div2 t) with (min (Nat.div2 t) (Nat.div2 t + 5)) at 1.
  rewrite <- firstn_firstn. rewrite app_assoc. rewrite firstn_skipn.
  rewrite firstn_skipn. reflexivity.
  apply Nat.min_l. rewrite <- Nat.add_0_r at 1.
  apply Nat.add_le_mono_l. apply le_0_n.

  assert (Nat.Even (length a - 5)).
  apply Nat.EvenT_Even. apply Nat.even_EvenT. rewrite Nat.even_sub.
  rewrite <- Nat.negb_odd. rewrite J. reflexivity.
  apply Nat.lt_le_incl. assumption.

  assert (length v = 5). unfold v. apply firstn_length_le.
  rewrite skipn_length. unfold t.
  rewrite Nat.mul_le_mono_pos_l with (p := 2).
  rewrite Nat.mul_sub_distr_l.
  replace (2 * Nat.div2 (length a - 5))
    with (Nat.double (Nat.div2 (length a - 5))).
  rewrite <- Nat.Even_double.

  replace (2 * length a) with ((length a + 5) + (length a - 5)).
  rewrite Nat.add_sub. replace (2*5) with (5+5).
  apply Nat.add_le_mono_r. apply Nat.lt_le_incl. assumption.
  reflexivity. rewrite <- Nat.add_assoc.

  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
  rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
  assumption. assumption.
  apply Nat.double_twice. apply Nat.lt_0_2.

  assert (length u = length w). unfold u. unfold w.
  rewrite firstn_length. rewrite skipn_length. rewrite Nat.min_l.
  unfold t. rewrite <- Nat.mul_cancel_l with (p := 2).
  rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
  rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_add_distr_l.
  rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double. rewrite Nat.double_twice.
  rewrite <- Nat.add_sub_swap. rewrite <- Nat.add_sub_assoc.
  replace (2 * length a) with ((length a - 5) + (length a + 5)).
  simpl. rewrite Nat.add_sub. reflexivity.
  rewrite Nat.add_comm. rewrite <- Nat.add_assoc.
  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
  rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
  assumption. simpl. apply le_n_S. apply le_n_S. apply le_n_S. apply le_n_S.
  apply le_n_S. apply le_0_n. apply Nat.lt_le_incl. assumption.
  assumption. assumption. easy.
  unfold t.
  rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
  rewrite <- Nat.Even_double. simpl. rewrite Nat.add_0_r.
  rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono.
  apply Nat.le_sub_l. apply le_0_n. assumption. apply Nat.lt_0_2.

  assert (v = rev v). rewrite H2 in I.
  rewrite rev_app_distr in I. rewrite rev_app_distr in I.
  rewrite <- app_assoc in I.

  assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
  generalize I. apply app_eq_length_head.
  rewrite H6 in I. rewrite rev_involutive in I.
  apply app_inv_head in I. apply app_inv_tail in I. assumption.

  assert (length v <> 5).
  assert (odd (length v) = true). rewrite H4. reflexivity.
  generalize H7. generalize H6. generalize H. rewrite H2.
  rewrite <- app_assoc. rewrite <- app_assoc. rewrite app_assoc.
  apply LEMMA. rewrite H4 in H7. contradiction H7.
  reflexivity.
Qed.

Lemma tm_step_palindromic_even_center :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> even (length (hd ++ a)) = true.
Proof.
  intros n hd a tl. intros H I.
  assert (J: a = removelast a ++ [ last a false ]).
  apply app_removelast_last.
  assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
  destruct K. rewrite e in I. inversion I. assumption.
  rewrite J in H. rewrite rev_app_distr in H.
  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
  rewrite app_assoc in H. 
  replace
    ([last a false] ++ rev [last a false] ++ rev (removelast a) ++ tl)
    with ([last a false; last a false] ++ (rev (removelast a) ++ tl)) in H.
  apply tm_step_consecutive_identical in H. rewrite J.
  rewrite app_assoc. rewrite app_length. rewrite Nat.even_add.
  rewrite <- Nat.negb_odd. rewrite H. reflexivity.
  reflexivity.
Qed.

Lemma tm_step_palindromic_even_center' :
  forall (n k m: nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> length (hd ++ a) = S (2 * k) * 2^m
  -> odd m = true.
Proof.
  intros n k m hd a tl. intros H I J.
  assert (Z := H).
  assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
  destruct K. rewrite e in I. inversion I.
  assert (L: a = removelast a ++ [ last a false ]).
  apply app_removelast_last. assumption.
  rewrite L in H. rewrite rev_app_distr in H.
  assert (nth_error (tm_step n) (length (hd++a))
    = nth_error (tm_step n) (pred (length (hd++a)))).
  rewrite H.
  rewrite app_assoc. rewrite nth_error_app2.
  symmetry. rewrite <- app_assoc. rewrite <- app_assoc.
  rewrite app_assoc. rewrite nth_error_app2.
  rewrite <- app_removelast_last. rewrite Nat.sub_diag.
  replace (hd++a) with ((hd ++ removelast a) ++ [last a false]).
  rewrite app_length. rewrite Nat.add_1_r. rewrite <- pred_Sn.
  rewrite Nat.sub_diag. reflexivity. rewrite L at 3.
  rewrite <- app_assoc. reflexivity. assumption.

  rewrite L at 2. rewrite app_assoc.
  replace (length ((hd ++ removelast a) ++ [last a false]))
    with (length (hd ++ removelast a) + length [last a false]).
  rewrite Nat.add_1_r. rewrite <- pred_Sn. apply Nat.le_refl.

  symmetry. rewrite app_length. reflexivity.
  rewrite <- app_removelast_last. apply Nat.le_refl.
  assumption.

  generalize H0. rewrite J. apply tm_step_pred.

  rewrite <- J. rewrite <- tm_size_power2. rewrite Z.
  rewrite app_length. rewrite app_length.
  apply Nat.add_lt_mono_l. rewrite app_length.
  rewrite <- Nat.add_0_r at 1.
  apply Nat.add_lt_mono_l. rewrite app_length. rewrite rev_length.
  assert (0 <= length tl). apply le_0_n. rewrite <- Nat.add_0_r at 1.
  apply Nat.add_lt_le_mono; assumption.
Qed.


Theorem tm_step_palindromic_full : forall (n : nat),
  odd n = true -> tm_step (S n) = (tm_step n) ++ rev (tm_step n).
Proof.
  intro n. intro H.
  apply Nat.odd_OddT in H. apply Nat.OddT_Odd in H.
  apply Nat.Odd_double in H. rewrite H. rewrite tm_step_odd_step.
  rewrite <- tm_build. reflexivity.
Qed.

(* very close to the previous one but we add the case n=0 here *)
Theorem tm_step_palindromic_full_even : forall (n : nat),
  even n = true -> tm_step n = rev (tm_step n).
Proof.
  intro n. intro H. destruct n. reflexivity.
  rewrite Nat.even_succ in H. apply tm_step_palindromic_full in H.
  rewrite H. rewrite rev_app_distr. rewrite rev_involutive.
  reflexivity.
Qed.


(**
   In this notebook I call "proper palindrome" in the Thue-Morse sequence,
   any palindromic subsequence such that the middle (of the palindromic
   subsequence) is not also the middle of a wider palindromic subsequence.
   In ther words, a proper palindrome can not be enlarged by adding more
   termes on both sides.
*)


(* palidrome 2*4 : soit centré en 4n+2 soit pas plus de 2*4 *)
(* on prouve facilement que hd != nil *)
Lemma tm_step_palindromic_length_8 :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> length a = 4
  -> length (hd ++ a) mod 4 = 0 \/ last hd false <> List.hd false tl.
Proof.
  intros n hd a tl. intros H I.

  (* proof that length hd++a is even *)
  assert (P: even (length (hd ++ a)) = true).
  assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0.
  generalize H. apply tm_step_palindromic_even_center.

  assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2).
  generalize P. apply even_mod4.

  (* proof that length hd is even *)
  assert (Q: even (length hd) = true). rewrite app_length in P.
  rewrite Nat.even_add_even in P. assumption. rewrite I.
  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.

  (* construction de a *)
  destruct a. inversion I. destruct a. inversion I.
  destruct a. inversion I. destruct a. inversion I.
  destruct a. simpl in H.

  (* proof that b1 <> b2 *)
  assert ({b1=b2} + {~ b1=b2}). apply bool_dec. destruct H0.
  replace (hd ++ b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
    with ((hd ++ b :: b0 :: nil)
              ++ [b1] ++ [b2] ++ [b2] ++  b1 :: b0 :: b :: tl) in H.
  rewrite e in H. apply tm_step_cubefree in H. contradiction H.
  reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.

  (* proof that n > 2 *)
  assert (2 < n).
  assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
        <= length hd
            + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)).
  apply Nat.add_le_mono. apply le_0_n. apply Nat.le_refl.
  rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J.
  rewrite tm_size_power2 in J.
  destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1.
  destruct n. inversion J. inversion H1.
  apply Nat.nle_succ_0 in H3. contradiction H3.
  destruct n. inversion J. inversion H1. inversion H3. inversion H5.
  inversion H7. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  apply Nat.lt_0_succ.

  (* proof that hd <> nil *)
  destruct hd.
  assert (Z: 4 < 2^n). replace 4 with (2^2).
  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
  assert (Some b2 = nth_error (tm_step n) 3). rewrite H. reflexivity.
  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H1.
  simpl in H1.
  assert (Some b2 = nth_error (tm_step n) 4). rewrite H. reflexivity.
  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H2.
  simpl in H2.
  rewrite H1 in H2. inversion H2. apply tm_step_stable. simpl.
  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. assumption. apply tm_step_stable. simpl.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (3 < 4).
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  generalize Z. generalize H2. apply Nat.lt_trans.
  
  (* proof that tl <> nil *)
  destruct tl.

  assert (Z: 4 < 2^n). replace 4 with (2^2).
  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.

  assert (Y: tm_step n = rev (tm_step n)
        \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev.
  destruct Y; rewrite H in H1 at 2; rewrite rev_app_distr in H1.

  assert (Some b2 = nth_error (tm_step n) 3). rewrite H1. reflexivity.
  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
  simpl in H2.
  assert (Some b2 = nth_error (tm_step n) 4). rewrite H1. reflexivity.
  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
  simpl in H3.
  rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
  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. assumption. apply tm_step_stable. simpl.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (3 < 4).
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  generalize Z. generalize H3. apply Nat.lt_trans.

  assert (Some (negb b2) = nth_error (tm_step n) 3). rewrite H1.
  rewrite nth_error_map. reflexivity.
  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
  simpl in H2.
  assert (Some (negb b2) = nth_error (tm_step n) 4). rewrite H1.
  rewrite nth_error_map. reflexivity.
  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
  simpl in H3.
  rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
  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. assumption. apply tm_step_stable. simpl.
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  assert (3 < 4).
  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
  generalize Z. generalize H3. apply Nat.lt_trans.

  (* première hypothèse   b0 = b1 mais alors on construit vers la
     gauche jusqu'à  (lest hd) et l'on a dans l'ordre jusqu'au centre :
       b1 | (negb b1) b1 | b1 (negb b1  ||
     et les quatre premiers termes vont impliquer que le centre soit en 4n+2 *)
  assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
  rewrite e in H.

  (* on a alors b = negb b1 (car dans le même bloc pair on a 01 ou 10 *)
  assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
  rewrite e0 in H.
  replace
    ((b3 :: hd) ++ b1 :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl)
    with
      ((b3 :: hd) ++ [b1] ++ [b1] ++ [b1]
              ++ b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_1. reflexivity.

  (* à ce stade on a F T | T F || F T T F
        trois cas :
              (??? T) | F T T F || F T T F | ???   impossible à gauche
                (T F) | F T T F || F T T F | (F T)  cube
                (T F) | F T T F || F T T F | (T F)   OK, diff + impossible à droite
   *)
  rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
  rewrite <- app_assoc in H.
  assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}).
  apply bool_dec. destruct H1. rewrite e0 in H.
  (* un cas à étudier 
                (??? T) | F T T F || F T T F | ???   impossible à gauche
  *)
  destruct M. left. assumption. (* ici on postule le modulo = 2 *)

  rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
  rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
  rewrite app_removelast_last with (l := b3::hd) (d := false) in H1.
  destruct Q.
  assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H2.
  assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H3.
  replace (
    removelast (b3 :: hd) ++
    [b1] ++ b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )
    with (
    removelast (b3 :: hd) ++ [b1;b;b1;b1]
      ++ (b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )) in H.
  generalize H. apply tm_step_factor4_1mod4. reflexivity.
  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
  contradiction n1. reflexivity.

  rewrite app_length in H1. rewrite app_length in H1.
  rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
  rewrite H2 in H1. inversion H1. easy. easy. easy.

  (* Deux cas
                (T F) | F T T F || F T T F | (F T)  cube
                (T F) | F T T F || F T T F | (T F)  impossible à droite
  *)
  assert ({b4=b1} + {~ b4=b1}). apply bool_dec. destruct H1. rewrite e0 in H.
     (* un sous-cas :
                (T F) | F T T F || F T T F | (T F)  impossible à droite
      *)
  destruct M. left. assumption. (* ici on postule le modulo = 2 *)

  rewrite e in H1.
  assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1.
  reflexivity. easy.

  replace(
    removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
    b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b1 :: tl )
  with (
    (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) ++ [b1; b1;b;b1] ++ tl) in H.

  assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H2.
  assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H3.
  generalize H. apply tm_step_factor4_3mod4.
  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
  contradiction n1. reflexivity.
  symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy.

  (* un sous-cas
                (T F) | F T T F || F T T F | (F T)  cube
  *)
  assert (b4 = b). destruct b4; destruct b1; destruct b.
  reflexivity. contradiction n3. reflexivity. reflexivity.
  contradiction n1. reflexivity. contradiction n1. reflexivity.
  reflexivity. contradiction n3. reflexivity. reflexivity. rewrite H1 in H.
  assert (b2 = b). destruct b2; destruct b1; destruct b.
  reflexivity. contradiction n0. reflexivity. reflexivity.
  contradiction n1. reflexivity. contradiction n1. reflexivity.
  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
  assert (last (b3::hd) false = b).
  destruct (last (b3::hd) false); destruct b1; destruct b.
  reflexivity. contradiction n2. reflexivity. reflexivity.
  contradiction n1. reflexivity. contradiction n1. reflexivity.
  reflexivity. contradiction n2. reflexivity. reflexivity.

       (* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
  destruct hd. inversion Q. destruct tl.
  assert (0 < n). assert (0 < 2). apply Nat.lt_0_2. generalize H0.
  generalize H4. apply Nat.lt_trans. apply tm_step_length_even in H4.
  rewrite H in H4.
  rewrite app_assoc in H4. rewrite <- app_removelast_last in H4.
  rewrite app_length in H4. rewrite Nat.even_add in H4.
  rewrite Q in H4. inversion H4. easy. rewrite H3 in H.
  rewrite app_removelast_last
         with (l := removelast (b3::b5::hd)) (d := false) in H.
  rewrite <- app_assoc in H.

  (* assigner
       last (removelast (b3 :: b5 :: hd)) false = b1
       b6 = b1
   *)
  assert ({last (removelast (b3 :: b5 :: hd)) false=b}
            + {~ last (removelast (b3 :: b5 :: hd)) false=b}). apply bool_dec.
  destruct H4. rewrite e0 in H.
  replace (
    removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b]
      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl)
    with (
    removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b] ++ [b]
      ++ b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_1. reflexivity.
  assert (last (removelast (b3 :: b5 :: hd)) false = b1).
  destruct (last (removelast (b3 :: b5 :: hd)) false); destruct b1; destruct b.
  reflexivity. reflexivity. contradiction n4. reflexivity.
  contradiction n1. reflexivity. contradiction n1. reflexivity.
  contradiction n4. reflexivity. reflexivity. reflexivity. rewrite H4 in H.
  assert ({b6=b} + {~ b6=b}). apply bool_dec. destruct H5. rewrite e0 in H.
  replace (
    removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b :: tl)
    with (
    (removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: nil)
      ++ [b] ++ [b] ++ [b] ++ tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
  assert (b6 = b1). destruct (b6); destruct b1; destruct b.
  reflexivity. reflexivity. contradiction n5. reflexivity.
  contradiction n1. reflexivity. contradiction n1. reflexivity.
  contradiction n5. reflexivity. reflexivity. reflexivity. rewrite H5 in H.

  (* contradiction *)
  replace (
    removelast (removelast (b3 :: b5 :: hd)) ++
    [b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b1 :: tl)
    with (removelast (removelast (b3 :: b5 :: hd)) ++
    [b1;b;b;b1] ++ [b1;b;b;b1] ++ [b1;b;b;b1] ++ tl) in H.
  apply tm_step_cubefree in H. contradiction H. reflexivity.
  apply Nat.lt_0_succ. reflexivity. easy. easy.





  




Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
    tm_step n' = w ++ z ++ y
    -> length z = 4 -> length w mod 4 = 3
    -> exists (x : bool), skipn 2 z = [x;x].


  rewrite app_length in H1. rewrite app_length in H1.
  rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
  rewrite H2 in H1. inversion H1. easy. easy. easy.








  (* sinon, sur la base de    T F T F || F T F T
        quatre cas :
                (F T) | T F T F || F T F T | (F T)     diff + impossible à droite
                (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
     empiriquement : n'apparaît jamais
                   remonter encore d'un cran et prouver la différence à ce stade,
                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
                     revoir l'énoncé en fonction
                (T F) | T F T F || F T F T | (F T)     cube
                (T F) | T F T F || F T F T | (T F)     diff + impossible à gauche


   *)
                  






Lemma tm_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool),
    tm_step n' = w ++ z ++ y
    -> length z = 4 -> length w mod 4 = 1
    -> exists (x : bool), firstn 2 z = [x;x].
Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
    tm_step n' = w ++ z ++ y
    -> length z = 4 -> length w mod 4 = 3
    -> exists (x : bool), skipn 2 z = [x;x].




  (* si on a ensuite le bloc précédent identique aux deux premiers de a




  (* TODO : terminer avec une inversion sur la longueur de a ;
     le dernier but vient de la destructuration initiale de a *)



      F T | T F    | T F ][ F T |    F T T F
                   4n

 ou         F T    | T F ][ F T | T F
                   4n ou 4n

         F T   F T T F F T T F    T F  (centre 4n+2 ET 4n : contra)
         T F   F T T F F T T F    T F  (centre : 4n+2)
         F T   F T T F F T T F    F T  (centre : 4n)
         T F   F T T F F T T F    F T  (cubes)  




              -->   T F   F T    | T F ][ F T | T F  F T  (impossible : cubes)
              -->   F T   F T    | T F ][ F T | T F  T F

  Bilan : seulement deux cas possible de palindrome 8
      F T | T F | T F ][ F T | F T | T F
         4n+2         4n+2    (trivial)

      F T | F T | T F ][ F T | T F | T F
                      4n   (par examen des cinq premiers termes à gauche)


Lemma tm_step_proper_palindromic_center :
  forall (m n k i: nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> length a = 2 ^ S (Nat.double m)
  -> length (hd ++ a) = S (Nat.double k) * 2 ^ i
  -> last hd false <> List.hd false tl
  -> i = 2 ^ S (Nat.double m).
Proof.
  intro m. induction m.
  - intros n  k i hd a tl. intros H I J K.
    destruct a. inversion I. destruct a. inversion I. destruct a.



















(* JUNK
Lemma xxx : forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ map negb (rev a) ++ tl
  -> length a = 4
  -> even (length hd) = true.
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.

  replace [b;b0;b1;b2] with ([b] ++ [b0] ++ [b1] ++ [b2]) in H at 1.
  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
  rewrite <- app_assoc in H.

  replace (map negb (rev [b; b0; b1; b2]))
    with ([negb b2] ++ [negb b1] ++ [negb b0] ++ [negb b]) in H.
  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
  rewrite <- app_assoc in H.

  assert (0 < length [b]). apply Nat.lt_0_1.
  assert (0 < length [b0]). apply Nat.lt_0_1.
  assert (0 < length [b1]). apply Nat.lt_0_1.
  assert (0 < length [b2]). apply Nat.lt_0_1.
  assert (J: {even (length hd) = true}
             + {~ even (length hd) = true}). apply bool_dec.

  destruct b; destruct b0; destruct b1; destruct b2.
  - assert ([true]<>[true]). generalize H0.
    generalize H. apply tm_step_cubefree.
    contradiction H4. reflexivity.
  - assert ([true]<>[true]). generalize H0.
    generalize H. apply tm_step_cubefree.
    contradiction H4. reflexivity.
  - assert([true] ++ [false] <> [true] ++ [false]). rewrite app_assoc in H.
    replace ( [true] ++ [false] ++ [true] ++ [negb true]
          ++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
      with ( ([true] ++ [false]) ++ ([true] ++ [negb true])
          ++ ([negb false] ++ [negb true]) ++ [negb true] ++ tl) in H.
    assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
    generalize H4. generalize H. apply tm_step_cubefree.
    reflexivity. contradiction H4. reflexivity.
  - assert (even (length (hd ++ [true] ++ [true] ++ [false] ++ [false])) = true).
    replace ( [true] ++ [true] ++ [false] ++ [false] ++ [negb false]
          ++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
      with ( ([true] ++ [true] ++ [false] ++ [false]) ++ ([negb false]
          ++ [negb false] ++ [negb true] ++ [negb true]) ++ tl) in H.
    assert (0 < length ([true] ++ [true] ++ [false] ++ [false])).
    apply Nat.lt_0_succ. generalize H4. generalize H. apply tm_step_square_pos.
    rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
    reflexivity.
    rewrite app_length in H4. simpl in H4.
    rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
    rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
    rewrite Nat.add_0_r in H4.
    rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
    rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
    rewrite H4. reflexivity.
  - destruct J. assumption.
    rewrite not_true_iff_false in n0.

    assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3).
    apply odd_mod4. rewrite <- Nat.negb_even. rewrite n0. reflexivity.
    destruct M.
    + replace ( [true] ++ [false] ++ [true] ++ [true]
          ++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
         with ( ([true] ++ [false] ++ [true] ++ [true])
          ++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
         in H.
      assert (exists (x:bool), firstn 2 [true;false;true;true] = [x;x]).
      generalize H4. generalize I. generalize H.
      apply tm_step_factor4_1mod4.
      destruct H5. inversion H5. inversion H8.
      rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
      reflexivity.
    + replace ( hd ++ [true] ++ [false] ++ [true] ++ [true]
          ++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
        with ( (hd ++ [true] ++ [false] ++ [true] ++ [true])
          ++ ([negb true] ++ [negb true] ++ [negb false] ++ [negb true]) ++ tl )
         in H.
      assert (exists (x:bool), skipn 2 [false;false;true;false] = [x;x]).
      assert (length (hd ++ [true]++[false]++[true]++[true]) mod 4 = 3).
      rewrite app_length. rewrite Nat.add_mod. rewrite H4. reflexivity.
      easy. generalize H5.
      assert (length [false;false;true;false]=4). reflexivity.
      generalize H6. generalize H. apply tm_step_factor4_3mod4.
      destruct H5. inversion H5. inversion H8.
      rewrite <- app_assoc. reflexivity.
  - assert([true] ++ [false] <> [true] ++ [false]).
    replace ( [true] ++ [false] ++ [true] ++ [false] ++ [negb false]
          ++ [negb true] ++ [negb false] ++ [negb true] ++ tl)
      with ( ([true] ++ [false]) ++ ([true] ++ [false])
          ++ ([negb false] ++ [negb true])
               ++ [negb false] ++ [negb true] ++ tl) in H.
    assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
    generalize H4. generalize H. apply tm_step_cubefree.
    reflexivity. contradiction H4. reflexivity.
  - destruct J. assumption. rewrite not_true_iff_false in n0.




 *)









(* TODO: bloqué

Lemma tm_step_proper_palindrome_center :
  forall (m n k : nat) (hd a tl : list bool),
    tm_step n = hd ++ a ++ (rev a) ++ tl
    -> length a = 2^(Nat.double m)     (* palindrome non propre *)
    -> skipn (length hd - length a) hd = rev (firstn (length a) tl).
Proof.
  induction m; intros n k hd a tl; intros H I.
  - simpl in I. destruct a. inversion I. destruct a.

    (* proof that hd is not nil *)
    destruct hd. assert (odd 0 = true).
    assert (nth_error (tm_step n) (S (2*0) * 2^0)
          = nth_error (tm_step n) (pred (S (2*0) * 2^0))).
    rewrite H. reflexivity. generalize H0.
    assert (S (2*0) * 2^0 < 2^n). destruct n. inversion H.
    rewrite Nat.mul_0_r. rewrite Nat.mul_1_l.
    apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_0_succ.
    generalize H1. apply tm_step_pred. inversion H0.

    (* proof that tl is not nil *)
    destruct tl. destruct n.
    assert (tm_step 0 = rev (tm_step 0)). reflexivity.
    rewrite H in H0 at 2. rewrite rev_app_distr in H0.
    simpl in H0. inversion H0. rewrite <- tm_step_lemma in H.
    assert (rev (tm_morphism (tm_step n)) = rev (tm_morphism (tm_step n))).
    reflexivity. rewrite H in H0 at 2. rewrite tm_morphism_rev in H0.
    rewrite rev_app_distr in H0. simpl in H0.
    destruct (map negb (rev (tm_step n))). inversion H0. simpl in H0.
    inversion H0. apply no_fixpoint_negb in H3. contradiction H3.

    (* proof that b <> b1 *)
    assert (J: {b=b1} + {~ b=b1}). apply bool_dec. destruct J.
    rewrite e in H.
    replace (rev [b1]) with ([b1]) in H.
    replace (b1::tl) with ([b1] ++ tl) in H.
    assert ([b1] <> [b1]). assert (0 < length [b1]). apply Nat.lt_0_1.
    generalize H0. generalize H. apply tm_step_cubefree.
    contradiction H0. reflexivity. reflexivity. reflexivity.

    (* proof that b <> last (b0::hd) false   *)
    assert (J: {b=last (b0::hd) false} + {~ b=last (b0::hd) false}).
    apply bool_dec. destruct J.
    rewrite app_removelast_last with (l := b0::hd) (d := false) in H.
    rewrite <- e in H. rewrite <- app_assoc in H.
    replace (rev [b]) with ([b]) in H.
    assert ([b] <> [b]). assert (0 < length [b]). apply Nat.lt_0_1.
    generalize H0. generalize H. apply tm_step_cubefree.
    contradiction H0. reflexivity. reflexivity. easy.

    (* proof that b1 = last (b0 :: hd) false  *)
    assert (b1 = last (b0 :: hd) false).
    destruct b; destruct b1; destruct (last (b0::hd) false).
    reflexivity. contradiction n0. reflexivity.
    contradiction n1. reflexivity. reflexivity.
    reflexivity. contradiction n1. reflexivity.
    contradiction n0. reflexivity. reflexivity.
    rewrite H0.

    rewrite <- rev_involutive at 1. rewrite <- firstn_rev.
    rewrite app_removelast_last with (l := b0::hd) (d := false) at 1.
    rewrite rev_app_distr. reflexivity.
    easy. inversion I.
  - assert (J: even (length (hd ++ a)) = true).
    assert (0 < length a). rewrite I.
    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
    generalize H0. generalize H. apply tm_step_palindromic_even_center.

    assert (H' := H).

    (* proof that 0 < n *)
    destruct n.
    assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
    rewrite H in H0 at 2. rewrite app_length in H0.
    rewrite app_length in H0. rewrite I in H0.
    assert (1 < 2^Nat.double(S m)).
    rewrite <- Nat.pow_0_r with (a := 2) at 1.
    apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
    rewrite Nat.double_S. apply Nat.lt_0_succ.
    assert (0 <= length (rev a ++ tl)). apply le_0_n.
    assert (1 < 2 ^ Nat.double (S m) + length (rev a ++ tl)).
    rewrite <- Nat.add_0_r at 1. generalize H2. generalize H1.
    apply Nat.add_lt_le_mono.
    assert (0 <= length hd). apply le_0_n.
    assert (1 < length (tm_step 0)). rewrite <- Nat.add_0_l at 1.
    rewrite H0. generalize H3. generalize H4.
    apply Nat.add_le_lt_mono.
    simpl in H5. apply Nat.lt_irrefl in H5. contradiction H5.

    rewrite <- tm_step_lemma in H.
    assert (K: even (length a) = true). rewrite Nat.double_S in I.
    rewrite Nat.pow_succ_r in I. rewrite I. rewrite Nat.even_mul.
    reflexivity. apply le_0_n.

    assert (L: even (length hd) = true).
    rewrite app_length in J. rewrite Nat.even_add in J.
    rewrite K in J. destruct (Nat.even (length hd)).
    reflexivity. inversion J.

    assert (M: hd = tm_morphism (firstn (Nat.div2 (length hd))
                         (tm_step n))).
    generalize L. generalize H. apply tm_morphism_app2.

    assert (N: a ++ rev a ++ tl
      = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
    generalize L. generalize H. apply tm_morphism_app3.
    symmetry in N.

    assert (O: a = tm_morphism (firstn (Nat.div2 (length a))
                    (skipn (Nat.div2 (length hd)) (tm_step n)))).
    generalize K. generalize N. apply tm_morphism_app2.

    assert (P: rev a ++ tl = tm_morphism (skipn (Nat.div2 (length a))
                    (skipn (Nat.div2 (length hd)) (tm_step n)))).
    generalize K. generalize N. apply tm_morphism_app3.
    symmetry in P.

    assert (even (length (rev a)) = true). rewrite rev_length. assumption.

    assert (R: tl = tm_morphism (skipn (Nat.div2 (length (rev a)))
              (skipn (Nat.div2 (length a))
                 (skipn (Nat.div2 (length hd)) (tm_step n))))).
    generalize H0. generalize P. apply tm_morphism_app3.

    rewrite M in H. rewrite O in H. rewrite R in H.
    rewrite tm_morphism_rev in H. rewrite <- tm_morphism_app in H.
    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
    rewrite <- tm_morphism_eq in H.
    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 (rev a)))
                    (skipn (Nat.div2 (length a))
                          (skipn (Nat.div2 (length hd)) (tm_step n)))).
    fold hd' in H. fold a' in H. fold tl' in H.

    assert (I': length a' = 2^S (Nat.double m)). unfold a'.
    rewrite firstn_length_le. rewrite I. rewrite Nat.double_S.
    rewrite Nat.pow_succ_r. rewrite Nat.div2_double. reflexivity.
    apply le_0_n. rewrite skipn_length.
    rewrite Nat.mul_le_mono_pos_r with (p := 2).
    rewrite Nat.mul_comm. rewrite <- Nat.add_0_r at 1.
    replace 0 with (Nat.b2n (Nat.odd (length a))) at 2.
    rewrite <- Nat.div2_odd. rewrite Nat.mul_sub_distr_r.
    replace (length (tm_step n) * 2) with (length (tm_step (S n))).
    replace (Nat.div2 (length hd) * 2) with (length hd).
    rewrite H'. rewrite app_length. rewrite Nat.add_sub_swap.
    rewrite Nat.sub_diag. simpl. rewrite app_length.
    rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l.
    apply Nat.le_0_l. apply Nat.le_refl.
    rewrite Nat.mul_comm. symmetry. rewrite <- Nat.add_0_r at 1.
    replace 0 with (Nat.b2n (Nat.odd (length hd))) at 2.
    rewrite <- Nat.div2_odd. reflexivity.
    rewrite <- Nat.negb_even. rewrite L. reflexivity.
    rewrite tm_build. rewrite app_length. rewrite Nat.mul_comm.
    simpl. rewrite Nat.add_0_r. rewrite map_length. reflexivity.
    rewrite <- Nat.negb_even. rewrite K. reflexivity.
    apply Nat.lt_0_2.

    assert (K': even (length a') = true). rewrite I'.
    rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
    apply le_0_n.
 *)

    (* le motif XX YY -> préfixe congru à 5 ou à 7 modulo 8 
     donc double du préfixe congru à 2 modulo 4 
       compatible avec ???
Lemma tm_step_palindromic_even_center' :
  forall (n k m: nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> length (hd ++ a) = S (2 * k) * 2^m
  -> odd m = true.
     *)





    (* réduire par la réciproque du morphisme *)




Lemma tm_morphism_app : forall (l1 l2 : list bool),
  tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
  tm_morphism l = hd ++ tl
  -> even (length hd) = true
  -> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
  tm_morphism l = hd ++ tl
  -> even (length hd) = true
  -> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
Lemma tm_step_palindromic_even_center :
  forall (n : nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> even (length (hd ++ a)) = true.
Lemma tm_step_palindromic_even_center' :
  forall (n k m: nat) (hd a tl : list bool),
  tm_step n = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> length (hd ++ a) = S (2 * k) * 2^m
  -> odd m = true.








Lemma tm_step_proper_palindrome_center :
  forall (n k m : nat) (hd a tl : list bool),
    tm_step n = hd ++ a ++ (rev a) ++ tl
    -> length a = 2^(Nat.double m)     (* palindrome non propre *)
    -> List.last hd false = List.hd false tl.
Proof.
  induction m.
  - intros. simpl in H0.
    destruct a. inversion H0. destruct a.

    (* proof that hd is not nil *)
    destruct hd. assert (odd 0 = true).
    assert (nth_error (tm_step n) (S (2*0) * 2^0)
          = nth_error (tm_step n) (pred (S (2*0) * 2^0))).
    rewrite H. reflexivity. generalize H1.
    assert (S (2*0) * 2^0 < 2^n). destruct n. inversion H.
    rewrite Nat.mul_0_r. rewrite Nat.mul_1_l.
    apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_0_succ.
    generalize H2. apply tm_step_pred. inversion H1.

    (* proof that tl is not nil *)
    destruct tl. destruct n.
    assert (tm_step 0 = rev (tm_step 0)). reflexivity.
    rewrite H in H1 at 2. rewrite rev_app_distr in H1.
    simpl in H1. inversion H1. rewrite <- tm_step_lemma in H.
    assert (rev (tm_morphism (tm_step n)) = rev (tm_morphism (tm_step n))).
    reflexivity. rewrite H in H1 at 2. rewrite tm_morphism_rev in H1.
    rewrite rev_app_distr in H1. simpl in H1.
    destruct (map negb (rev (tm_step n))). inversion H1. simpl in H1.
    inversion H1. destruct b; inversion H4.

    (* proof that b <> b1 *)
    assert (I: {b=b1} + {~ b=b1}). apply bool_dec. destruct I.
    rewrite e in H.
    replace (rev [b1]) with ([b1]) in H.
    replace (b1::tl) with ([b1] ++ tl) in H.
    assert ([b1] <> [b1]). assert (0 < length [b1]). apply Nat.lt_0_1.
    generalize H1. generalize H. apply tm_step_cubefree.
    contradiction H1. reflexivity. reflexivity. reflexivity.

    (* proof that b <> last (b0::hd) false   *)
    assert (I: {b=last (b0::hd) false} + {~ b=last (b0::hd) false}).
    apply bool_dec. destruct I.
    rewrite app_removelast_last with (l := b0::hd) (d := false) in H.
    rewrite <- e in H. rewrite <- app_assoc in H.
    replace (rev [b]) with ([b]) in H.
    assert ([b] <> [b]). assert (0 < length [b]). apply Nat.lt_0_1.
    generalize H1. generalize H. apply tm_step_cubefree.
    contradiction H1. reflexivity. reflexivity. easy.
    
    (* final part of the proof *)
    destruct b; destruct b1; destruct (last (b0::hd) false).
    reflexivity. contradiction n0. reflexivity.
    contradiction n1. reflexivity. reflexivity.
    reflexivity. contradiction n1. reflexivity.
    contradiction n0. reflexivity. reflexivity.
    inversion H0.

  - intros.















  induction m.
  - intros. simpl in H0.

    assert (I: a = (List.hd false a)::nil).
    destruct a. inversion H0. destruct a. reflexivity. inversion H0.

    assert (N: n = 0 \/ 0 < n). apply Nat.eq_0_gt_0_cases.
    destruct N as [N|N]. rewrite N in H.
    assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
    rewrite H in H1 at 2. rewrite app_length in H1.
    rewrite app_length in H1. rewrite app_length in H1.
    rewrite I in H1.
    rewrite Nat.add_1_l in H1. simpl in H1.
    rewrite Nat.add_comm in H1.
    rewrite Nat.add_succ_l in H1. rewrite Nat.add_succ_l in H1.
    apply Nat.succ_inj in H1. apply O_S in H1. contradiction H1.

    assert (J: hd <> nil).
    assert ({hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
    destruct H1. rewrite e in H.

    simpl in H. rewrite app_assoc in H.
    assert (count_occ bool_dec (a++rev a) true
      = count_occ bool_dec (a++rev a) false).
    assert (even (length (a++rev a))=true). rewrite I. reflexivity.
    generalize H1. generalize H. apply tm_step_count_occ.
    rewrite I in H1.

    rewrite tm_step_head_1 in H. rewrite <- app_assoc in H.
    inversion H. rewrite I in H3. inversion H3.
    rewrite <- H4 in H1. inversion H1.
    assumption.

    assert (K: tl <> nil).
    assert ({tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
    destruct H1. rewrite e in H.

    assert (count_occ bool_dec (hd++a++rev a) true
      = count_occ bool_dec (hd++a++rev a) false).
    assert (even (length (hd++a++rev a))=true).
    rewrite app_nil_r in H.
    rewrite <- H. rewrite tm_size_power2.
    destruct n. inversion N. rewrite Nat.pow_succ_r.
    rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
    rewrite app_assoc in H. rewrite app_assoc in H.
    replace ((hd++a)++rev a) with (hd++a++rev a) in H.
    generalize H1. generalize H. apply tm_step_count_occ.
    rewrite <- app_assoc. reflexivity.

    assert (count_occ bool_dec hd true
      = count_occ bool_dec hd false).
    assert (even (length hd)=true).
    assert (even (length (tm_step n)) = true).
    rewrite tm_size_power2. destruct n. inversion N. rewrite Nat.pow_succ_r.
    rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
    rewrite H in H2. rewrite app_length in H2.
    rewrite Nat.even_add in H2. rewrite I in H2. simpl in H2.
    destruct (Nat.even (length hd)). reflexivity. inversion H2.
    generalize H2. generalize H. apply tm_step_count_occ.

    rewrite count_occ_app in H1. symmetry in H1.
    rewrite count_occ_app in H1. rewrite H2 in H1.
    rewrite Nat.add_cancel_l in H1.
    destruct a. inversion H0. destruct a. destruct b.
    inversion H1. inversion H1. inversion H0.
    assumption.

    (* utiliser ici cubefree *)
    assert (last hd false = true).
    assert ({last hd false=true} + {~ last hd false=true}). apply bool_dec.
    destruct H1. assumption.







    assert (List.hd false (List.tl (tm_step n)) = nth 1 (tm_step n) false).

    

    replace (rev a) with a in H.

    assert (last hd false = negb (List.hd false a)).
    assert ({last hd false=List.hd false a}
             + {~ last hd false=List.hd false a}). apply bool_dec.
    destruct H1.
    replace hd with ((removelast hd) ++ a) in H.
    rewrite <- app_assoc in H.
    assert (0 < length a). rewrite H0. apply Nat.lt_0_1.
    assert (a<>a). generalize H1. generalize H. apply tm_step_cubefree.
    contradiction H2. reflexivity.

    rewrite I. rewrite <- e. symmetry. apply app_removelast_last.





    /\ length a = 2^m /\ length (hd ++ a) = k
    /\ last
  )
    -> (tm_step (S (S n)) =
          (tm_morphism (tm_morphism hd)) ++
    

(*
Seules les puissances paires de 2 (16, 64, etc.) sont des longueurs
de palindromes propres (palindromes piles de cette taille pas
encapsulés dans des plus gros palindromes) :

Positions du centre pour 16 :

In [25]: [ i+32 for i in range(32, 800) if test_proper_palidrome(T
    ...: , i, 64) ]
Out[25]: [96, 160, 352, 416, 480, 544, 608, 672]

In [26]: [ i+8 for i in range(8, 300) if test_proper_palidrome(T,
    ...: i, 16) ]
Out[26]: [24, 40, 88, 104, 120, 136, 152, 168, 216, 232, 280, 296]
In [27]: [ i+2 for i in range(2, 100) if test_proper_palidrome(T,
    ...: i, 4) ]
Out[27]: [6, 10, 22, 26, 30, 34, 38, 42, 54, 58, 70, 74, 86, 90, 94, 98]

Idée de lemme : si k est une position centrale pour un palindrome propre
  de taille 2^j, alors  4*k est une position centrale pour un palindrome
   propre de taille 2^(S (S j))


 *)





(*
Lemma tm_step_palindromic_full : forall (n : nat),
  tm_step (Nat.double (S n)) =
    (tm_step (S (Nat.double n))) ++ rev (tm_step (S (Nat.double n))).
Proof.
  intro n. rewrite tm_step_odd_step. rewrite <- tm_build.
  rewrite Nat.double_S. reflexivity.
Qed.
 *)

(*
Lemma tm_step_palindromic_even_seed :
  forall (n : nat) (hd a tl : list bool),
  tm_step (S n) = hd ++ a ++ (rev a) ++ tl
  -> 0 < length a
  -> (2^n <= length hd) \/ (2^n <= length tl) \/ (length (hd ++a) = 2^n).
Proof.
  intro n. induction n.
  - intros hd a tl. intros H I. destruct a.
    + inversion I.
    + destruct a.
      assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
      rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
      rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
      apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
      destruct hd; destruct tl. right. right. reflexivity.
      right. left. simpl. apply le_n_S. apply le_0_n.
      rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
      contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
      assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
      rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
      rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
      apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
      rewrite app_length in H0. rewrite app_length in H0.
      rewrite app_length in H0. simpl in H0.
      rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
      rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
      rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
  - intros hd a tl. intros H I. rewrite tm_build in H.
    assert (2^S n <= length hd \/ length hd < 2^S n). apply Nat.le_gt_cases.
    assert (2^S n <= length tl \/ length tl < 2^S n). apply Nat.le_gt_cases.
    destruct H0. left. assumption. destruct H1. right. left. assumption.
    right. right.
    assert (2^S n <= length (hd++a) \/ length (hd++a) < 2^S n).
    apply Nat.le_gt_cases. destruct H2. apply Nat.lt_eq_cases in H2.
    destruct H2.
    pose (c := length (hd ++ a) - 2^ S n). (* ce qui dépasse, excès de a *)
    pose (d := skipn ((length a) - c) a). (* on cherche le milieu de tm_step S (S n) *)
    pose (e := d ++ firstn c (rev a)).
    (* TODO e = rev e est-il vraiment utile ??? *)
    assert (e = rev e). (* nouveau palindrome dans la seconde moitié *)
    unfold e. unfold d.
    rewrite firstn_rev. rewrite rev_app_distr. rewrite rev_involutive.
    reflexivity.

    (* montrer que e est dans la seconde moitié, excentré *)
    assert (a = (firstn (length a - c) a) ++ d). unfold d.
    symmetry. apply firstn_skipn.

    rewrite H4 in H. rewrite <- app_assoc in H. rewrite rev_app_distr in H.
    rewrite <- app_assoc in H. rewrite app_assoc in H.

    assert (length hd + length a - 2 ^ S n <= length a).
    rewrite Nat.add_le_mono_r with (p := 2^S n).
    rewrite Nat.sub_add. rewrite Nat.add_comm at 1.
    rewrite <- Nat.add_le_mono_l. apply Nat.lt_le_incl. assumption.
    rewrite <- app_length. apply Nat.lt_le_incl. assumption.

    assert (length (tm_step (S n)) = length (hd ++ firstn (length a - c) a)).
    unfold c. rewrite app_length. rewrite tm_size_power2.
    rewrite firstn_length_le. rewrite app_length.
    rewrite Nat.add_sub_assoc.

    replace (length hd + length a)
      with (length hd + length a - 2^S n + 2^S n) at 1.
    rewrite Nat.add_sub_swap. rewrite <- Nat.add_0_l at 1.
    rewrite Nat.add_cancel_r. symmetry. apply Nat.sub_diag.
    apply Nat.le_refl. rewrite <- Nat.add_sub_swap.
    rewrite Nat.add_sub. reflexivity. apply Nat.lt_le_incl.
    rewrite <- app_length. assumption. assumption.

    apply Nat.le_sub_le_add_r. rewrite <- Nat.add_0_r at 1.
    rewrite <- Nat.add_le_mono_l. apply le_0_n.

    assert (tm_step (S n) = hd ++ firstn (length a - c) a).
    generalize H6. generalize H.
    apply app_eq_length_head. rewrite <- H7 in H.
    apply app_inv_head in H.



    assert (map negb (tm_step (S n)) = e ++ ??? ++ tl). unfold e. unfold d.









  intros n hd a tl. intros H I.
  induction n.
  - right. right. destruct a. inversion I. destruct a.
    assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
    rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
    rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
    apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
    destruct hd; destruct tl. reflexivity. reflexivity.
    rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
    contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
    assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
    rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
    rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
    apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
    rewrite app_length in H0. rewrite app_length in H0.
    rewrite app_length in H0. simpl in H0.
    rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
    rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
    rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
  -
  

 *)

 (* TODO: reprendre tous les lemmes hd ++ a ++ rev a ++ tl
           et trouver un équivalent pour hd ++ a ++ map negb (rev a) ++ tl *)

(*
  TODO: les palindromes de longueur 16 sont centrés autour
   des valeurs de la suite ci-dessous A056196
   TODO: erratum 216 est un centre possible ! (216 = 2^3  3^3)

A056196          Numbers n such that A055229(n) = 2.                                +30
                                                                                      2
 8, 24, 32, 40, 56, 72, 88, 96, 104, 120, 128, 136, 152, 160, 168, 184, 200, 224, 232,
 248, 264, 280, 288, 296, 312, 328, 344, 352, 360, 376, 384, 392, 408, 416, 424, 440,
 456, 472, 480, 488, 504, 512, 520, 536, 544, 552, 568, 584, 600, 608, 616, 632, 640
 (list; graph; refs; listen; history; text; internal format)
 OFFSET      1,1
 COMMENTS    By definition, the largest square divisor and squarefree part of these
             numbers have GCD = 2.

             Different from A036966. E.g., 81 is not here because A055229(81) = 1.

             Numbers of the form 2^(2*k+1) * m, where k >= 1 and m is an odd number
             whose prime factorization contains only exponents that are either 1 or
             even. The asymptotic density of this sequence is (1/12) * Product_{p odd
             prime} (1-1/(p^2*(p+1))) = A065465 / 11 = 0.08013762179319734335... -
             Amiram Eldar, Dec 04 2020, Nov 25 2022
 LINKS       Robert Israel, Table of n, a(n) for n = 1..10000
 EXAMPLE     88 is here because 88 has squarefree part 22, largest square divisor 4,
             and A055229(88) = gcd(22, 4) = 2.




 *)