diff --git a/src/thue_morse.v b/src/thue_morse.v index 4893944..b4cd90a 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -340,6 +340,16 @@ Proof. simpl. rewrite negb_involutive. reflexivity. Qed. +Lemma tm_morphism_twice_rev : forall (l : list bool), + rev (tm_morphism (tm_morphism l)) = tm_morphism (tm_morphism (rev l)). +Proof. + intro l. induction l. + - reflexivity. + - simpl. rewrite tm_morphism_app. rewrite tm_morphism_app. + rewrite <- IHl. rewrite <- app_assoc. rewrite <- app_assoc. + rewrite <- app_assoc. simpl. rewrite negb_involutive. reflexivity. +Qed. + (** Lemmas and theorems below are related to the second function defined initially. diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 01386a4..b2d3d9b 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -211,7 +211,7 @@ Proof. reflexivity. Qed. -Lemma tm_step_palindromic_even_center : +Theorem tm_step_palindromic_even_center : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl -> 0 < length a @@ -1852,9 +1852,58 @@ Qed. +Lemma xxx : + forall (m n k : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 6 < length a + -> length a = 2^(Nat.double m) + -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0. +Proof. + intros m n k hd a tl. intros H I J. + + destruct m. rewrite J in I. inversion I. inversion H1. + destruct m. rewrite J in I. inversion I. inversion H1. + inversion H3. inversion H5. inversion H7. + + assert (W: (length a) mod 4 = 0). + rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. + rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. + rewrite Nat.mul_assoc in J. + replace (2*2) with 4 in J. rewrite J. + rewrite <- Nat.mul_mod_idemp_l. reflexivity. + easy. reflexivity. apply le_0_n. apply le_0_n. + + assert ( + hd = tm_morphism (tm_morphism (firstn (length hd / 4) + (tm_step (pred (pred n))))) + /\ a = tm_morphism (tm_morphism + (firstn (length a / 4) (skipn (length hd / 4) + (tm_step (pred (pred n)))))) + /\ tl = tm_morphism (tm_morphism + (skipn (length hd / 4 + Nat.div2 (length a)) + (tm_step (pred (pred n)))))). + generalize W. generalize I. generalize H. + apply tm_step_palindromic_even_morphism2. + destruct H0 as [K H0]. destruct H0 as [L M]. + + assert (V: 3 < n). generalize I. generalize H. + apply tm_step_palindromic_length_12_n. + + induction m. + - rewrite K in H. rewrite L in H. rewrite M in H. + rewrite tm_morphism_twice_rev in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. +Theorem tm_step_palindromic_even_center : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 0 < length a + -> even (length (hd ++ a)) = true. + @@ -1891,6 +1940,7 @@ Proof. (tm_step (pred (pred n)))))). generalize W. generalize I. generalize H. apply tm_step_palindromic_even_morphism2. + destruct H0 as [K H0]. destruct H0 as [L M].