Update

src/thue_morse3.v

@@ -110,5 +110,97 @@ Proof.
   (* 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 tm_step_palindromic_odd. rewrite H4 in H7. contradiction H7.
+  reflexivity.
+Qed.