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 (forall x0 x1 y0 y1 : list bool,
    x0 ++ x1 = y0 ++ y1 -> length x0 = length y0 -> x0 = y0).

  intro x0. induction x0. destruct y0. intros. reflexivity.
  intros. inversion H7. destruct y0. intros. inversion H7.
  intros. simpl in H7. apply Nat.succ_inj in H7.
  rewrite <- app_comm_cons in H6.
  rewrite <- app_comm_cons in H6.

  destruct a0; destruct b. inversion H6.
  apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
  assumption. inversion H6. inversion H6. inversion H6.
  apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
  assumption.

  assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
  generalize I. apply H6.
  rewrite H7 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.


  



  (* TODO: voir si une preuve du lemme précédent est plus rapide comme ceci *)


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




 *)