From 09b3f8f05cc5217bc9020e0d3c4ea265dfaaca36 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 2 Feb 2023 18:44:05 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 64 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 0fa0fc8..a71a420 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2108,6 +2108,9 @@ Proof. assert (K := J). rewrite tm_step_palindromic_length_12_prefix with (n := n) (hd := hd) (tl := tl) in K. + 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. @@ -2133,6 +2136,15 @@ Proof. reflexivity. destruct H1. inversion H1. reflexivity. rewrite <- app_assoc. reflexivity. rewrite H0 in H. + 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. + assert (b5 <> b3). replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6] ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl) @@ -2142,8 +2154,60 @@ Proof. 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. (* Lemma tm_step_proper_palindrome_center :