Update

src/thue_morse.v

@@ -37,6 +37,45 @@ Fixpoint tm_step (n: nat) : list bool :=
    the previous functions are proved below.
 *)
 
+Lemma trailing_zeros :
+  forall n, 0 < n -> exists k j, n = S (Nat.double k) * 2^j.
+Proof.
+  intro n. intro H.
+  assert (exists m, 2^m <= n < 2^(S m)).
+  exists (Nat.log2 n). apply Nat.log2_spec; assumption.
+  destruct H0. generalize dependent n. induction x; intros n H I.
+  - exists 0. exists 0. simpl.
+    destruct n. inversion H. destruct I. destruct n. reflexivity.
+    simpl in H1. rewrite <- Nat.succ_lt_mono in H1.
+    rewrite <- Nat.succ_lt_mono in H1. apply Nat.nlt_0_r in H1.
+    contradiction.
+  - destruct I. apply Nat.div_le_mono with (c := 2) in H0.
+    rewrite Nat.pow_succ_r in H0. rewrite Nat.mul_comm in H0.
+    rewrite Nat.div_mul in H0.
+
+    assert (Nat.Even n \/ Nat.Odd n). apply Nat.Even_or_Odd.
+    destruct H2. assert (U := H2).
+    + apply Nat.Even_double in H2. rewrite Nat.double_twice in H2.
+      rewrite H2 in H1. rewrite Nat.pow_succ_r in H1.
+      rewrite <- Nat.mul_lt_mono_pos_l in H1. rewrite Nat.div2_div in H1.
+      assert (exists k j, n/2 = S (Nat.double k) * 2^j).
+      apply IHx. assert (0 < 2^x). rewrite <- Nat.neq_0_lt_0.
+      apply Nat.pow_nonzero. easy. generalize H0. generalize H3.
+      apply Nat.lt_le_trans. split; assumption.
+      destruct H3. destruct H3. exists x0. exists (S x1).
+      rewrite H2. rewrite Nat.pow_succ_r. symmetry. rewrite Nat.mul_comm.
+      rewrite <- Nat.mul_assoc. rewrite Nat.mul_cancel_l.
+      rewrite Nat.mul_comm. rewrite <- H3. rewrite Nat.div2_div.
+      reflexivity. easy. apply Nat.le_0_l. apply Nat.lt_0_2.
+      apply Nat.le_0_l.
+    + apply Nat.Odd_double in H2.
+      exists (Nat.div2 n). exists 0. rewrite H2 at 1.
+      rewrite Nat.mul_1_r. reflexivity.
+    + easy.
+    + apply Nat.le_0_l.
+    + easy.
+Qed.
+
 Lemma lt_split_bits : forall n m k j,
   0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
 Proof.

src/thue_morse4.v

@@ -160,45 +160,6 @@ Proof.
 Qed.
 
 
-Lemma trailing_zeros :
-  forall n, 0 < n -> exists k j, n = S (Nat.double k) * 2^j.
-Proof.
-  intro n. intro H.
-  assert (exists m, 2^m <= n < 2^(S m)).
-  exists (Nat.log2 n). apply Nat.log2_spec; assumption.
-  destruct H0. generalize dependent n. induction x; intros n H I.
-  - exists 0. exists 0. simpl.
-    destruct n. inversion H. destruct I. destruct n. reflexivity.
-    simpl in H1. rewrite <- Nat.succ_lt_mono in H1.
-    rewrite <- Nat.succ_lt_mono in H1. apply Nat.nlt_0_r in H1.
-    contradiction.
-  - destruct I. apply Nat.div_le_mono with (c := 2) in H0.
-    rewrite Nat.pow_succ_r in H0. rewrite Nat.mul_comm in H0.
-    rewrite Nat.div_mul in H0.
-
-    assert (Nat.Even n \/ Nat.Odd n). apply Nat.Even_or_Odd.
-    destruct H2. assert (U := H2).
-    + apply Nat.Even_double in H2. rewrite Nat.double_twice in H2.
-      rewrite H2 in H1. rewrite Nat.pow_succ_r in H1.
-      rewrite <- Nat.mul_lt_mono_pos_l in H1. rewrite Nat.div2_div in H1.
-      assert (exists k j, n/2 = S (Nat.double k) * 2^j).
-      apply IHx. assert (0 < 2^x). rewrite <- Nat.neq_0_lt_0.
-      apply Nat.pow_nonzero. easy. generalize H0. generalize H3.
-      apply Nat.lt_le_trans. split; assumption.
-      destruct H3. destruct H3. exists x0. exists (S x1).
-      rewrite H2. rewrite Nat.pow_succ_r. symmetry. rewrite Nat.mul_comm.
-      rewrite <- Nat.mul_assoc. rewrite Nat.mul_cancel_l.
-      rewrite Nat.mul_comm. rewrite <- H3. rewrite Nat.div2_div.
-      reflexivity. easy. apply Nat.le_0_l. apply Nat.lt_0_2.
-      apply Nat.le_0_l.
-    + apply Nat.Odd_double in H2.
-      exists (Nat.div2 n). exists 0. rewrite H2 at 1.
-      rewrite Nat.mul_1_r. reflexivity.
-    + easy.
-    + apply Nat.le_0_l.
-    + easy.
-Qed.
-
 
 
 
@@ -206,16 +167,34 @@ Lemma xxx :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> a = rev a
-  -> 11 = 42.
+  -> 0 < length a
+  -> length a <= 4 \/ 11 = 42 \/ 17 = 55.
 Proof.
-  intros n hd a tl. intros H I.
+  intros n hd a tl. intros H I J.
+  destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
+  rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
+  rewrite app_length in H0. rewrite Nat.add_comm in H0.
+  destruct a. inversion J. rewrite <- Nat.add_assoc in H0.
+  rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
+  apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
 
+  assert (exists k j, length a = S (Nat.double k) * 2^j).
+  apply trailing_zeros; assumption. destruct H0. destruct H0.
+  assert (x = 0 \/ x = 1). generalize H0. generalize H.
+  apply tm_step_square_size.
 
+  rewrite I in H at 2.
 
-
-
-tm_step_square_size:
-  forall (n k j : nat) (hd a tl : list bool),
-  tm_step (S n) = hd ++ a ++ a ++ tl ->
-  length a = S (Nat.double k) * 2 ^ j -> k = 0 \/ k = 1
+  destruct H1; rewrite H1 in H0.
+  - rewrite Nat.mul_1_l in H0.
+    assert (length a <= 4 \/ 4 < length a). apply Nat.le_gt_cases.
+    destruct H2. left. assumption.
+    assert (2 < x0). destruct x0. rewrite H0 in H2. inversion H2.
+    inversion H4. destruct x0. rewrite H0 in H2. inversion H2.
+    inversion H4. inversion H6. destruct x0. rewrite H0 in H2.
+    inversion H2. inversion H4. inversion H6. inversion H8. inversion H10.
+    lia.
+    assert (length (hd ++ a) mod 2^(pred (Nat.double (Nat.div2 (S x0)))) = 0).
+    generalize H3. generalize H0. generalize H.
+    apply tm_step_palindrome_power2.