Update

src/thue_morse2.v

@@ -88,6 +88,7 @@ Qed.
 (**
    The following lemmas and theorems are all related to
    squares of odd length in the Thue-Morse sequence.
+   All squared factors of odd length have length 1 or 3.
 *)
 
 Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
@@ -331,6 +332,131 @@ Qed.
    New section
 *)
 
+Lemma tm_step_shift_odd_prefix_even_squares :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> even (length a) = true
+  -> odd (length hd) = true
+  -> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
+          /\ even (length hd') = true /\ length a = length b.
+Proof.
+  intros n hd a tl. intros H I J.
+
+  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
+  destruct W. rewrite e in J. simpl in J. rewrite Nat.odd_0 in J.
+  inversion J.
+
+  assert (Z: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
+  destruct Z.
+  exists (removelast hd). exists nil. exists ((last hd true)::nil++tl).
+  split. rewrite app_nil_l. rewrite app_nil_l. rewrite app_nil_l.
+  replace ((last hd true)::tl) with ([last hd true] ++ tl).
+  rewrite app_assoc. rewrite <- app_removelast_last.
+  rewrite H. rewrite e. rewrite app_nil_l. rewrite app_nil_l. reflexivity.
+  assumption.
+  split. rewrite app_removelast_last with (l := hd) (d := last hd true) in J.
+  rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
+  rewrite J. split. reflexivity. rewrite e. reflexivity. assumption.
+
+  rewrite app_removelast_last with (l := hd) (d := true) in H.
+  rewrite app_removelast_last with (l := a) (d := true) in H.
+  rewrite app_assoc_reverse in H.
+  rewrite app_removelast_last with (l := hd) (d := true) in J.
+  rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
+  rewrite app_removelast_last with (l := a) (d := true) in I.
+  rewrite app_length in I. rewrite Nat.add_1_r in I.
+  exists (removelast hd).
+  rewrite app_assoc_reverse in H. rewrite app_assoc_reverse in H.
+  replace (
+    removelast hd ++ [last hd true] ++
+    removelast a ++ [last a true] ++ removelast a ++ [last a true] ++ tl)
+    with (
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
+    ([last a true] ++ tl)) in H.
+  assert (K: count_occ Bool.bool_dec (removelast hd) true
+           = count_occ Bool.bool_dec (removelast hd) false).
+  generalize J. generalize H. apply tm_step_count_occ.
+  assert (L: count_occ Bool.bool_dec (
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) true
+    = count_occ Bool.bool_dec (
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) false).
+  assert (M: even (length (
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a))) = true).
+  rewrite app_length. rewrite Nat.even_add_even. apply J.
+  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
+  rewrite Nat.even_add_even. rewrite app_length.
+  rewrite Nat.add_1_l. assumption.
+  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
+  rewrite Nat.add_1_l. assumption.
+  generalize M.
+  replace (
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
+    ([last a true] ++ tl))
+    with ((
+    removelast hd ++
+    ([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) ++
+    ([last a true] ++ tl)) in H.
+  generalize H. apply tm_step_count_occ.
+
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+
+  assert (M: count_occ Bool.bool_dec (
+    removelast hd ++
+    ([last hd true] ++ removelast a)) true
+    = count_occ Bool.bool_dec (
+    removelast hd ++
+    ([last hd true] ++ removelast a)) false).
+  assert (N: even (length (
+    removelast hd ++
+    ([last hd true] ++ removelast a))) = true).
+  rewrite app_length. rewrite Nat.even_add_even. assumption.
+  rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
+  rewrite Nat.add_1_l. assumption.
+  generalize N.
+  rewrite app_assoc in H. generalize H. apply tm_step_count_occ.
+
+  rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M.
+  rewrite K in M. rewrite Nat.add_cancel_l in M.
+
+  rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
+  rewrite K in L. rewrite Nat.add_cancel_l in L.
+  rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
+  rewrite M in L. rewrite Nat.add_cancel_l in L.
+
+  assert (O: forall (m: nat), m <> S (S m)).
+  induction m. easy. apply not_eq_S. assumption.
+
+  assert (N: last hd true = last a true).
+  destruct (last hd true); destruct (last a true).
+  reflexivity.
+  rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
+  rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
+  rewrite L in M. apply O in M. contradiction M.
+  rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
+  rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
+  rewrite <- L in M. symmetry in M. apply O in M. contradiction M.
+  reflexivity.
+
+  rewrite N in H. exists ([last a true] ++ removelast a).
+  exists ([last a true] ++ tl). rewrite H.
+
+  split. reflexivity.
+  split. assumption.
+  rewrite app_length. rewrite app_removelast_last with (l := a) (d := true).
+  rewrite app_length. rewrite last_last. rewrite removelast_app.
+  rewrite Nat.add_1_r. rewrite app_nil_r. reflexivity. easy.
+
+  assumption.
+  rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
+  assumption. assumption. assumption. assumption.
+Qed.
+