diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 579480a..fefef68 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2096,6 +2096,134 @@ Proof. Qed. +Lemma tm_step_palindrome_7_destruct : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> length a = 7 + -> exists x, a = [negb x; negb x; x; negb x; x; x; negb x]. +Proof. + intros n hd a tl. intros H I. + + assert (J: 6 < length a). rewrite I. apply Nat.lt_succ_diag_r. + assert (K: length (hd ++ a) mod 4 = 0). generalize J. generalize H. + apply tm_step_palindromic_length_12. + + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. destruct a. inversion I. + destruct a. inversion I. + + destruct a. + replace (rev [b; b0; b1; b2; b3; b4; b5]) + with ([b5; b4; b3; b2; b1; b0; b]) in H. + + assert (even (length (hd ++ [b; b0; b1; b2; b3; b4; b5])) = true). + rewrite <- Nat.div_exact in K. rewrite K. rewrite Nat.even_mul. + reflexivity. easy. + assert (odd (length hd) = true). rewrite app_length in H0. + rewrite Nat.even_add in H0. simpl in H0. apply eqb_prop in H0. + rewrite <- Nat.negb_even. rewrite H0. reflexivity. + assert (length hd mod 4 = 1 \/ length hd mod 4 = 3). + apply odd_mod4. assumption. + destruct H2. + + assert (b3 = b4). + replace (hd ++ [b; b0; b1; b2; b3; b4; b5] + ++ [b5; b4; b3; b2; b1; b0; b] ++ tl) + with ((hd ++ [b; b0]) ++ [b1; b2; b3; b4] + ++ [b5; b5; b4; b3; b2; b1; b0; b] ++ tl) in H. + assert (length (hd ++ [b; b0]) mod 4 = 3). + rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2. + reflexivity. easy. + assert (exists x, skipn 2 [b1; b2; b3; b4] = [x; x]). + generalize H3. + apply tm_step_factor4_3mod4 with (n' := n) + (y := [b5; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption. + reflexivity. destruct H4. inversion H4. reflexivity. + rewrite <- app_assoc. reflexivity. rewrite H3 in H. + + assert (b4 <> b5). + replace (hd ++ [b; b0; b1; b2; b4; b4; b5] + ++ [b5; b4; b4; b2; b1; b0; b] ++ tl) + with ((hd ++ [b; b0; b1; b2]) ++ [b4] ++ [b4] ++ [b5] + ++ [b5; b4; b4; b2;b1;b0;b] ++ tl) in H. + apply tm_step_cubefree in H. destruct b4; destruct b5. + contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. + apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. + + assert (b4 <> b2). + replace (hd ++ [b; b0; b1; b2; b4; b4; b5] + ++ [b5; b4; b4; b2; b1; b0; b] ++ tl) + with ((hd ++ [b; b0; b1; b2; b4; b4; b5; b5]) + ++ [b4] ++ [b4] ++ [b2] ++ [b1;b0;b] ++ tl) in H. + apply tm_step_cubefree in H. destruct b4; destruct b2. + contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. + apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. + + assert (b2 = b5). destruct b2; destruct b4; destruct b5. + contradiction H4. reflexivity. contradiction H5. reflexivity. + reflexivity. contradiction H4. reflexivity. + contradiction H4. reflexivity. reflexivity. + contradiction H5. reflexivity. contradiction H4. reflexivity. + rewrite H6 in H. + + assert (b = b0). + replace (hd ++ [b; b0; b1; b5; b4; b4; b5] + ++ [b5; b4; b4; b5; b1; b0; b] ++ tl) + with (hd ++ [b; b0; b1; b5] + ++ [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl) in H. + assert (exists x, firstn 2 [b; b0; b1; b5] = [x; x]). + generalize H2. + apply tm_step_factor4_1mod4 with (n' := n) + (y := [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl). assumption. + reflexivity. destruct H7. inversion H7. reflexivity. reflexivity. + rewrite H7 in H. + + assert ({b1=b5} + {~ b1=b5}). apply bool_dec. destruct H8. rewrite e in H. + replace (hd ++ [b0; b0; b5; b5; b4; b4; b5] + ++ [b5; b4; b4; b5; b5; b0; b0] ++ tl) + with ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4] + ++ [b5; b5; b4; b4] ++ [b5; b5; b0; b0] ++ tl) in H. + assert (even (length ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4])) = true). + assert (0 < length ([b5; b5; b4; b4])). apply Nat.lt_0_succ. + generalize H8. generalize H. apply tm_step_square_pos. + rewrite app_length in H8. rewrite app_length in H8. + rewrite <- Nat.add_assoc in H8. rewrite Nat.even_add in H8. + rewrite <- Nat.negb_odd in H8. + rewrite H1 in H8. inversion H8. rewrite <- app_assoc. reflexivity. + + assert (b1 = b4). destruct b1; destruct b4; destruct b5. + reflexivity. reflexivity. contradiction n0. reflexivity. + contradiction H4. reflexivity. contradiction H4. reflexivity. + contradiction n0. reflexivity. reflexivity. reflexivity. + rewrite H8 in H. + + assert (b0 <> b4). + replace (hd ++ [b0; b0; b4; b5; b4; b4; b5] + ++ [b5; b4; b4; b5; b4; b0; b0] ++ tl) + with (hd ++ [b0] ++ [b0] ++ [b4] + ++ [b5;b4;b4;b5;b5; b4; b4; b5; b4; b0; b0] ++ tl) in H. + apply tm_step_cubefree in H. destruct b0; destruct b4. + contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. + apply Nat.lt_0_1. reflexivity. + + assert (b0 = b5). destruct b0; destruct b4; destruct b5. + reflexivity. contradiction H9. reflexivity. reflexivity. + contradiction H4. reflexivity. contradiction H4. reflexivity. + reflexivity. contradiction H9. reflexivity. reflexivity. + rewrite H10 in H. + + assert (b5 = negb b4). destruct b4; destruct b5. + contradiction H4. reflexivity. reflexivity. reflexivity. + contradiction H4. reflexivity. rewrite H11 in H. + + exists b4. rewrite H3. rewrite H6. rewrite H7. rewrite H8. rewrite H10. + rewrite H11. reflexivity. + rewrite app_length in K. rewrite <- Nat.add_mod_idemp_l in K. + rewrite H2 in K. inversion K. easy. reflexivity. + inversion I. +Qed. + Lemma tm_step_palindrome_8_destruct : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl @@ -2104,6 +2232,8 @@ Lemma tm_step_palindrome_8_destruct : Proof. intros n hd a tl. intros H I. + + (* assert (J: length a mod 4 = 0). rewrite I. reflexivity. assert (K := J). rewrite tm_step_palindromic_length_12_prefix @@ -2111,6 +2241,7 @@ Proof. assert (L: even (length hd) = true). rewrite <- Nat.div_exact in K. rewrite K. rewrite Nat.even_mul. reflexivity. easy. + *) destruct a. inversion I. destruct a. inversion I. destruct a. inversion I. destruct a. inversion I. @@ -2121,116 +2252,31 @@ Proof. replace (rev [b; b0; b1; b2; b3; b4; b5; b6]) with ([b6; b5; b4; b3; b2; b1; b0; b]) in H. - assert (b4 = b5). - replace (hd ++ [b; b0; b1; b2; b3; b4; b5; b6] - ++ [b6; b5; b4; b3; b2; b1; b0; b] ++ tl) - with ((hd ++ [b; b0; b1]) ++ [b2; b3; b4; b5] - ++ [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl) in H. - assert (length (hd ++ [b; b0; b1]) mod 4 = 3). - rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K. - reflexivity. easy. - assert (exists x, skipn 2 [b2; b3; b4; b5] = [x; x]). - generalize H0. - apply tm_step_factor4_3mod4 with (n' := n) - (y := [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption. - reflexivity. destruct H1. inversion H1. reflexivity. - rewrite <- app_assoc. reflexivity. rewrite H0 in H. + assert (exists x, [b0; b1; b2; b3; b4; b5; b6] + = [negb x; negb x; x; negb x; x; x; negb x]). + apply tm_step_palindrome_7_destruct + with (n := n) (hd := hd ++ [b]) (tl := [b] ++ tl). + rewrite <- app_assoc. assumption. reflexivity. - assert (b5 <> b6). - replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6] - ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl) - with ((hd ++ [b; b0; b1; b2; b3]) ++ [b5] ++ [b5] ++ [b6] - ++ [b6; b5; b5; b3; b2;b1;b0;b] ++ tl) in H. - apply tm_step_cubefree in H. destruct b5; destruct b6. - contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. - apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. + destruct H0. inversion H0. rewrite H2 in H. rewrite H3 in H. + rewrite H4 in H. rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. + rewrite H8 in H. - assert (b5 <> b3). - replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6] - ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl) - with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6]) - ++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H. - apply tm_step_cubefree in H. destruct b5; destruct b3. - contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. - apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. - - assert (b3 = b6). destruct b3; destruct b5; destruct b6. - contradiction H1. reflexivity. contradiction H2. reflexivity. - reflexivity. contradiction H1. reflexivity. - contradiction H1. reflexivity. reflexivity. - contradiction H2. reflexivity. contradiction H1. reflexivity. - rewrite H3 in H. - - assert (b0 = b1). - replace (hd ++ [b; b0; b1; b2; b6; b5; b5; b6] - ++ [b6; b5; b5; b6; b2; b1; b0; b] ++ tl) - with ((hd ++ [b]) ++ [b0; b1; b2; b6] - ++ [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl) in H. - assert (length (hd ++ [b]) mod 4 = 1). - rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K. - reflexivity. easy. - assert (exists x, firstn 2 [b0; b1; b2; b6] = [x; x]). - generalize H4. - apply tm_step_factor4_1mod4 with (n' := n) - (y := [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl). assumption. - reflexivity. destruct H5. inversion H5. reflexivity. - rewrite <- app_assoc. reflexivity. rewrite H4 in H. - - assert ({b2=b6} + {~ b2=b6}). apply bool_dec. destruct H5. rewrite e in H. - replace (hd ++ [b; b1; b1; b6; b6; b5; b5; b6] - ++ [b6; b5; b5; b6; b6; b1; b1; b] ++ tl) - with ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5] - ++ [b6; b6; b5; b5] ++ [b6; b6; b1; b1; b] ++ tl) in H. - assert (even (length ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5])) = true). - assert (0 < length ([b6; b6; b5; b5])). apply Nat.lt_0_succ. - generalize H5. generalize H. apply tm_step_square_pos. - rewrite app_length in H5. rewrite app_length in H5. - rewrite <- Nat.add_assoc in H5. rewrite Nat.even_add in H5. - rewrite L in H5. inversion H5. rewrite <- app_assoc. reflexivity. - - assert (b2 = b5). destruct b2; destruct b6; destruct b5. - reflexivity. contradiction n0. reflexivity. reflexivity. - contradiction H1. reflexivity. contradiction H1. reflexivity. - reflexivity. contradiction n0. reflexivity. reflexivity. - rewrite H5 in H. - - assert (b1 <> b5). - replace (hd ++ [b; b1; b1; b5; b6; b5; b5; b6] - ++ [b6; b5; b5; b6; b5; b1; b1; b] ++ tl) - with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b5] - ++ [b6;b5;b5;b6;b6; b5; b5; b6; b5; b1; b1; b] ++ tl) in H. - apply tm_step_cubefree in H. destruct b1; destruct b5. - contradiction H. reflexivity. easy. easy. contradiction H. reflexivity. - apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. - - assert (b1 = b6). destruct b1; destruct b5; destruct b6. - reflexivity. contradiction H6. reflexivity. reflexivity. - contradiction H1. reflexivity. contradiction H1. reflexivity. - reflexivity. contradiction H6. reflexivity. reflexivity. - rewrite H7 in H. - - assert ({b=b6} + {~ b=b6}). apply bool_dec. destruct H8. rewrite e in H. - replace (hd ++ [b6; b6; b6; b5; b6; b5; b5; b6] - ++ [b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) - with (hd ++ [b6] ++ [b6] ++ [b6] - ++ [b5; b6;b5;b5;b6;b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) in H. + assert ({b=x} + {~ b=x}). apply bool_dec. destruct H1. + exists x. rewrite e. reflexivity. + assert (b = negb x). destruct b; destruct x. + contradiction n0. reflexivity. reflexivity. reflexivity. + contradiction n0. reflexivity. + rewrite H1 in H. + replace (hd ++ [negb x; negb x; negb x; x; negb x; x; x; negb x] ++ + [negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl) + with (hd ++ [negb x] ++ [negb x] ++ [negb x] + ++ [x; negb x; x; x; negb x; + negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. - assert (b = b5). destruct b; destruct b5; destruct b6. - reflexivity. reflexivity. contradiction n1. reflexivity. - contradiction H1. reflexivity. contradiction H1. reflexivity. - contradiction n1. reflexivity. reflexivity. reflexivity. - rewrite H8 in H. - - assert (b6 = negb b5). destruct b5; destruct b6. - contradiction H1. reflexivity. reflexivity. reflexivity. - contradiction H1. reflexivity. rewrite H9 in H. - - exists b5. rewrite H4. rewrite H3. rewrite H8. rewrite H7. rewrite H5. - rewrite H0. rewrite H9. reflexivity. - reflexivity. inversion I. assumption. rewrite I. - rewrite <- Nat.le_succ_l. apply Nat.le_succ_diag_r. + reflexivity. inversion I. Qed. @@ -2254,6 +2300,21 @@ Proof. generalize I. generalize H. apply tm_step_palindrome_8_destruct. destruct M as [x M]. + assert (N: length (hd ++ a) mod 4 = 0). + rewrite app_length. rewrite Nat.add_mod. + rewrite J. rewrite K. reflexivity. easy. + + 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. + + destruct O as [O | O]. assumption. + (*