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.


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.




 *)