Update

src/thue_morse3.v

@@ -0,0 +1,114 @@
+(** * 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 <> 5.
+Proof.
+  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.
+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.
+  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 tm_step_palindromic_odd. 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 *)
+
+