(** * The Thue-Morse sequence (part 4) TODO *) Require Import thue_morse. Require Import thue_morse2. Require Import thue_morse3. Require Import Coq.Lists.List. Require Import PeanoNat. Require Import Nat. Require Import Bool. Require Import Arith. Require Import Lia. Import ListNotations. Theorem tm_step_palindrome_power2_inverse : forall (m n k : nat) (hd tl : list bool), tm_step n = hd ++ tl -> length hd = S (Nat.double k) * 2^m -> odd m = true -> tl <> nil -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl). Proof. intros m n k hd tl. intros H I J K. assert (L: 2^m <= length hd). rewrite I. lia. assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)). rewrite H. reflexivity. rewrite tm_size_power2 in H0. rewrite app_length in H0. (* rewrite I in H0. *) assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H1. apply Nat.pow_le_mono_r with (a := 2) in H1. assert (2^n <= length hd). generalize L. generalize H1. apply Nat.le_trans. rewrite H0 in H2. rewrite <- Nat.add_0_r in H2. rewrite <- Nat.add_le_mono_l in H2. destruct tl. contradiction K. reflexivity. simpl in H2. apply Nat.nle_succ_0 in H2. contradiction. easy. assumption. assert (N: length (tm_step n) mod 2^m = 0). rewrite tm_size_power2. apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite <- Nat.pow_sub_r. rewrite <- Nat.pow_add_r. rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. apply Nat.lt_le_incl. assumption. easy. apply Nat.lt_le_incl. assumption. assert (O: length hd mod 2^m = 0). apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite I. rewrite Nat.div_mul. rewrite Nat.mul_comm. reflexivity. apply Nat.pow_nonzero. easy. assert (P: length tl mod 2 ^ m = 0). rewrite H in N. rewrite app_length in N. rewrite <- Nat.add_mod_idemp_l in N. rewrite O in N. assumption. apply Nat.pow_nonzero. easy. assert (Q: 2^m <= length tl). apply Nat.div_exact in P. rewrite P. destruct (length tl / 2^m). rewrite Nat.mul_0_r in P. apply length_zero_iff_nil in P. rewrite P in K. contradiction K. reflexivity. rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.pow_nonzero. easy. replace hd with (firstn (length hd - 2^m) hd ++ skipn (length hd - 2^m) hd) in H. replace tl with (firstn (2^m) tl ++ skipn (2^m) tl) in H. rewrite <- app_assoc in H. replace ( skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl ++ skipn (2 ^ m) tl ) with ( (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) ++ skipn (2 ^ m) tl ) in H. assert (length (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) = 2^(S m)). rewrite app_length. rewrite skipn_length. rewrite firstn_length_le. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. simpl. rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption. assumption. assert (length (firstn (length hd - 2^m) hd) mod 2^(S m) = 0). rewrite firstn_length_le. replace (2^m) with (2^m * 1). rewrite I. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_l. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. rewrite Nat.double_twice. rewrite Nat.mul_assoc. replace (2^m * 2) with (2^(S m)). rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity. apply Nat.pow_nonzero. easy. rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity. apply Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l. assert ( skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m) \/ skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = map negb (tm_step (S m))). generalize H1. generalize H0. generalize H. apply tm_step_repeating_patterns2. apply tm_step_palindromic_full in J. destruct H2; rewrite J in H2. - assert (skipn (length hd - 2^m) hd = tm_step m). apply app_eq_length_head in H2. assumption. rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite tm_size_power2. reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. assert (firstn (2^m) tl = rev (tm_step m)). rewrite H3 in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity. rewrite H4. rewrite rev_involutive. reflexivity. - assert (skipn (length hd - 2^m) hd = map negb (tm_step m)). rewrite map_app in H2. apply app_eq_length_head in H2. assumption. rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite map_length. rewrite tm_size_power2. reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. assert (firstn (2^m) tl = map negb (rev (tm_step m))). rewrite H3 in H2. rewrite map_app in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity. rewrite H4. rewrite map_rev. rewrite rev_involutive. reflexivity. - rewrite <- app_assoc. reflexivity. - rewrite firstn_skipn. reflexivity. - rewrite firstn_skipn. reflexivity. Qed. Theorem tm_step_palindrome_power2_inverse' : forall (m n k : nat) (hd tl : list bool), tm_step n = hd ++ tl -> length hd = S (Nat.double k) * 2^m -> odd m = true -> 0 < k -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl). Proof. intros m n k hd tl. intros H I J L. assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec. destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H. rewrite <- H in I. rewrite tm_size_power2 in I. assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0. apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0. rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0. rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0. rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0. rewrite H0 in L. inversion L. easy. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy. replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I. rewrite Nat.mul_cancel_r in I. assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0. apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0. rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1. rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1. inversion H1. apply Nat.pow_nonzero. easy. lia. generalize K. generalize J. generalize I. generalize H. 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