diff --git a/src/thue_morse4.v b/src/thue_morse4.v index f9f2552..5d2cd8a 100644 --- a/src/thue_morse4.v +++ b/src/thue_morse4.v @@ -124,8 +124,6 @@ Proof. Qed. - - Theorem tm_step_palindrome_power2_inverse' : forall (m n k : nat) (hd tl : list bool), tm_step n = hd ++ tl @@ -161,3 +159,63 @@ Proof. apply tm_step_palindrome_power2_inverse. 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. + + + + +Lemma xxx : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl + -> a = rev a + -> 11 = 42. +Proof. + intros n hd a tl. intros H I. + + + + + +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 +