Update

src/thue_morse2.v

@@ -327,7 +327,6 @@ Proof.
 Qed.
 
 
-
 (**
    New following lemmas and theorems are related to the size
    of squares in the Thue-Morse sequence, namely lengths of
@@ -605,6 +604,148 @@ Proof.
     generalize H2. apply IHj. easy.
 Qed.
 
+(**
+   This section contains lemmas and theorems related to the length of the
+   prefix being odd or even in front of a squared pattern.
+*)
+
+Lemma tm_step_odd_prefix_square_1 : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 1 -> even (length hd) = false.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
+  apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
+  - assert (K: count_occ Bool.bool_dec hd true
+                 = count_occ Bool.bool_dec hd false).
+    generalize H0. generalize H. apply tm_step_count_occ.
+    assert (L: even (length (hd ++ a ++ a)) = true).
+    rewrite app_length. rewrite app_length. rewrite I.
+    rewrite Nat.even_add_even. assumption. rewrite Nat.add_1_r.
+    apply Nat.EvenT_Even. apply Nat.even_EvenT. easy.
+    assert (M: count_occ Bool.bool_dec (hd ++ a ++ a) true
+                  = count_occ Bool.bool_dec (hd ++ a ++ a) false).
+    generalize L. generalize H.
+    replace (hd ++ a ++ a ++ tl) with ((hd ++ a ++ a) ++ tl).
+    apply tm_step_count_occ.
+    rewrite <- app_assoc. apply app_inv_head_iff.
+    rewrite <- app_assoc. reflexivity.
+    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. destruct a.
+    + inversion I.
+    + destruct b; simpl in I; apply Nat.succ_inj in I;
+      rewrite length_zero_iff_nil in I; rewrite I in M;
+      simpl in M; inversion M.
+  - rewrite <- Nat.negb_odd. rewrite H0. reflexivity.
+Qed.
+
+Lemma tm_step_odd_prefix_square_3 : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 3 -> even (length hd) = false.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
+  apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
+  assert (Z: a = [true;false;true] \/ a = [false;true;false]).
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a.
+  - destruct b; destruct b0; destruct b1.
+    + replace ([true;true;true] ++ [true;true;true] ++ tl)
+      with ([true;true] ++ [true] ++ [true;true] ++ [true] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      reflexivity.
+    + replace ([true;true;false] ++ [true;true;false] ++ tl)
+      with ([true;true] ++ [false] ++ [true;true] ++ [false] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      reflexivity.
+    + left. reflexivity.
+    + replace (hd ++ [true;false;false] ++ [true;false;false] ++ tl)
+      with ((hd ++ [true]) ++ [false; false] ++ [true] ++ [false;false] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      rewrite <- app_assoc. reflexivity.
+    + replace (hd ++ [false;true;true] ++ [false;true;true] ++ tl)
+      with ((hd ++ [false]) ++ [true; true] ++ [false] ++ [true;true] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      rewrite <- app_assoc. reflexivity.
+    + right. reflexivity.
+    + replace ([false;false;true] ++ [false;false;true] ++ tl)
+      with ([false;false] ++ [true] ++ [false;false] ++ [true] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      reflexivity.
+    + replace ([false;false;false] ++ [false;false;false] ++ tl)
+      with ([false;false] ++ [false] ++ [false;false] ++ [false] ++ tl) in H.
+      apply tm_step_consecutive_identical in H. inversion H.
+      reflexivity.
+  - inversion I.
+  - assert (K: count_occ Bool.bool_dec hd true
+                 = count_occ Bool.bool_dec hd false).
+    generalize H0. generalize H. apply tm_step_count_occ.
+    destruct Z; rewrite H1 in H.
+    replace (hd ++ [true;false;true] ++ [true;false;true] ++ tl)
+      with ((hd ++ [true;false;true;true]) ++ [false;true] ++ tl) in H.
+    assert (even (length (hd ++ [true;false;true;true])) = true).
+    rewrite app_length. rewrite Nat.even_add. rewrite H0. reflexivity.
+    assert (M: count_occ Bool.bool_dec (hd ++ [true;false;true;true]) true
+                  = count_occ Bool.bool_dec (hd ++ [true;false;true;true]) false).
+    generalize H2. 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. inversion M.
+    rewrite <- app_assoc. reflexivity.
+    replace (hd ++ [false;true;false] ++ [false;true;false] ++ tl)
+      with ((hd ++ [false;true;false;false]) ++ [true;false] ++ tl) in H.
+    assert (even (length (hd ++ [false;true;false;false])) = true).
+    rewrite app_length. rewrite Nat.even_add. rewrite H0. reflexivity.
+    assert (M: count_occ Bool.bool_dec (hd ++ [false;true;false;false]) true
+                  = count_occ Bool.bool_dec (hd ++ [false;true;false;false]) false).
+    generalize H2. 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. inversion M.
+    rewrite <- app_assoc. reflexivity.
+  - rewrite <- Nat.negb_odd. rewrite H0. reflexivity.
+Qed.
+
+Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> odd (length a) = true -> even (length hd) = false.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (length a < 4).
+  generalize I. generalize H. apply tm_step_odd_square.
+  destruct a. inversion I.
+  destruct a.
+  apply tm_step_odd_prefix_square_1 with (n := n) (a := [b]) (tl := tl).
+  assumption. reflexivity.
+  destruct a. inversion I.
+  destruct a.
+  apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl).
+  assumption. reflexivity.
+  simpl in H0.
+  rewrite <- Nat.succ_lt_mono in H0.
+  rewrite <- Nat.succ_lt_mono in H0.
+  rewrite <- Nat.succ_lt_mono in H0.
+  rewrite <- Nat.succ_lt_mono in H0.
+  apply Nat.nlt_0_r in H0. contradiction H0.
+Qed.
+ 
+
+
+
+
+
+
+
+
+Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> 0 < length a -> even (length (hd ++ a)) = true.
+Proof.
+  intros n hd a tl. intros H I.
+
+  rewrite app_length. rewrite Nat.even_add.
+  assert (J: Nat.even (length a) || Nat.odd (length a) = true).
+  apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
+  - rewrite H0.