diff --git a/src/thue_morse3.v b/src/thue_morse3.v index fefef68..86b235c 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2280,6 +2280,206 @@ Proof. Qed. +Lemma tm_step_palindrome_mod8 : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length (hd ++ a) mod 8 = 0. +Proof. + intros n hd a tl. intros H I. assert (Z := H). + + assert (X : 3 < n). rewrite Nat.pow_lt_mono_r_iff with (a := 2). + simpl. rewrite <- tm_size_power2. rewrite H. + rewrite app_length. rewrite Nat.add_comm. rewrite app_length. + rewrite app_length. rewrite Nat.add_assoc. + assert (6+6 < length a + length (rev a)). rewrite rev_length. + apply Nat.add_lt_mono; assumption. + assert (length a + length (rev a) + <= length a + length (rev a) + length tl + length hd). + rewrite <- Nat.add_assoc. apply Nat.le_add_r. + assert (6+6 < length a + length (rev a) + length tl + length hd). + generalize H1. generalize H0. apply Nat.lt_le_trans. + replace (6+6) with 12 in H2. + apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2. + apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2. assumption. + reflexivity. apply Nat.lt_1_2. + + assert (N: length (hd ++ a) mod 4 = 0). generalize I. generalize H. + apply tm_step_palindromic_length_12. + + assert (O: length (hd++a) mod 8 = 0 \/ length (hd++a) mod 8 = 4). + assert (length (hd ++ a) mod (4*2) + = (length (hd ++ a) mod 4 + 4 * (length (hd ++ a) / 4 mod 2))). + apply Nat.mod_mul_r. easy. easy. + rewrite N in H0. rewrite <- Nat.bit0_mod in H0. + replace (4*2) with 8 in H0. rewrite Nat.add_0_l in H0. + destruct (Nat.testbit (length (hd ++ a) / 4)). + right. apply H0. left. apply H0. reflexivity. + + assert (J: firstn (length a - 7) a ++ skipn (length a - 7) a = a). + apply firstn_skipn. rewrite <- J in H. rewrite rev_app_distr in H. + rewrite <- app_assoc in H. rewrite <- app_assoc in H. + + assert (K: exists x, skipn (length a - 7) a + = [negb x; negb x; x; negb x; x; x; negb x]). + assert (length (skipn (length a - 7) a) = 7). rewrite skipn_length. + assert ((length a - 7) - (length a - 7) = 0). apply Nat.sub_diag. + rewrite <- Nat.add_cancel_r with (p := 7) in H0. + rewrite <- Nat.add_sub_swap in H0. rewrite <- Nat.add_sub_swap in H0. + rewrite Nat.add_sub in H0. assumption. apply Nat.le_succ_l. assumption. + apply Nat.le_refl. generalize H0. rewrite app_assoc in H. generalize H. + apply tm_step_palindrome_7_destruct. + destruct K. rewrite H0 in H. + + destruct O as [O | O]. assumption. + assert (nth_error (tm_step 3) 3 = nth_error (tm_step 3) 4 + <-> nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 3) + = nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 4)). + apply tm_step_repeating_patterns. simpl. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + apply Nat.lt_0_succ. simpl. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + apply Nat.lt_0_succ. + + rewrite Nat.mul_lt_mono_pos_l with (p := 8). + rewrite Nat.add_lt_mono_r with (p := length (hd ++ a) mod 8). + rewrite <- Nat.div_mod_eq. rewrite O. + + replace 8 with (2*2*2). + rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. + rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. + rewrite <- Nat.pow_succ_r. rewrite <- Nat.sub_succ_l. + rewrite <- Nat.sub_succ_l. rewrite <- Nat.sub_succ_l. + replace (S (S (S n))) with (n + 3). rewrite Nat.add_sub. + + assert (length (hd++a) <= length (tm_step n)). + rewrite Z. rewrite app_assoc. + replace (length ((hd ++ a) ++ rev a ++ tl)) + with (length (hd ++ a) + length ((rev a) ++ tl)). + apply Nat.le_add_r. symmetry. rewrite app_length. reflexivity. + + assert (length (tm_step n) < 2^n + 4). rewrite tm_size_power2. + apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. + + generalize H2. generalize H1. apply Nat.le_lt_trans. + rewrite Nat.add_comm. reflexivity. + apply le_S. apply le_S. apply Nat.lt_le_incl. assumption. + apply le_S. apply Nat.lt_le_incl. assumption. + apply Nat.lt_le_incl. assumption. + apply le_S. apply le_S. apply Nat.lt_le_incl. + rewrite Nat.add_lt_mono_r with (p := 3). + rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption. + apply Nat.lt_le_incl. assumption. + apply le_S. apply Nat.lt_le_incl. + rewrite Nat.add_lt_mono_r with (p := 3). + rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption. + apply Nat.lt_le_incl. assumption. + apply Nat.lt_le_incl. + rewrite Nat.add_lt_mono_r with (p := 3). + rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption. + apply Nat.lt_le_incl. assumption. + reflexivity. apply Nat.lt_0_succ. + + replace (3 + (n-3)) with n in H1. + + assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 3) = Some (negb x)). + rewrite H. rewrite app_assoc. rewrite nth_error_app2. + + rewrite Nat.mul_comm. replace (2^3) with 8. + replace 3 with (length (hd++a) mod 8 - 1) at 4. + rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq. + rewrite app_length. rewrite app_length. + rewrite firstn_length_le. + rewrite <- Nat.add_sub_assoc. + replace (length a - 1) with (6 + length a - 7). + rewrite Nat.add_sub_assoc. rewrite Nat.add_assoc. + rewrite <- Nat.add_sub_assoc. + replace (length hd + 6) with (6 + length hd). + rewrite <- Nat.add_assoc. rewrite Nat.add_sub. simpl. reflexivity. + rewrite Nat.add_comm. reflexivity. apply Nat.le_succ_l. assumption. + rewrite Nat.le_succ_l. rewrite <- Nat.add_0_l at 1. + apply Nat.add_lt_mono. apply Nat.lt_0_succ. assumption. + + rewrite Nat.add_comm. + rewrite Nat.add_sub_swap. replace 6 with (7 - 1) at 2. + rewrite <- Nat.add_sub_swap. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.add_sub. reflexivity. + + rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. assumption. + + apply Nat.le_succ_l. apply Nat.lt_0_succ. + apply Nat.le_succ_l. assumption. reflexivity. + apply Nat.le_succ_l. assumption. + + rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. assumption. + + apply Nat.le_sub_l. rewrite O. + apply Nat.le_succ_l. apply Nat.lt_0_succ. + rewrite O. reflexivity. reflexivity. + + rewrite Nat.mul_comm. replace (2^3) with 8. + replace 3 with (length (hd++a) mod 8 - 1) at 4. + rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq. + rewrite app_length. rewrite app_length. + rewrite <- Nat.add_sub_assoc. rewrite <- Nat.add_le_mono_l. + rewrite firstn_length_le. + apply Nat.sub_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ. + rewrite <- Nat.sub_0_r. + apply Nat.sub_le_mono_l. apply le_0_n. + + rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. + apply Nat.lt_succ_l in I. assumption. + + rewrite O. apply Nat.le_succ_l. apply Nat.lt_0_succ. + rewrite O. reflexivity. reflexivity. + + assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 4) = Some (negb x)). + rewrite H. rewrite app_assoc. rewrite app_assoc. rewrite app_assoc. + rewrite nth_error_app1. + + rewrite Nat.mul_comm. replace (2^3) with 8. + replace 4 with (length (hd++a) mod 8) at 4. + rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1. + rewrite nth_error_app2. rewrite <- app_assoc. rewrite firstn_skipn. + rewrite Nat.sub_diag. reflexivity. + rewrite <- app_assoc. rewrite firstn_skipn. apply Nat.le_refl. + + reflexivity. + + + rewrite Nat.mul_comm. replace (2^3) with 8. + replace 4 with (length (hd++a) mod 8) at 3. + rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1. + replace ((hd ++ firstn (length a - 7) a) ++ skipn (length a - 7) a) + with (hd ++ firstn (length a - 7) a ++ skipn (length a - 7) a). + rewrite firstn_skipn. + replace (length ((hd ++ a) ++ rev [negb x; negb x; x; negb x; x; x; negb x])) + with (length (hd ++ a) + + length (rev [negb x; negb x; x; negb x; x; x; negb x])). + apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. + rewrite app_length. rewrite app_length. rewrite app_length. reflexivity. + rewrite <- app_assoc. reflexivity. reflexivity. + + rewrite H2 in H1. rewrite H3 in H1. simpl in H1. + inversion H1. contradiction H4. + + + + + + + + Lemma tm_step_palindrome_8_mod8 : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl