2023-01-17 16:12:20 +00:00
|
|
|
(** * The Thue-Morse sequence (part 3)
|
|
|
|
|
|
|
|
TODO
|
|
|
|
*)
|
|
|
|
|
|
|
|
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 20:07:54 +00:00
|
|
|
-> length a < 4.
|
2023-01-17 16:12:20 +00:00
|
|
|
Proof.
|
2023-01-17 20:07:54 +00: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 16:12:20 +00: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.
|
|
|
|
|
|
|
|
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 20:07:54 +00:00
|
|
|
(* end of the lemma *)
|
2023-01-17 16:12:20 +00: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 20:07:54 +00:00
|
|
|
apply LEMMA. rewrite H0 in H1. contradiction H1.
|
2023-01-17 16:12:20 +00:00
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
(* main part of the proof:
|
|
|
|
each odd palindromic factor greater than 5
|
|
|
|
contains a palindromic subfactor of length 5 *)
|
2023-01-17 17:59:33 +00: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.
|
|
|
|
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,
|
|
|
|
x0 ++ x1 = y0 ++ y1 -> length x0 = length y0 -> x0 = y0).
|
|
|
|
|
|
|
|
intro x0. induction x0. destruct y0. intros. reflexivity.
|
|
|
|
intros. inversion H7. destruct y0. intros. inversion H7.
|
|
|
|
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.
|
|
|
|
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 20:07:54 +00:00
|
|
|
apply LEMMA. rewrite H4 in H7. contradiction H7.
|
2023-01-17 17:59:33 +00:00
|
|
|
reflexivity.
|
|
|
|
Qed.
|