diff --git a/src/thue_morse.v b/src/thue_morse.v index 48a0f12..ea39049 100644 --- a/src/thue_morse.v +++ b/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. diff --git a/src/thue_morse4.v b/src/thue_morse4.v index 5d2cd8a..f93f223 100644 --- a/src/thue_morse4.v +++ b/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.