Update

src/thue_morse3.v

@@ -1479,65 +1479,133 @@ Qed.
 
 
 
+Lemma tm_step_palindromic_even_morphism2 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> length a > 6
+  -> (length a) mod 4 = 0
+  -> 11 = 42.
+Proof.
+  intros n hd a tl. intros H W J0.
 
+  assert (Z: 0 < length a).
+  apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
+  apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
+  assumption.
 
+  (* proof that n <> 0 *)
+  destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
+  apply Nat.le_refl.
+  rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0.
+  rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0. simpl in H0.
+  apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0.
+  rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0.
+  assert (K: 1 <= length a + (length tl + length hd)).
+  rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption.
+  rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0.
+  rewrite H0 in Z. inversion Z.
 
+  assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
+  generalize H. apply tm_step_palindromic_length_12_prefix.
 
+  assert (EVEN: forall m, m mod 4 = 0 -> even m = true).
+  intro m. intro U. rewrite <- Nat.div_exact in U.
+  rewrite U. rewrite Nat.even_mul. reflexivity. easy.
 
-  assert (tm_step (S n) = tm_morphism
-      (firstn (Nat.div2 (length hd)) (tm_step n) ++
-       firstn (Nat.div2 (length a))
-         (skipn (Nat.div2 (length hd)) (tm_step n)) ++
-       firstn (Nat.div2 (length (rev a)))
-         (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
-       skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) (tm_step n))).
-  assert (K : even (length (rev a)) = true).
-  rewrite rev_length. assumption.
-  generalize K. generalize J. generalize H1. generalize H.
-  apply tm_step_morphism4. rewrite rev_length in H2.
+  assert (J: even (length a) = true).
+  apply EVEN in J0. assumption.
 
-  rewrite <- pred_Sn.
-
-
-
-
-
-
-
-  assert (even (length (hd ++ a)) = true). generalize I. generalize H.
+  assert (even (length (hd ++ a)) = true). generalize Z. generalize H.
   apply tm_step_palindromic_even_center.
 
-  assert (even (length hd) = true). rewrite app_length in H0.
+  assert (I: even (length hd) = true). rewrite app_length in H0.
   rewrite Nat.even_add in H0. rewrite J in H0.
   destruct (even (length hd)). reflexivity. inversion H0.
 
-  rewrite <- tm_step_lemma in H.
+  assert (K: even (length (rev a)) = true). rewrite rev_length. assumption.
+
+  rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
+
+  assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
+                                  (tm_step n))).
+  generalize H0. generalize H. apply tm_morphism_app2.
+
+  rewrite <- app_assoc in H. symmetry in H1.
+  assert (even (length (hd ++ a ++ (rev a))) = true).
+  rewrite app_length. rewrite Nat.even_add. rewrite I.
+  rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
+  reflexivity.
+
+  assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a))))
+                         (tm_step n))).
+  replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H.
+  generalize H2. generalize H. apply tm_morphism_app3.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
 
   assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
-  generalize H1. generalize H. apply tm_morphism_app2.
+  generalize I. generalize H. apply tm_morphism_app2.
 
-  assert (a ++ (rev a) ++ tl
-    = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
-  generalize H1. generalize H. apply tm_morphism_app3. symmetry in H3.
+  assert (a = tm_morphism (skipn (Nat.div2 (length hd))
+           (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
+  generalize I. generalize H1. apply tm_morphism_app3.
 
-  assert (a = tm_morphism (firstn (Nat.div2 (length a))
-         (skipn (Nat.div2 (length hd)) (tm_step n)))).
-  generalize J. generalize H3. apply tm_morphism_app2.
+  rewrite skipn_firstn_comm in H5. rewrite app_length in H5.
 
-  assert (tl = tm_morphism (skipn (Nat.div2 (length (a ++ (rev a))))
-         (skipn (Nat.div2 (length hd)) (tm_step n)))).
-  assert (even (length (a ++ (rev a))) = true). rewrite app_length.
-  rewrite rev_length. rewrite Nat.even_add. rewrite J. reflexivity.
-  generalize H5. rewrite app_assoc in H3. generalize H3.
-  apply tm_morphism_app3.
+  replace (Nat.div2 (length hd + length a))
+    with ((length hd) / 2 + Nat.div2 (length a)) in H5.
+  rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5.
+  rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5.
 
-  rewrite H2 in H. rewrite H4 in H. rewrite tm_morphism_rev in H.
-  rewrite H5 in H. rewrite <- tm_morphism_app in H.
+  rewrite H4 in H. rewrite H5 in H. rewrite H3 in H.
+  rewrite tm_morphism_rev in H.
   rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H.
+
+  rewrite app_length in H. rewrite app_length in H. rewrite rev_length in H.
+  replace (length a + length a) with ((length a)*2) in H.
+  replace (Nat.div2 (length hd + length a * 2))
+    with ((length hd + length a * 2) / 2) in H.
+  rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
+
+  pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)).
+  pose (a' := firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd))
+            (tm_step n))).
+  pose (tl' := skipn (Nat.div2 (length hd) + length a) (tm_step n)).
+  fold hd' in H. fold a' in H. fold tl' in H.
+
+  assert (EVEN2: forall m, m mod 4 = 0 -> even (Nat.div2 m) = true).
+  intro m. intro U. rewrite <- Nat.div_exact in U.
+  rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc.
+  rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy.
+
+  assert (I': even (length hd') = true).
+  unfold hd'. rewrite firstn_length_le. apply EVEN2. assumption.
+
+
+
+
+
+
+  assumption. easy.
+  rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl.
+  rewrite Nat.add_0_r. reflexivity.
+
+  apply Nat.le_refl.
+  rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
+  rewrite Nat.mul_comm.
+
+  rewrite Nat.div2_odd with (a := length a) at 2.
+  rewrite <- Nat.negb_even. rewrite J. simpl.
+  rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy.
+Qed.
+
+
+
+
+
+
+
 
-  rewrite app_length in H. rewrite rev_length in H.
-  replace (Nat.div2 (length a + length a)) with (length a) in H.
-  rewrite <- pred_Sn.