Update

src/thue_morse3.v

@@ -2280,6 +2280,206 @@ Proof.
 Qed.
 
 
+Lemma tm_step_palindrome_mod8 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> 6 < length a
+  -> length (hd ++ a) mod 8 = 0.
+Proof.
+  intros n hd a tl. intros H I. assert (Z := H).
+
+  assert (X : 3 < n). rewrite Nat.pow_lt_mono_r_iff with (a := 2).
+  simpl. rewrite <- tm_size_power2. rewrite H.
+  rewrite app_length. rewrite Nat.add_comm. rewrite app_length.
+  rewrite app_length. rewrite Nat.add_assoc.
+  assert (6+6 < length a + length (rev a)). rewrite rev_length.
+  apply Nat.add_lt_mono; assumption.
+  assert (length a + length (rev a)
+      <= length a + length (rev a) + length tl + length hd).
+  rewrite <- Nat.add_assoc. apply Nat.le_add_r.
+  assert (6+6 < length a + length (rev a) + length tl + length hd).
+  generalize H1. generalize H0. apply Nat.lt_le_trans.
+  replace (6+6) with 12 in H2.
+  apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2.
+  apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2. assumption.
+  reflexivity. apply Nat.lt_1_2.
+
+  assert (N: length (hd ++ a) mod 4 = 0). generalize I. generalize H.
+  apply tm_step_palindromic_length_12.
+
+  assert (O: length (hd++a) mod 8 = 0 \/ length (hd++a) mod 8 = 4).
+  assert (length (hd ++ a) mod (4*2)
+  = (length (hd ++ a) mod 4 + 4 * (length (hd ++ a) / 4 mod 2))).
+  apply Nat.mod_mul_r. easy. easy.
+  rewrite N in H0. rewrite <- Nat.bit0_mod in H0.
+  replace (4*2) with 8 in H0. rewrite Nat.add_0_l in H0.
+  destruct (Nat.testbit (length (hd ++ a) / 4)).
+  right. apply H0. left. apply H0. reflexivity.
+
+  assert (J: firstn (length a - 7) a ++ skipn (length a - 7) a = a).
+  apply firstn_skipn. rewrite <- J in H. rewrite rev_app_distr in H.
+  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
+
+  assert (K: exists x, skipn (length a - 7) a
+    = [negb x; negb x; x; negb x; x; x; negb x]).
+  assert (length (skipn (length a - 7) a) = 7). rewrite skipn_length.
+  assert ((length a - 7) - (length a - 7) = 0). apply Nat.sub_diag.
+  rewrite <- Nat.add_cancel_r with (p := 7) in H0.
+  rewrite <- Nat.add_sub_swap in H0. rewrite <- Nat.add_sub_swap in H0.
+  rewrite Nat.add_sub in H0. assumption. apply Nat.le_succ_l. assumption.
+  apply Nat.le_refl. generalize H0. rewrite app_assoc in H. generalize H.
+  apply tm_step_palindrome_7_destruct.
+  destruct K. rewrite H0 in H.
+
+  destruct O as [O | O]. assumption.
+  assert (nth_error (tm_step 3) 3 = nth_error (tm_step 3) 4
+      <-> nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 3)
+        = nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 4)).
+  apply tm_step_repeating_patterns. simpl. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. 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.
+
+  rewrite Nat.mul_lt_mono_pos_l with (p := 8).
+  rewrite Nat.add_lt_mono_r with (p := length (hd ++ a) mod 8).
+  rewrite <- Nat.div_mod_eq. rewrite O.
+
+  replace 8 with (2*2*2).
+  rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
+  rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
+  rewrite <- Nat.pow_succ_r. rewrite <- Nat.sub_succ_l.
+  rewrite <- Nat.sub_succ_l. rewrite <- Nat.sub_succ_l.
+  replace (S (S (S n))) with (n + 3). rewrite Nat.add_sub.
+
+  assert (length (hd++a) <= length (tm_step n)).
+  rewrite Z. rewrite app_assoc.
+  replace (length ((hd ++ a) ++ rev a ++ tl))
+    with (length (hd ++ a) + length ((rev a) ++ tl)).
+  apply Nat.le_add_r. symmetry. rewrite app_length. reflexivity.
+
+  assert (length (tm_step n) < 2^n + 4). rewrite tm_size_power2.
+  apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+
+  generalize H2. generalize H1. apply Nat.le_lt_trans.
+  rewrite Nat.add_comm. reflexivity.
+  apply le_S. apply le_S. apply Nat.lt_le_incl. assumption.
+  apply le_S. apply Nat.lt_le_incl. assumption.
+  apply Nat.lt_le_incl. assumption.
+  apply le_S. apply le_S. apply Nat.lt_le_incl.
+  rewrite Nat.add_lt_mono_r with (p := 3).
+  rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
+  apply Nat.lt_le_incl. assumption.
+  apply le_S. apply Nat.lt_le_incl.
+  rewrite Nat.add_lt_mono_r with (p := 3).
+  rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
+  apply Nat.lt_le_incl. assumption.
+  apply Nat.lt_le_incl.
+  rewrite Nat.add_lt_mono_r with (p := 3).
+  rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
+  apply Nat.lt_le_incl. assumption.
+  reflexivity. apply Nat.lt_0_succ.
+
+  replace (3 + (n-3)) with n in H1.
+
+  assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 3) = Some (negb x)).
+  rewrite H. rewrite app_assoc. rewrite nth_error_app2.
+
+  rewrite Nat.mul_comm. replace (2^3) with 8.
+  replace 3 with (length (hd++a) mod 8 - 1) at 4.
+  rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq.
+  rewrite app_length. rewrite app_length.
+  rewrite firstn_length_le.
+  rewrite <- Nat.add_sub_assoc.
+  replace (length a - 1) with (6 + length a - 7).
+  rewrite Nat.add_sub_assoc. rewrite Nat.add_assoc.
+  rewrite <- Nat.add_sub_assoc.
+  replace (length hd + 6) with (6 + length hd).
+  rewrite <- Nat.add_assoc. rewrite Nat.add_sub. simpl. reflexivity.
+  rewrite Nat.add_comm. reflexivity. apply Nat.le_succ_l. assumption.
+  rewrite Nat.le_succ_l. rewrite <- Nat.add_0_l at 1.
+  apply Nat.add_lt_mono. apply Nat.lt_0_succ. assumption.
+
+  rewrite Nat.add_comm.
+  rewrite Nat.add_sub_swap. replace 6 with (7 - 1) at 2.
+  rewrite <- Nat.add_sub_swap.
+  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
+  rewrite Nat.add_sub. reflexivity.
+
+  rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. assumption.
+
+  apply Nat.le_succ_l. apply Nat.lt_0_succ.
+  apply Nat.le_succ_l. assumption. reflexivity.
+  apply Nat.le_succ_l. assumption.
+
+  rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. assumption.
+
+  apply Nat.le_sub_l. rewrite O.
+  apply Nat.le_succ_l. apply Nat.lt_0_succ.
+  rewrite O. reflexivity. reflexivity.
+
+  rewrite Nat.mul_comm. replace (2^3) with 8.
+  replace 3 with (length (hd++a) mod 8 - 1) at 4.
+  rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq.
+  rewrite app_length. rewrite app_length.
+  rewrite <- Nat.add_sub_assoc. rewrite <- Nat.add_le_mono_l.
+  rewrite firstn_length_le.
+  apply Nat.sub_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ.
+  rewrite <- Nat.sub_0_r.
+  apply Nat.sub_le_mono_l. apply le_0_n.
+
+  rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
+  apply Nat.lt_succ_l in I. assumption.
+
+  rewrite O. apply Nat.le_succ_l. apply Nat.lt_0_succ.
+  rewrite O. reflexivity. reflexivity.
+
+  assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 4) = Some (negb x)).
+  rewrite H. rewrite app_assoc. rewrite app_assoc. rewrite app_assoc.
+  rewrite nth_error_app1.
+
+  rewrite Nat.mul_comm. replace (2^3) with 8.
+  replace 4 with (length (hd++a) mod 8) at 4.
+  rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1.
+  rewrite nth_error_app2. rewrite <- app_assoc. rewrite firstn_skipn.
+  rewrite Nat.sub_diag. reflexivity.
+  rewrite <- app_assoc. rewrite firstn_skipn. apply Nat.le_refl.
+
+  reflexivity.
+
+
+  rewrite Nat.mul_comm. replace (2^3) with 8.
+  replace 4 with (length (hd++a) mod 8) at 3.
+  rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1.
+  replace ((hd ++ firstn (length a - 7) a) ++ skipn (length a - 7) a)
+    with (hd ++ firstn (length a - 7) a ++ skipn (length a - 7) a).
+  rewrite firstn_skipn.
+  replace (length ((hd ++ a) ++ rev [negb x; negb x; x; negb x; x; x; negb x]))
+    with (length (hd ++ a)
+      + length (rev [negb x; negb x; x; negb x; x; x; negb x])).
+  apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+  rewrite app_length. rewrite app_length. rewrite app_length. reflexivity.
+  rewrite <- app_assoc. reflexivity. reflexivity.
+
+  rewrite H2 in H1. rewrite H3 in H1. simpl in H1.
+  inversion H1. contradiction H4.
+
+
+
+
+
+
+
+
 Lemma tm_step_palindrome_8_mod8 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl