coqbooks/src/thue_morse3.v

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

   TODO
*)

Require Import thue_morse.
Require Import thue_morse2.

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

Import ListNotations.


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

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.

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


    re






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




 *)