baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

This commit is contained in:
Thomas Baruchel 2023-01-18 09:45:21 +01:00
parent 8f027411c3
commit 43d9079e58
1 changed files with 63 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
src/thue_morse3.v
View File

@ -1,7 +1,7 @@
(** * The Thue-Morse sequence (part 3)
TODO
*)
*)
Require Import thue_morse.
Require Import thue_morse2.
@ -59,7 +59,7 @@ Proof.
with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b1] ++ ([b3] ++ tl)) in H.
apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_succ. rewrite <- app_assoc. simpl. reflexivity.
inversion I. rewrite H3 in n1. contradiction n1.
destruct M. rewrite <- e in I. inversion I.
@ -174,7 +174,7 @@ Proof.
apply Nat.le_sub_l. apply le_0_n. assumption. apply Nat.lt_0_2.
assert (v = rev v). rewrite H2 in I.
rewrite rev_app_distr in I. rewrite rev_app_distr in I.
rewrite rev_app_distr in I. rewrite rev_app_distr in I.
rewrite <- app_assoc in I.
assert (forall x0 x1 y0 y1 : list bool,
@ -185,13 +185,13 @@ Proof.
intros. simpl in H7. apply Nat.succ_inj in H7.
rewrite <- app_comm_cons in H6.
rewrite <- app_comm_cons in H6.
destruct a0; destruct b. inversion H6.
apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
assumption. inversion H6. inversion H6. inversion H6.
apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
assumption.
assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
generalize I. apply H6.
rewrite H7 in I. rewrite rev_involutive in I.
@ -204,3 +204,61 @@ Proof.
apply LEMMA. rewrite H4 in H7. contradiction H7.
reflexivity.
Qed.
Lemma 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.
Proof.
intros n hd a tl. intros H I.
assert (J: a = removelast a ++ [ last a false ]).
apply app_removelast_last.
assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
destruct K. rewrite e in I. inversion I. assumption.
rewrite J in H. rewrite rev_app_distr in H.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite app_assoc in H.
replace
([last a false] ++ rev [last a false] ++ rev (removelast a) ++ tl)
with ([last a false; last a false] ++ (rev (removelast a) ++ tl)) in H.
apply tm_step_consecutive_identical in H. rewrite J.
rewrite app_assoc. rewrite app_length. rewrite Nat.even_add.
rewrite <- Nat.negb_odd. rewrite H. reflexivity.
reflexivity.
Qed.
(*
TODO: les palindromes de longueur 16 sont centrés autour
des valeurs de la suite ci-dessous A056196
TODO: erratum 216 est un centre possible ! (216 = 2^3 3^3)
A056196 Numbers n such that A055229(n) = 2. +30
2
8, 24, 32, 40, 56, 72, 88, 96, 104, 120, 128, 136, 152, 160, 168, 184, 200, 224, 232,
248, 264, 280, 288, 296, 312, 328, 344, 352, 360, 376, 384, 392, 408, 416, 424, 440,
456, 472, 480, 488, 504, 512, 520, 536, 544, 552, 568, 584, 600, 608, 616, 632, 640
(list; graph; refs; listen; history; text; internal format)
OFFSET 1,1
COMMENTS By definition, the largest square divisor and squarefree part of these
numbers have GCD = 2.
Different from A036966. E.g., 81 is not here because A055229(81) = 1.
Numbers of the form 2^(2*k+1) * m, where k >= 1 and m is an odd number
whose prime factorization contains only exponents that are either 1 or
even. The asymptotic density of this sequence is (1/12) * Product_{p odd
prime} (1-1/(p^2*(p+1))) = A065465 / 11 = 0.08013762179319734335... -
Amiram Eldar, Dec 04 2020, Nov 25 2022
LINKS Robert Israel, Table of n, a(n) for n = 1..10000
EXAMPLE 88 is here because 88 has squarefree part 22, largest square divisor 4,
and A055229(88) = gcd(22, 4) = 2.
*)