2023-01-17 11:12:20 -05:00
|
|
|
(** * The Thue-Morse sequence (part 3)
|
|
|
|
|
|
|
|
TODO
|
2023-01-18 03:45:21 -05:00
|
|
|
*)
|
2023-01-17 11:12:20 -05:00
|
|
|
|
|
|
|
Require Import thue_morse.
|
|
|
|
Require Import thue_morse2.
|
|
|
|
|
|
|
|
Require Import Coq.Lists.List.
|
|
|
|
Require Import PeanoNat.
|
|
|
|
Require Import Nat.
|
|
|
|
Require Import Bool.
|
|
|
|
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_palindromic_odd : forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ tl
|
|
|
|
-> a = rev a
|
|
|
|
-> odd (length a) = true
|
2023-01-17 15:07:54 -05:00
|
|
|
-> length a < 4.
|
2023-01-17 11:12:20 -05:00
|
|
|
Proof.
|
2023-01-17 15:07:54 -05:00
|
|
|
(* end of the lemma *)
|
|
|
|
assert (LEMMA: forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ tl
|
|
|
|
-> a = rev a
|
|
|
|
-> odd (length a) = true
|
|
|
|
-> length a <> 5).
|
2023-01-17 11:12:20 -05:00
|
|
|
intros n hd a tl. intros H I J.
|
|
|
|
destruct a. easy. destruct a. easy.
|
|
|
|
destruct a. easy. destruct a. easy.
|
|
|
|
destruct a. easy.
|
|
|
|
|
|
|
|
destruct a. (* case of length 5 *)
|
|
|
|
assert (exists (u v : list bool) (d: bool),
|
|
|
|
b::b0::b1::b2::b3::nil = u ++ [d;d] ++ v).
|
|
|
|
assert (4 < length (b::b0::b1::b2::b3::nil)). 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. generalize H0. generalize H.
|
|
|
|
apply tm_step_consecutive_identical_length.
|
|
|
|
|
|
|
|
destruct H0. destruct H0. destruct H0.
|
|
|
|
|
|
|
|
assert (K: {b=b0} + {~ b=b0}). apply bool_dec.
|
|
|
|
assert (L: {b0=b1} + {~ b0=b1}). apply bool_dec.
|
|
|
|
assert (M: {b1=b2} + {~ b1=b2}). apply bool_dec.
|
|
|
|
assert (N: {b2=b3} + {~ b2=b3}). apply bool_dec.
|
|
|
|
|
|
|
|
destruct K. rewrite e in H. rewrite e in I.
|
|
|
|
destruct N. rewrite e0 in H.
|
|
|
|
replace ([b0;b0;b1;b3;b3] ++ tl) with ([b0;b0] ++ [b1] ++ [b3;b3] ++ tl) in H.
|
|
|
|
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
|
|
|
|
inversion I. rewrite H3 in n0. contradiction n0.
|
|
|
|
|
|
|
|
destruct L. rewrite e in H. rewrite e in I.
|
|
|
|
destruct M. rewrite <- e0 in H.
|
|
|
|
replace (hd ++ [b; b1; b1; b1; b3] ++ tl)
|
|
|
|
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.
|
2023-01-18 03:45:21 -05:00
|
|
|
|
2023-01-17 11:12:20 -05:00
|
|
|
inversion I. rewrite H3 in n1. contradiction n1.
|
|
|
|
|
|
|
|
destruct M. rewrite <- e in I. inversion I.
|
|
|
|
rewrite H3 in n1. contradiction n1.
|
|
|
|
destruct N. rewrite e in I. inversion I.
|
|
|
|
rewrite H2 in n0. rewrite H3 in n0. contradiction n0.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H2 in n0. rewrite H3 in n0. contradiction n0.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H3 in n1. rewrite H4 in n1. contradiction n1.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H4 in n2. rewrite H5 in n2. contradiction n2.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H5 in n3. rewrite H6 in n3. contradiction n3.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
assert (length [b;b0;b1;b2;b3] = length [b;b0;b1;b2;b3]).
|
|
|
|
reflexivity. rewrite H0 in H1 at 2. simpl in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
|
|
|
|
rewrite app_length in H1. simpl in H1.
|
|
|
|
rewrite Nat.add_succ_r in H1. rewrite Nat.add_succ_r in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply O_S in H1. contradiction H1.
|
|
|
|
|
|
|
|
simpl. apply not_eq_S. apply not_eq_S. apply not_eq_S.
|
|
|
|
apply not_eq_S. apply not_eq_S. apply Nat.neq_succ_0.
|
2023-01-17 15:07:54 -05:00
|
|
|
(* end of the lemma *)
|
2023-01-17 11:12:20 -05:00
|
|
|
|
|
|
|
intros n hd a tl. intros H I J.
|
|
|
|
|
|
|
|
assert (length a <= 5 \/ 5 < length a). apply Nat.le_gt_cases.
|
|
|
|
destruct H0.
|
|
|
|
apply Nat.lt_eq_cases in H0. destruct H0.
|
|
|
|
rewrite Nat.lt_succ_r in H0.
|
|
|
|
apply Nat.lt_eq_cases in H0. destruct H0. assumption.
|
|
|
|
rewrite H0 in J. inversion J.
|
|
|
|
assert (length a <> 5). generalize J. generalize I. generalize H.
|
2023-01-17 15:07:54 -05:00
|
|
|
apply LEMMA. rewrite H0 in H1. contradiction H1.
|
2023-01-17 11:12:20 -05:00
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
(* main part of the proof:
|
|
|
|
each odd palindromic factor greater than 5
|
|
|
|
contains a palindromic subfactor of length 5 *)
|
2023-01-17 12:59:33 -05:00
|
|
|
pose (t := length a - 5). assert (Nat.even t = true).
|
|
|
|
unfold t. rewrite Nat.even_sub. rewrite <- Nat.negb_odd.
|
|
|
|
rewrite J. reflexivity. generalize H0.
|
|
|
|
apply Nat.lt_le_incl.
|
|
|
|
|
|
|
|
pose (u := firstn (Nat.div2 t) a).
|
|
|
|
pose (v := firstn 5 (skipn (Nat.div2 t) a)).
|
|
|
|
pose (w := skipn (Nat.div2 t + 5) a).
|
|
|
|
|
|
|
|
assert (a = u ++ v ++ w).
|
|
|
|
unfold u. unfold v. unfold w.
|
|
|
|
rewrite firstn_skipn_comm.
|
|
|
|
replace (Nat.div2 t) with (min (Nat.div2 t) (Nat.div2 t + 5)) at 1.
|
|
|
|
rewrite <- firstn_firstn. rewrite app_assoc. rewrite firstn_skipn.
|
|
|
|
rewrite firstn_skipn. reflexivity.
|
|
|
|
apply Nat.min_l. rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_le_mono_l. apply le_0_n.
|
|
|
|
|
|
|
|
assert (Nat.Even (length a - 5)).
|
|
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. rewrite Nat.even_sub.
|
|
|
|
rewrite <- Nat.negb_odd. rewrite J. reflexivity.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
|
|
|
|
assert (length v = 5). unfold v. apply firstn_length_le.
|
|
|
|
rewrite skipn_length. unfold t.
|
|
|
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
|
|
|
rewrite Nat.mul_sub_distr_l.
|
|
|
|
replace (2 * Nat.div2 (length a - 5))
|
|
|
|
with (Nat.double (Nat.div2 (length a - 5))).
|
|
|
|
rewrite <- Nat.Even_double.
|
|
|
|
|
|
|
|
replace (2 * length a) with ((length a + 5) + (length a - 5)).
|
|
|
|
rewrite Nat.add_sub. replace (2*5) with (5+5).
|
|
|
|
apply Nat.add_le_mono_r. apply Nat.lt_le_incl. assumption.
|
|
|
|
reflexivity. rewrite <- Nat.add_assoc.
|
|
|
|
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
|
|
|
|
rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
|
|
assumption. assumption.
|
|
|
|
apply Nat.double_twice. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
assert (length u = length w). unfold u. unfold w.
|
|
|
|
rewrite firstn_length. rewrite skipn_length. rewrite Nat.min_l.
|
|
|
|
unfold t. rewrite <- Nat.mul_cancel_l with (p := 2).
|
|
|
|
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
|
|
|
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_add_distr_l.
|
|
|
|
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
|
|
|
rewrite <- Nat.Even_double. rewrite Nat.double_twice.
|
|
|
|
rewrite <- Nat.add_sub_swap. rewrite <- Nat.add_sub_assoc.
|
|
|
|
replace (2 * length a) with ((length a - 5) + (length a + 5)).
|
|
|
|
simpl. rewrite Nat.add_sub. reflexivity.
|
|
|
|
rewrite Nat.add_comm. rewrite <- Nat.add_assoc.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
|
|
|
|
rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
|
|
assumption. simpl. apply le_n_S. apply le_n_S. apply le_n_S. apply le_n_S.
|
|
|
|
apply le_n_S. apply le_0_n. apply Nat.lt_le_incl. assumption.
|
|
|
|
assumption. assumption. easy.
|
|
|
|
unfold t.
|
|
|
|
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
|
|
|
|
rewrite <- Nat.Even_double. simpl. rewrite Nat.add_0_r.
|
|
|
|
rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono.
|
|
|
|
apply Nat.le_sub_l. apply le_0_n. assumption. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
assert (v = rev v). rewrite H2 in I.
|
2023-01-18 03:45:21 -05:00
|
|
|
rewrite rev_app_distr in I. rewrite rev_app_distr in I.
|
2023-01-17 12:59:33 -05:00
|
|
|
rewrite <- app_assoc in I.
|
|
|
|
|
|
|
|
assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
|
2023-01-19 01:17:53 -05:00
|
|
|
generalize I. apply app_eq_length_head.
|
|
|
|
rewrite H6 in I. rewrite rev_involutive in I.
|
2023-01-17 12:59:33 -05:00
|
|
|
apply app_inv_head in I. apply app_inv_tail in I. assumption.
|
|
|
|
|
|
|
|
assert (length v <> 5).
|
|
|
|
assert (odd (length v) = true). rewrite H4. reflexivity.
|
|
|
|
generalize H7. generalize H6. generalize H. rewrite H2.
|
|
|
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite app_assoc.
|
2023-01-17 15:07:54 -05:00
|
|
|
apply LEMMA. rewrite H4 in H7. contradiction H7.
|
2023-01-17 12:59:33 -05:00
|
|
|
reflexivity.
|
|
|
|
Qed.
|
2023-01-18 03:45:21 -05:00
|
|
|
|
|
|
|
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.
|
|
|
|
|
2023-01-18 06:24:21 -05:00
|
|
|
Lemma tm_step_palindromic_even_center' :
|
|
|
|
forall (n k m: nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 0 < length a
|
|
|
|
-> length (hd ++ a) = S (2 * k) * 2^m
|
|
|
|
-> odd m = true.
|
|
|
|
Proof.
|
|
|
|
intros n k m hd a tl. intros H I J.
|
|
|
|
assert (Z := H).
|
|
|
|
assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct K. rewrite e in I. inversion I.
|
|
|
|
assert (L: a = removelast a ++ [ last a false ]).
|
|
|
|
apply app_removelast_last. assumption.
|
|
|
|
rewrite L in H. rewrite rev_app_distr in H.
|
|
|
|
assert (nth_error (tm_step n) (length (hd++a))
|
|
|
|
= nth_error (tm_step n) (pred (length (hd++a)))).
|
|
|
|
rewrite H.
|
|
|
|
rewrite app_assoc. rewrite nth_error_app2.
|
|
|
|
symmetry. rewrite <- app_assoc. rewrite <- app_assoc.
|
|
|
|
rewrite app_assoc. rewrite nth_error_app2.
|
|
|
|
rewrite <- app_removelast_last. rewrite Nat.sub_diag.
|
|
|
|
replace (hd++a) with ((hd ++ removelast a) ++ [last a false]).
|
|
|
|
rewrite app_length. rewrite Nat.add_1_r. rewrite <- pred_Sn.
|
|
|
|
rewrite Nat.sub_diag. reflexivity. rewrite L at 3.
|
|
|
|
rewrite <- app_assoc. reflexivity. assumption.
|
|
|
|
|
|
|
|
rewrite L at 2. rewrite app_assoc.
|
|
|
|
replace (length ((hd ++ removelast a) ++ [last a false]))
|
|
|
|
with (length (hd ++ removelast a) + length [last a false]).
|
|
|
|
rewrite Nat.add_1_r. rewrite <- pred_Sn. apply Nat.le_refl.
|
|
|
|
|
|
|
|
symmetry. rewrite app_length. reflexivity.
|
|
|
|
rewrite <- app_removelast_last. apply Nat.le_refl.
|
|
|
|
assumption.
|
|
|
|
|
|
|
|
generalize H0. rewrite J. apply tm_step_pred.
|
|
|
|
|
|
|
|
rewrite <- J. rewrite <- tm_size_power2. rewrite Z.
|
|
|
|
rewrite app_length. rewrite app_length.
|
|
|
|
apply Nat.add_lt_mono_l. rewrite app_length.
|
|
|
|
rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_lt_mono_l. rewrite app_length. rewrite rev_length.
|
|
|
|
assert (0 <= length tl). apply le_0_n. rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_lt_le_mono; assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-01-19 01:17:53 -05:00
|
|
|
Lemma tm_step_palindromic_full : forall (n : nat),
|
|
|
|
tm_step (Nat.double (S n)) =
|
|
|
|
(tm_step (S (Nat.double n))) ++ rev (tm_step (S (Nat.double n))).
|
|
|
|
Proof.
|
|
|
|
intro n. induction n.
|
|
|
|
- reflexivity.
|
|
|
|
- rewrite Nat.double_S. rewrite tm_build. rewrite app_inv_head_iff.
|
|
|
|
rewrite <- tm_step_lemma. rewrite IHn.
|
|
|
|
rewrite tm_morphism_rev. rewrite tm_morphism_app. rewrite rev_app_distr.
|
|
|
|
rewrite map_app. rewrite map_app. rewrite tm_morphism_app.
|
|
|
|
rewrite rev_involutive. rewrite tm_build_negb. rewrite tm_build_negb.
|
|
|
|
reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
Lemma tm_step_palindromic_even_seed :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step (S n) = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 0 < length a
|
|
|
|
-> (2^n <= length hd) \/ (2^n <= length tl) \/ (length (hd ++a) = 2^n).
|
|
|
|
Proof.
|
|
|
|
intro n. induction n.
|
|
|
|
- intros hd a tl. intros H I. destruct a.
|
|
|
|
+ inversion I.
|
|
|
|
+ destruct a.
|
|
|
|
assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
|
|
|
|
rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
|
|
|
|
destruct hd; destruct tl. right. right. reflexivity.
|
|
|
|
right. left. simpl. apply le_n_S. apply le_0_n.
|
|
|
|
rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
|
|
|
|
contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
|
|
|
|
assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
|
|
|
|
rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
|
|
|
|
rewrite app_length in H0. rewrite app_length in H0.
|
|
|
|
rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
|
|
|
|
rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
|
|
|
|
- intros hd a tl. intros H I. rewrite tm_build in H.
|
|
|
|
assert (2^S n <= length hd \/ length hd < 2^S n). apply Nat.le_gt_cases.
|
|
|
|
assert (2^S n <= length tl \/ length tl < 2^S n). apply Nat.le_gt_cases.
|
|
|
|
destruct H0. left. assumption. destruct H1. right. left. assumption.
|
|
|
|
right. right.
|
|
|
|
assert (2^S n <= length (hd++a) \/ length (hd++a) < 2^S n).
|
|
|
|
apply Nat.le_gt_cases. destruct H2. apply Nat.lt_eq_cases in H2.
|
|
|
|
destruct H2.
|
|
|
|
pose (c := length (hd ++ a) - 2^ S n). (* ce qui dépasse, excès de a *)
|
|
|
|
pose (d := skipn ((length a) - c) a). (* on cherche le milieu de tm_step S (S n) *)
|
|
|
|
pose (e := d ++ firstn c (rev a)).
|
|
|
|
(* TODO e = rev e est-il vraiment utile ??? *)
|
|
|
|
assert (e = rev e). (* nouveau palindrome dans la seconde moitié *)
|
|
|
|
unfold e. unfold d.
|
|
|
|
rewrite firstn_rev. rewrite rev_app_distr. rewrite rev_involutive.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
(* montrer que e est dans la seconde moitié, excentré *)
|
|
|
|
assert (a = (firstn (length a - c) a) ++ d). unfold d.
|
|
|
|
symmetry. apply firstn_skipn.
|
|
|
|
|
|
|
|
rewrite H4 in H. rewrite <- app_assoc in H. rewrite rev_app_distr in H.
|
|
|
|
rewrite <- app_assoc in H. rewrite app_assoc in H.
|
|
|
|
|
|
|
|
assert (length hd + length a - 2 ^ S n <= length a).
|
|
|
|
rewrite Nat.add_le_mono_r with (p := 2^S n).
|
|
|
|
rewrite Nat.sub_add. rewrite Nat.add_comm at 1.
|
|
|
|
rewrite <- Nat.add_le_mono_l. apply Nat.lt_le_incl. assumption.
|
|
|
|
rewrite <- app_length. apply Nat.lt_le_incl. assumption.
|
|
|
|
|
|
|
|
assert (length (tm_step (S n)) = length (hd ++ firstn (length a - c) a)).
|
|
|
|
unfold c. rewrite app_length. rewrite tm_size_power2.
|
|
|
|
rewrite firstn_length_le. rewrite app_length.
|
|
|
|
rewrite Nat.add_sub_assoc.
|
|
|
|
|
|
|
|
replace (length hd + length a)
|
|
|
|
with (length hd + length a - 2^S n + 2^S n) at 1.
|
|
|
|
rewrite Nat.add_sub_swap. rewrite <- Nat.add_0_l at 1.
|
|
|
|
rewrite Nat.add_cancel_r. symmetry. apply Nat.sub_diag.
|
|
|
|
apply Nat.le_refl. rewrite <- Nat.add_sub_swap.
|
|
|
|
rewrite Nat.add_sub. reflexivity. apply Nat.lt_le_incl.
|
|
|
|
rewrite <- app_length. assumption. assumption.
|
|
|
|
|
|
|
|
apply Nat.le_sub_le_add_r. rewrite <- Nat.add_0_r at 1.
|
|
|
|
rewrite <- Nat.add_le_mono_l. apply le_0_n.
|
|
|
|
|
|
|
|
assert (tm_step (S n) = hd ++ firstn (length a - c) a).
|
|
|
|
generalize H6. generalize H.
|
|
|
|
apply app_eq_length_head. rewrite <- H7 in H.
|
|
|
|
apply app_inv_head in H.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
assert (map negb (tm_step (S n)) = e ++ ??? ++ tl). unfold e. unfold d.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-01-18 06:24:21 -05:00
|
|
|
|
2023-01-18 03:45:21 -05:00
|
|
|
|
|
|
|
|
2023-01-19 01:17:53 -05:00
|
|
|
|
|
|
|
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
induction n.
|
|
|
|
- right. right. destruct a. inversion I. destruct a.
|
|
|
|
assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
|
|
|
|
rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
|
|
|
|
destruct hd; destruct tl. reflexivity. reflexivity.
|
|
|
|
rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
|
|
|
|
contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
|
|
|
|
assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
|
|
|
|
rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
|
|
|
|
rewrite app_length in H0. rewrite app_length in H0.
|
|
|
|
rewrite app_length in H0. simpl in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
|
|
|
|
rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
|
|
|
|
rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
|
|
|
|
-
|
|
|
|
|
|
|
|
|
|
|
|
*)
|
2023-01-18 03:45:21 -05:00
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*)
|