1639 lines
64 KiB
Coq
1639 lines
64 KiB
Coq
(** * The Thue-Morse sequence (part 3)
|
|
|
|
TODO
|
|
|
|
tm_step_rev
|
|
*)
|
|
|
|
Require Import thue_morse.
|
|
Require Import thue_morse2.
|
|
|
|
Require Import Coq.Lists.List.
|
|
Require Import PeanoNat.
|
|
Require Import Nat.
|
|
Require Import Bool.
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
Theorem tm_step_rev : forall (n : nat),
|
|
tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n)).
|
|
Proof.
|
|
assert (Z: forall l, map (fun x : bool => negb (negb x)) l = l).
|
|
intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
|
|
rewrite IHl. reflexivity.
|
|
|
|
intro n. induction n. left. reflexivity.
|
|
rewrite tm_build. destruct IHn ; [right | left];
|
|
rewrite rev_app_distr; rewrite H at 1;
|
|
rewrite H at 2; rewrite <- map_rev.
|
|
rewrite map_app. rewrite map_map. rewrite Z. reflexivity.
|
|
rewrite map_map. rewrite Z. reflexivity.
|
|
Qed.
|
|
|
|
|
|
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
|
|
-> length a < 4.
|
|
Proof.
|
|
(* 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).
|
|
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.
|
|
(* end of the lemma *)
|
|
|
|
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.
|
|
apply LEMMA. rewrite H0 in H1. contradiction H1.
|
|
reflexivity.
|
|
|
|
(* main part of the proof:
|
|
each odd palindromic factor greater than 5
|
|
contains a palindromic subfactor of length 5 *)
|
|
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 (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
|
|
generalize I. apply app_eq_length_head.
|
|
rewrite H6 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.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
Theorem tm_step_palindromic_full : forall (n : nat),
|
|
odd n = true -> tm_step (S n) = (tm_step n) ++ rev (tm_step n).
|
|
Proof.
|
|
intro n. intro H.
|
|
apply Nat.odd_OddT in H. apply Nat.OddT_Odd in H.
|
|
apply Nat.Odd_double in H. rewrite H. rewrite tm_step_odd_step.
|
|
rewrite <- tm_build. reflexivity.
|
|
Qed.
|
|
|
|
(* very close to the previous one but we add the case n=0 here *)
|
|
Theorem tm_step_palindromic_full_even : forall (n : nat),
|
|
even n = true -> tm_step n = rev (tm_step n).
|
|
Proof.
|
|
intro n. intro H. destruct n. reflexivity.
|
|
rewrite Nat.even_succ in H. apply tm_step_palindromic_full in H.
|
|
rewrite H. rewrite rev_app_distr. rewrite rev_involutive.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
|
|
(**
|
|
In this notebook I call "proper palindrome" in the Thue-Morse sequence,
|
|
any palindromic subsequence such that the middle (of the palindromic
|
|
subsequence) is not also the middle of a wider palindromic subsequence.
|
|
In ther words, a proper palindrome can not be enlarged by adding more
|
|
termes on both sides.
|
|
*)
|
|
|
|
|
|
(* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *)
|
|
(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème
|
|
ET existence d'un palindrome 2 * - *)
|
|
Lemma tm_step_palindromic_length_8 :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
-> length a = 4
|
|
-> length (hd ++ a) mod 4 = 0
|
|
\/ nth_error hd (length hd - 3) <> nth_error tl 2.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
|
|
(* proof that length hd++a is even *)
|
|
assert (P: even (length (hd ++ a)) = true).
|
|
assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0.
|
|
generalize H. apply tm_step_palindromic_even_center.
|
|
|
|
assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2).
|
|
generalize P. apply even_mod4.
|
|
|
|
(* proof that length hd is even *)
|
|
assert (Q: even (length hd) = true). rewrite app_length in P.
|
|
rewrite Nat.even_add_even in P. assumption. rewrite I.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
|
|
(* construction de a *)
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a. simpl in H.
|
|
|
|
(* proof that b1 <> b2 *)
|
|
assert ({b1=b2} + {~ b1=b2}). apply bool_dec. destruct H0.
|
|
replace (hd ++ b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
|
|
with ((hd ++ b :: b0 :: nil)
|
|
++ [b1] ++ [b2] ++ [b2] ++ b1 :: b0 :: b :: tl) in H.
|
|
rewrite e in H. apply tm_step_cubefree in H. contradiction H.
|
|
reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
|
|
|
(* proof that n > 2 *)
|
|
assert (2 < n).
|
|
assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
|
|
<= length hd
|
|
+ length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)).
|
|
apply Nat.add_le_mono. apply le_0_n. apply Nat.le_refl.
|
|
rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J.
|
|
rewrite tm_size_power2 in J.
|
|
destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1.
|
|
destruct n. inversion J. inversion H1.
|
|
apply Nat.nle_succ_0 in H3. contradiction H3.
|
|
destruct n. inversion J. inversion H1. inversion H3. inversion H5.
|
|
inversion H7. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
apply Nat.lt_0_succ.
|
|
|
|
(* proof that hd <> nil *)
|
|
destruct hd.
|
|
assert (Z: 4 < 2^n). replace 4 with (2^2).
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
|
assert (Some b2 = nth_error (tm_step n) 3). rewrite H. reflexivity.
|
|
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H1.
|
|
simpl in H1.
|
|
assert (Some b2 = nth_error (tm_step n) 4). rewrite H. reflexivity.
|
|
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H2.
|
|
simpl in H2.
|
|
rewrite H1 in H2. inversion H2. apply tm_step_stable. 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. assumption. apply tm_step_stable. simpl.
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
assert (3 < 4).
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
generalize Z. generalize H2. apply Nat.lt_trans.
|
|
|
|
(* proof that tl <> nil *)
|
|
destruct tl.
|
|
|
|
assert (Z: 4 < 2^n). replace 4 with (2^2).
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
|
|
|
assert (Y: tm_step n = rev (tm_step n)
|
|
\/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev.
|
|
destruct Y; rewrite H in H1 at 2; rewrite rev_app_distr in H1.
|
|
|
|
assert (Some b2 = nth_error (tm_step n) 3). rewrite H1. reflexivity.
|
|
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
|
|
simpl in H2.
|
|
assert (Some b2 = nth_error (tm_step n) 4). rewrite H1. reflexivity.
|
|
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
|
|
simpl in H3.
|
|
rewrite H2 in H3. inversion H3. apply tm_step_stable. 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. assumption. apply tm_step_stable. simpl.
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
assert (3 < 4).
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
generalize Z. generalize H3. apply Nat.lt_trans.
|
|
|
|
assert (Some (negb b2) = nth_error (tm_step n) 3). rewrite H1.
|
|
rewrite nth_error_map. reflexivity.
|
|
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
|
|
simpl in H2.
|
|
assert (Some (negb b2) = nth_error (tm_step n) 4). rewrite H1.
|
|
rewrite nth_error_map. reflexivity.
|
|
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
|
|
simpl in H3.
|
|
rewrite H2 in H3. inversion H3. apply tm_step_stable. 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. assumption. apply tm_step_stable. simpl.
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
assert (3 < 4).
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
generalize Z. generalize H3. apply Nat.lt_trans.
|
|
|
|
(* FIRST PART OF THE PROOF: case b0 = b1 *)
|
|
(* première hypothèse b0 = b1 mais alors on construit vers la
|
|
gauche jusqu'à (lest hd) et l'on a dans l'ordre jusqu'au centre :
|
|
b1 | (negb b1) b1 | b1 (negb b1 ||
|
|
et les quatre premiers termes vont impliquer que le centre soit en 4n+2 *)
|
|
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
|
|
rewrite e in H.
|
|
|
|
(* on a alors b = negb b1 (car dans le même bloc pair on a 01 ou 10 *)
|
|
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
|
|
rewrite e0 in H.
|
|
replace
|
|
((b3 :: hd) ++ b1 :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl)
|
|
with
|
|
((b3 :: hd) ++ [b1] ++ [b1] ++ [b1]
|
|
++ b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_1. reflexivity.
|
|
|
|
(* à ce stade on a F T | T F || F T T F
|
|
trois cas :
|
|
(??? T) | F T T F || F T T F | ??? impossible à gauche
|
|
(T F) | F T T F || F T T F | (F T) cube
|
|
(T F) | F T T F || F T T F | (T F) OK, diff + impossible à droite
|
|
*)
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
|
|
rewrite <- app_assoc in H.
|
|
assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}).
|
|
apply bool_dec. destruct H1. rewrite e0 in H.
|
|
(* un cas à étudier
|
|
(??? T) | F T T F || F T T F | ??? impossible à gauche
|
|
*)
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
|
|
rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in H1.
|
|
destruct Q.
|
|
assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H2.
|
|
assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H3.
|
|
replace (
|
|
removelast (b3 :: hd) ++
|
|
[b1] ++ b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )
|
|
with (
|
|
removelast (b3 :: hd) ++ [b1;b;b1;b1]
|
|
++ (b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )) in H.
|
|
generalize H. apply tm_step_factor4_1mod4. reflexivity.
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
|
|
contradiction n1. reflexivity.
|
|
|
|
rewrite app_length in H1. rewrite app_length in H1.
|
|
rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
|
|
rewrite H2 in H1. inversion H1. easy. easy. easy.
|
|
|
|
(* Deux cas
|
|
(T F) | F T T F || F T T F | (F T) cube
|
|
(T F) | F T T F || F T T F | (T F) impossible à droite
|
|
*)
|
|
assert ({b4=b1} + {~ b4=b1}). apply bool_dec. destruct H1. rewrite e0 in H.
|
|
(* un sous-cas :
|
|
(T F) | F T T F || F T T F | (T F) impossible à droite
|
|
*)
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
rewrite e in H1.
|
|
assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
|
|
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1.
|
|
reflexivity. easy.
|
|
|
|
replace(
|
|
removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
|
|
b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b1 :: tl )
|
|
with (
|
|
(((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) ++ [b1; b1;b;b1] ++ tl) in H.
|
|
|
|
assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H2.
|
|
assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H3.
|
|
generalize H. apply tm_step_factor4_3mod4.
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
|
|
contradiction n1. reflexivity.
|
|
symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
|
|
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy.
|
|
|
|
(* un sous-cas
|
|
(T F) | F T T F || F T T F | (F T) cube
|
|
*)
|
|
assert (b4 = b). destruct b4; destruct b1; destruct b.
|
|
reflexivity. contradiction n3. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n3. reflexivity. reflexivity. rewrite H1 in H.
|
|
assert (b2 = b). destruct b2; destruct b1; destruct b.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
|
|
assert (last (b3::hd) false = b).
|
|
destruct (last (b3::hd) false); destruct b1; destruct b.
|
|
reflexivity. contradiction n2. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n2. reflexivity. reflexivity.
|
|
|
|
(* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
|
|
destruct hd. inversion Q. destruct tl.
|
|
assert (0 < n). apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption.
|
|
apply tm_step_length_even in H4. rewrite H in H4.
|
|
rewrite app_assoc in H4. rewrite <- app_removelast_last in H4.
|
|
rewrite app_length in H4. rewrite Nat.even_add in H4.
|
|
rewrite Q in H4. inversion H4. easy. rewrite H3 in H.
|
|
rewrite app_removelast_last
|
|
with (l := removelast (b3::b5::hd)) (d := false) in H.
|
|
rewrite <- app_assoc in H.
|
|
|
|
(* assigner
|
|
last (removelast (b3 :: b5 :: hd)) false = b1
|
|
b6 = b1
|
|
*)
|
|
assert ({last (removelast (b3 :: b5 :: hd)) false=b}
|
|
+ {~ last (removelast (b3 :: b5 :: hd)) false=b}). apply bool_dec.
|
|
destruct H4. rewrite e0 in H.
|
|
replace (
|
|
removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b]
|
|
++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl)
|
|
with (
|
|
removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b] ++ [b]
|
|
++ b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_1. reflexivity.
|
|
assert (last (removelast (b3 :: b5 :: hd)) false = b1).
|
|
destruct (last (removelast (b3 :: b5 :: hd)) false); destruct b1; destruct b.
|
|
reflexivity. reflexivity. contradiction n4. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
contradiction n4. reflexivity. reflexivity. reflexivity. rewrite H4 in H.
|
|
assert ({b6=b} + {~ b6=b}). apply bool_dec. destruct H5. rewrite e0 in H.
|
|
replace (
|
|
removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
|
|
++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b :: tl)
|
|
with (
|
|
(removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
|
|
++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: nil)
|
|
++ [b] ++ [b] ++ [b] ++ tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
|
assert (b6 = b1). destruct (b6); destruct b1; destruct b.
|
|
reflexivity. reflexivity. contradiction n5. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
contradiction n5. reflexivity. reflexivity. reflexivity. rewrite H5 in H.
|
|
|
|
(* contradiction *)
|
|
replace (
|
|
removelast (removelast (b3 :: b5 :: hd)) ++
|
|
[b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b1 :: tl)
|
|
with (removelast (removelast (b3 :: b5 :: hd)) ++
|
|
[b1;b;b;b1] ++ [b1;b;b;b1] ++ [b1;b;b;b1] ++ tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_succ. reflexivity. easy. easy.
|
|
|
|
(* SECOND PART PF THE PROOF: case b0 <> b1 *)
|
|
(* sinon, sur la base de T F T F || F T F T
|
|
quatre cas :
|
|
(F T) | T F T F || F T F T | (F T) diff + impossible à droite
|
|
(F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ?
|
|
empiriquement : n'apparaît jamais
|
|
remonter encore d'un cran et prouver la différence à ce stade,
|
|
TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
|
|
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
|
|
revoir l'énoncé en fonction
|
|
(T F) | T F T F || F T F T | (F T) cube
|
|
(T F) | T F T F || F T F T | (T F) diff + impossible à gauche
|
|
*)
|
|
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e in H.
|
|
(*
|
|
assert (b2 = b0). destruct (b2); destruct b1; destruct b0.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
|
|
*)
|
|
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
|
|
rewrite <- app_assoc in H.
|
|
assert ({last (b3::hd) false=b0} + {~ last (b3::hd) false=b0}).
|
|
apply bool_dec. destruct H1. rewrite e0 in H.
|
|
|
|
(* problème à gauche *)
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
|
|
rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
|
|
destruct Q.
|
|
assert (exists x, firstn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
|
|
assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
|
|
replace (
|
|
removelast (b3 :: hd) ++
|
|
[b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
|
|
with (
|
|
removelast (b3 :: hd) ++ [b0;b1;b0;b1]
|
|
++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
|
|
generalize H. apply tm_step_factor4_1mod4. reflexivity.
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
|
|
contradiction n1. reflexivity.
|
|
|
|
assert (exists x, skipn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
|
|
assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
|
|
replace (
|
|
removelast (b3 :: hd) ++
|
|
[b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
|
|
with (
|
|
removelast (b3 :: hd) ++ [b0;b1;b0;b1]
|
|
++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
|
|
generalize H. apply tm_step_factor4_3mod4. reflexivity.
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
|
|
contradiction n1. reflexivity. easy.
|
|
|
|
(* nouveau cas : last (b3 :: hd) false <> b0
|
|
(F T) | T F T F || F T F T | (F T) diff + impossible à droite
|
|
(F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ?
|
|
*)
|
|
(* régler d'abord la question du modulo au centre *)
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
assert (last (b3::hd) false = b1).
|
|
destruct (last (b3::hd) false); destruct b1; destruct b0.
|
|
reflexivity. reflexivity. contradiction n2. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
contradiction n2. reflexivity. reflexivity. reflexivity.
|
|
|
|
assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H.
|
|
assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]).
|
|
replace (removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
|
|
b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b0 :: tl)
|
|
with (((b3 :: hd) ++ [b1;b0;b1;b2;b2])
|
|
++ [b1;b0;b1;b0] ++ tl) in H.
|
|
assert (length ((b3::hd) ++ [b1; b0; b1; b2; b2]) mod 4 = 3). rewrite e in H1.
|
|
replace ([b1;b0;b1;b2;b2]) with ([b1;b0;b1;b2] ++ [b2]).
|
|
rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
|
|
rewrite H1. reflexivity. easy. reflexivity.
|
|
assert (length [b1;b0;b1;b0] = 4). reflexivity.
|
|
generalize H3. generalize H4. generalize H. apply tm_step_factor4_3mod4.
|
|
symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
|
|
rewrite <- app_assoc. reflexivity. easy.
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
|
|
contradiction n1. reflexivity.
|
|
|
|
assert (b4 = b1). destruct b4; destruct b1; destruct b0.
|
|
reflexivity. reflexivity. contradiction n3. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
contradiction n3. reflexivity. reflexivity. reflexivity.
|
|
rewrite H3 in H. rewrite H2 in H.
|
|
|
|
assert (b2 = b0). destruct b2; destruct b1; destruct b0.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n0. reflexivity. reflexivity.
|
|
rewrite H4 in H.
|
|
|
|
(* dernier cas (difficile
|
|
(F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ?
|
|
remarquer le schéma a ++ (rev a) ++ a
|
|
apparaît jusqu'à six termes à gauche et à droite
|
|
empiriquement : n'apparaît jamais avec un 7ème palindromique ajouté
|
|
remonter encore d'un cran et prouver la différence à ce stade,
|
|
TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
|
|
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
|
|
FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???)
|
|
TFT TFT FF TFT TFT (si on part sur 2 mod 8)
|
|
(idem en partant de la droite pour 6 mod 8)
|
|
Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|
[False, True, True, False, True, False, False, True]
|
|
--> il y a une contradiction à chaque fois
|
|
*)
|
|
|
|
(* on prouve 3 < n *)
|
|
assert (R: 2^3 < length (tm_step n)). rewrite H.
|
|
rewrite app_length. rewrite <- Nat.add_0_l at 1.
|
|
apply Nat.add_le_lt_mono. apply Nat.le_0_l. simpl.
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
|
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. rewrite tm_size_power2 in R.
|
|
rewrite <- Nat.pow_lt_mono_r_iff in R.
|
|
|
|
(* on étend hd *)
|
|
destruct hd. inversion Q.
|
|
rewrite app_removelast_last
|
|
with (l := removelast (b3::b5::hd)) (d := false) in H.
|
|
assert ({last (removelast (b3 :: b5 :: hd)) false = b1}
|
|
+ {~ last (removelast (b3 :: b5 :: hd)) false = b1}).
|
|
apply bool_dec. destruct H5. rewrite e0 in H.
|
|
rewrite <- app_assoc in H.
|
|
replace (b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl)
|
|
with ([b1] ++ b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_1. reflexivity.
|
|
|
|
(* on étend tl*)
|
|
destruct tl.
|
|
assert (tm_step n = rev (tm_step n)
|
|
\/ tm_step n = map negb (rev (tm_step n))).
|
|
apply tm_step_rev. destruct H5; rewrite H in H5 at 2;
|
|
rewrite rev_app_distr in H5; simpl in H5;
|
|
assert (odd 0 = true).
|
|
assert (nth_error (tm_step n) (S (2*0) * 2^0) =
|
|
nth_error (tm_step n) (pred (S (2*0) * 2^0))).
|
|
rewrite H5. reflexivity. generalize H6.
|
|
apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
|
|
assert (nth_error (tm_step n) (S (2*0) * 2^0) =
|
|
nth_error (tm_step n) (pred (S (2*0) * 2^0))).
|
|
rewrite H5. reflexivity. generalize H6.
|
|
apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
|
|
assert ({b6=b1} + {~ b6=b1}). apply bool_dec. destruct H5. rewrite e0 in H.
|
|
replace (
|
|
(removelast (removelast (b3 :: b5 :: hd)) ++
|
|
[last (removelast (b3 :: b5 :: hd)) false]) ++
|
|
[b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b1 :: tl)
|
|
with (
|
|
(removelast (removelast (b3 :: b5 :: hd)) ++
|
|
[last (removelast (b3 :: b5 :: hd)) false] ++
|
|
[b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: nil)
|
|
++ [b1] ++ [b1] ++ [b1] ++ tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
apply Nat.lt_0_1.
|
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
(* on assigne les valeurs correctes aux deux extrémités *)
|
|
assert (b6 = b0). destruct b6; destruct b1; destruct b0.
|
|
reflexivity. contradiction n5. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n5. reflexivity. reflexivity.
|
|
rewrite H5 in H.
|
|
assert (last (removelast (b3 :: b5 :: hd)) false = b0).
|
|
destruct (last (removelast (b3 :: b5 :: hd)) false);
|
|
destruct b1; destruct b0.
|
|
reflexivity. contradiction n4. reflexivity. reflexivity.
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
reflexivity. contradiction n4. reflexivity. reflexivity.
|
|
rewrite H6 in H.
|
|
|
|
(* on étend hd *)
|
|
destruct hd. simpl in H. assert (odd 3 = true). reflexivity.
|
|
rewrite <- tm_step_pred with (n := n) (k := 0) in H7.
|
|
rewrite H in H7. simpl in H7. inversion H7. rewrite H9 in n1.
|
|
contradiction n1. reflexivity. simpl.
|
|
replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
|
|
assumption. apply Nat.lt_1_2. reflexivity.
|
|
rewrite app_removelast_last
|
|
with (l := removelast (removelast (b3::b5::b7::hd))) (d := false) in H.
|
|
pose (b8 := last (removelast (removelast (b3 :: b5 :: b7 :: hd))) false).
|
|
fold b8 in H. rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
|
|
|
|
|
|
|
|
|
|
False, True, True, False, True, False, False, True, True, False, False
|
|
|
|
Admitted.
|
|
|
|
|
|
TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
|
|
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
|
|
FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???)
|
|
TFT TFT FF TFT TFT (si on part sur 2 mod 8)
|
|
(idem en partant de la droite pour 6 mod 8)
|
|
Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* si on a ensuite le bloc précédent identique aux deux premiers de a
|
|
|
|
|
|
|
|
|
|
(* TODO : terminer avec une inversion sur la longueur de a ;
|
|
le dernier but vient de la destructuration initiale de a *)
|
|
|
|
|
|
|
|
F T | T F | T F ][ F T | F T T F
|
|
4n
|
|
|
|
ou F T | T F ][ F T | T F
|
|
4n ou 4n
|
|
|
|
F T F T T F F T T F T F (centre 4n+2 ET 4n : contra)
|
|
T F F T T F F T T F T F (centre : 4n+2)
|
|
F T F T T F F T T F F T (centre : 4n)
|
|
T F F T T F F T T F F T (cubes)
|
|
|
|
|
|
|
|
|
|
--> T F F T | T F ][ F T | T F F T (impossible : cubes)
|
|
--> F T F T | T F ][ F T | T F T F
|
|
|
|
Bilan : seulement deux cas possible de palindrome 8
|
|
F T | T F | T F ][ F T | F T | T F
|
|
4n+2 4n+2 (trivial)
|
|
|
|
F T | F T | T F ][ F T | T F | T F
|
|
4n (par examen des cinq premiers termes à gauche)
|
|
|
|
*)
|
|
|
|
|
|
Lemma tm_step_palindromic_length_12 :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ rev a ++ tl
|
|
-> 6 < length a
|
|
-> length (hd ++ a) mod 4 = 0.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
assert (J: even (length (hd ++ a)) = true).
|
|
assert (0 < length a).
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
assumption. generalize H0. generalize H.
|
|
apply tm_step_palindromic_even_center.
|
|
apply even_mod4 in J. destruct J. assumption.
|
|
|
|
rewrite <- firstn_skipn with (l := a) (n := length a - 4) in H.
|
|
rewrite rev_app_distr in H. rewrite <- app_assoc in H.
|
|
rewrite app_assoc in H.
|
|
assert (length (skipn (length a - 4) a) = 4). rewrite skipn_length.
|
|
replace (length a) with ((length a - 4) + 4) at 1. rewrite Nat.add_comm.
|
|
rewrite Nat.add_sub. reflexivity. rewrite Nat.add_comm.
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. reflexivity.
|
|
apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
assumption.
|
|
|
|
pose (hd' := hd ++ firstn (length a - 4) a). fold hd' in H.
|
|
pose (a' := skipn (length a - 4) a). fold a' in H.
|
|
rewrite <- app_assoc in H.
|
|
pose (tl' := rev (firstn (length a - 4) a) ++ tl). fold tl' in H.
|
|
|
|
assert (K: length (hd' ++ a') mod 4 = 0
|
|
\/ nth_error hd' (length hd' - 3) <> nth_error tl' 2).
|
|
fold a' in H1. generalize H1. generalize H.
|
|
apply tm_step_palindromic_length_8.
|
|
destruct K.
|
|
unfold hd' in H2. unfold a' in H2. rewrite <- app_assoc in H2.
|
|
rewrite firstn_skipn in H2. assumption.
|
|
|
|
rewrite <- firstn_skipn with (l := a) (n := length a - 4) in I.
|
|
rewrite app_length in I. rewrite H1 in I. rewrite Nat.add_comm in I.
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
|
|
destruct (firstn (length a - 4) a). inversion I. destruct l.
|
|
apply Nat.succ_lt_mono in I. inversion I. destruct l.
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
inversion I.
|
|
|
|
unfold hd' in H2. unfold tl' in H2.
|
|
rewrite nth_error_app2 in H2. rewrite nth_error_app1 in H2.
|
|
rewrite app_length in H2. rewrite Nat.add_comm in H2.
|
|
rewrite Nat.add_sub_swap in H2. rewrite Nat.add_sub in H2.
|
|
|
|
assert (K: forall m (u : list bool),
|
|
nth_error u m = nth_error (rev u) (length u - S m)).
|
|
intros. induction u. destruct m. reflexivity.
|
|
rewrite nth_error_None. apply Nat.le_0_l.
|
|
induction m. simpl. rewrite nth_error_app2. rewrite rev_length.
|
|
rewrite Nat.sub_0_r. rewrite Nat.sub_diag. reflexivity.
|
|
rewrite rev_length. rewrite Nat.sub_0_r. apply Nat.le_refl.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_proper_palindromic_center :
|
|
forall (m n k i: nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
-> length a = 2 ^ S (Nat.double m)
|
|
-> length (hd ++ a) = S (Nat.double k) * 2 ^ i
|
|
-> last hd false <> List.hd false tl
|
|
-> i = 2 ^ S (Nat.double m).
|
|
Proof.
|
|
intro m. induction m.
|
|
- intros n k i hd a tl. intros H I J K.
|
|
destruct a. inversion I. destruct a. inversion I. destruct a.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* JUNK
|
|
Lemma xxx : forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ map negb (rev a) ++ tl
|
|
-> length a = 4
|
|
-> even (length hd) = true.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a.
|
|
|
|
replace [b;b0;b1;b2] with ([b] ++ [b0] ++ [b1] ++ [b2]) in H at 1.
|
|
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
rewrite <- app_assoc in H.
|
|
|
|
replace (map negb (rev [b; b0; b1; b2]))
|
|
with ([negb b2] ++ [negb b1] ++ [negb b0] ++ [negb b]) in H.
|
|
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
rewrite <- app_assoc in H.
|
|
|
|
assert (0 < length [b]). apply Nat.lt_0_1.
|
|
assert (0 < length [b0]). apply Nat.lt_0_1.
|
|
assert (0 < length [b1]). apply Nat.lt_0_1.
|
|
assert (0 < length [b2]). apply Nat.lt_0_1.
|
|
assert (J: {even (length hd) = true}
|
|
+ {~ even (length hd) = true}). apply bool_dec.
|
|
|
|
destruct b; destruct b0; destruct b1; destruct b2.
|
|
- assert ([true]<>[true]). generalize H0.
|
|
generalize H. apply tm_step_cubefree.
|
|
contradiction H4. reflexivity.
|
|
- assert ([true]<>[true]). generalize H0.
|
|
generalize H. apply tm_step_cubefree.
|
|
contradiction H4. reflexivity.
|
|
- assert([true] ++ [false] <> [true] ++ [false]). rewrite app_assoc in H.
|
|
replace ( [true] ++ [false] ++ [true] ++ [negb true]
|
|
++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
|
|
with ( ([true] ++ [false]) ++ ([true] ++ [negb true])
|
|
++ ([negb false] ++ [negb true]) ++ [negb true] ++ tl) in H.
|
|
assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
|
|
generalize H4. generalize H. apply tm_step_cubefree.
|
|
reflexivity. contradiction H4. reflexivity.
|
|
- assert (even (length (hd ++ [true] ++ [true] ++ [false] ++ [false])) = true).
|
|
replace ( [true] ++ [true] ++ [false] ++ [false] ++ [negb false]
|
|
++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
|
|
with ( ([true] ++ [true] ++ [false] ++ [false]) ++ ([negb false]
|
|
++ [negb false] ++ [negb true] ++ [negb true]) ++ tl) in H.
|
|
assert (0 < length ([true] ++ [true] ++ [false] ++ [false])).
|
|
apply Nat.lt_0_succ. generalize H4. generalize H. apply tm_step_square_pos.
|
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
|
reflexivity.
|
|
rewrite app_length in H4. simpl in H4.
|
|
rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
|
|
rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
|
|
rewrite Nat.add_0_r in H4.
|
|
rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
|
|
rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
|
|
rewrite H4. reflexivity.
|
|
- destruct J. assumption.
|
|
rewrite not_true_iff_false in n0.
|
|
|
|
assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3).
|
|
apply odd_mod4. rewrite <- Nat.negb_even. rewrite n0. reflexivity.
|
|
destruct M.
|
|
+ replace ( [true] ++ [false] ++ [true] ++ [true]
|
|
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
|
|
with ( ([true] ++ [false] ++ [true] ++ [true])
|
|
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
|
|
in H.
|
|
assert (exists (x:bool), firstn 2 [true;false;true;true] = [x;x]).
|
|
generalize H4. generalize I. generalize H.
|
|
apply tm_step_factor4_1mod4.
|
|
destruct H5. inversion H5. inversion H8.
|
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
|
reflexivity.
|
|
+ replace ( hd ++ [true] ++ [false] ++ [true] ++ [true]
|
|
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
|
|
with ( (hd ++ [true] ++ [false] ++ [true] ++ [true])
|
|
++ ([negb true] ++ [negb true] ++ [negb false] ++ [negb true]) ++ tl )
|
|
in H.
|
|
assert (exists (x:bool), skipn 2 [false;false;true;false] = [x;x]).
|
|
assert (length (hd ++ [true]++[false]++[true]++[true]) mod 4 = 3).
|
|
rewrite app_length. rewrite Nat.add_mod. rewrite H4. reflexivity.
|
|
easy. generalize H5.
|
|
assert (length [false;false;true;false]=4). reflexivity.
|
|
generalize H6. generalize H. apply tm_step_factor4_3mod4.
|
|
destruct H5. inversion H5. inversion H8.
|
|
rewrite <- app_assoc. reflexivity.
|
|
- assert([true] ++ [false] <> [true] ++ [false]).
|
|
replace ( [true] ++ [false] ++ [true] ++ [false] ++ [negb false]
|
|
++ [negb true] ++ [negb false] ++ [negb true] ++ tl)
|
|
with ( ([true] ++ [false]) ++ ([true] ++ [false])
|
|
++ ([negb false] ++ [negb true])
|
|
++ [negb false] ++ [negb true] ++ tl) in H.
|
|
assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
|
|
generalize H4. generalize H. apply tm_step_cubefree.
|
|
reflexivity. contradiction H4. reflexivity.
|
|
- destruct J. assumption. rewrite not_true_iff_false in n0.
|
|
|
|
|
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* TODO: bloqué
|
|
|
|
Lemma tm_step_proper_palindrome_center :
|
|
forall (m n k : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
-> length a = 2^(Nat.double m) (* palindrome non propre *)
|
|
-> skipn (length hd - length a) hd = rev (firstn (length a) tl).
|
|
Proof.
|
|
induction m; intros n k hd a tl; intros H I.
|
|
- simpl in I. destruct a. inversion I. destruct a.
|
|
|
|
(* proof that hd is not nil *)
|
|
destruct hd. assert (odd 0 = true).
|
|
assert (nth_error (tm_step n) (S (2*0) * 2^0)
|
|
= nth_error (tm_step n) (pred (S (2*0) * 2^0))).
|
|
rewrite H. reflexivity. generalize H0.
|
|
assert (S (2*0) * 2^0 < 2^n). destruct n. inversion H.
|
|
rewrite Nat.mul_0_r. rewrite Nat.mul_1_l.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_0_succ.
|
|
generalize H1. apply tm_step_pred. inversion H0.
|
|
|
|
(* proof that tl is not nil *)
|
|
destruct tl. destruct n.
|
|
assert (tm_step 0 = rev (tm_step 0)). reflexivity.
|
|
rewrite H in H0 at 2. rewrite rev_app_distr in H0.
|
|
simpl in H0. inversion H0. rewrite <- tm_step_lemma in H.
|
|
assert (rev (tm_morphism (tm_step n)) = rev (tm_morphism (tm_step n))).
|
|
reflexivity. rewrite H in H0 at 2. rewrite tm_morphism_rev in H0.
|
|
rewrite rev_app_distr in H0. simpl in H0.
|
|
destruct (map negb (rev (tm_step n))). inversion H0. simpl in H0.
|
|
inversion H0. apply no_fixpoint_negb in H3. contradiction H3.
|
|
|
|
(* proof that b <> b1 *)
|
|
assert (J: {b=b1} + {~ b=b1}). apply bool_dec. destruct J.
|
|
rewrite e in H.
|
|
replace (rev [b1]) with ([b1]) in H.
|
|
replace (b1::tl) with ([b1] ++ tl) in H.
|
|
assert ([b1] <> [b1]). assert (0 < length [b1]). apply Nat.lt_0_1.
|
|
generalize H0. generalize H. apply tm_step_cubefree.
|
|
contradiction H0. reflexivity. reflexivity. reflexivity.
|
|
|
|
(* proof that b <> last (b0::hd) false *)
|
|
assert (J: {b=last (b0::hd) false} + {~ b=last (b0::hd) false}).
|
|
apply bool_dec. destruct J.
|
|
rewrite app_removelast_last with (l := b0::hd) (d := false) in H.
|
|
rewrite <- e in H. rewrite <- app_assoc in H.
|
|
replace (rev [b]) with ([b]) in H.
|
|
assert ([b] <> [b]). assert (0 < length [b]). apply Nat.lt_0_1.
|
|
generalize H0. generalize H. apply tm_step_cubefree.
|
|
contradiction H0. reflexivity. reflexivity. easy.
|
|
|
|
(* proof that b1 = last (b0 :: hd) false *)
|
|
assert (b1 = last (b0 :: hd) false).
|
|
destruct b; destruct b1; destruct (last (b0::hd) false).
|
|
reflexivity. contradiction n0. reflexivity.
|
|
contradiction n1. reflexivity. reflexivity.
|
|
reflexivity. contradiction n1. reflexivity.
|
|
contradiction n0. reflexivity. reflexivity.
|
|
rewrite H0.
|
|
|
|
rewrite <- rev_involutive at 1. rewrite <- firstn_rev.
|
|
rewrite app_removelast_last with (l := b0::hd) (d := false) at 1.
|
|
rewrite rev_app_distr. reflexivity.
|
|
easy. inversion I.
|
|
- assert (J: even (length (hd ++ a)) = true).
|
|
assert (0 < length a). rewrite I.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
|
generalize H0. generalize H. apply tm_step_palindromic_even_center.
|
|
|
|
assert (H' := H).
|
|
|
|
(* proof that 0 < n *)
|
|
destruct n.
|
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
|
rewrite H in H0 at 2. rewrite app_length in H0.
|
|
rewrite app_length in H0. rewrite I in H0.
|
|
assert (1 < 2^Nat.double(S m)).
|
|
rewrite <- Nat.pow_0_r with (a := 2) at 1.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
|
rewrite Nat.double_S. apply Nat.lt_0_succ.
|
|
assert (0 <= length (rev a ++ tl)). apply le_0_n.
|
|
assert (1 < 2 ^ Nat.double (S m) + length (rev a ++ tl)).
|
|
rewrite <- Nat.add_0_r at 1. generalize H2. generalize H1.
|
|
apply Nat.add_lt_le_mono.
|
|
assert (0 <= length hd). apply le_0_n.
|
|
assert (1 < length (tm_step 0)). rewrite <- Nat.add_0_l at 1.
|
|
rewrite H0. generalize H3. generalize H4.
|
|
apply Nat.add_le_lt_mono.
|
|
simpl in H5. apply Nat.lt_irrefl in H5. contradiction H5.
|
|
|
|
rewrite <- tm_step_lemma in H.
|
|
assert (K: even (length a) = true). rewrite Nat.double_S in I.
|
|
rewrite Nat.pow_succ_r in I. rewrite I. rewrite Nat.even_mul.
|
|
reflexivity. apply le_0_n.
|
|
|
|
assert (L: even (length hd) = true).
|
|
rewrite app_length in J. rewrite Nat.even_add in J.
|
|
rewrite K in J. destruct (Nat.even (length hd)).
|
|
reflexivity. inversion J.
|
|
|
|
assert (M: hd = tm_morphism (firstn (Nat.div2 (length hd))
|
|
(tm_step n))).
|
|
generalize L. generalize H. apply tm_morphism_app2.
|
|
|
|
assert (N: a ++ rev a ++ tl
|
|
= tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
|
|
generalize L. generalize H. apply tm_morphism_app3.
|
|
symmetry in N.
|
|
|
|
assert (O: a = tm_morphism (firstn (Nat.div2 (length a))
|
|
(skipn (Nat.div2 (length hd)) (tm_step n)))).
|
|
generalize K. generalize N. apply tm_morphism_app2.
|
|
|
|
assert (P: rev a ++ tl = tm_morphism (skipn (Nat.div2 (length a))
|
|
(skipn (Nat.div2 (length hd)) (tm_step n)))).
|
|
generalize K. generalize N. apply tm_morphism_app3.
|
|
symmetry in P.
|
|
|
|
assert (even (length (rev a)) = true). rewrite rev_length. assumption.
|
|
|
|
assert (R: tl = tm_morphism (skipn (Nat.div2 (length (rev a)))
|
|
(skipn (Nat.div2 (length a))
|
|
(skipn (Nat.div2 (length hd)) (tm_step n))))).
|
|
generalize H0. generalize P. apply tm_morphism_app3.
|
|
|
|
rewrite M in H. rewrite O in H. rewrite R in H.
|
|
rewrite tm_morphism_rev in H. rewrite <- tm_morphism_app in H.
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
rewrite <- tm_morphism_eq in H.
|
|
pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)).
|
|
pose (a' := firstn (Nat.div2 (length a))
|
|
(skipn (Nat.div2 (length hd)) (tm_step n))).
|
|
pose (tl' := skipn (Nat.div2 (length (rev a)))
|
|
(skipn (Nat.div2 (length a))
|
|
(skipn (Nat.div2 (length hd)) (tm_step n)))).
|
|
fold hd' in H. fold a' in H. fold tl' in H.
|
|
|
|
assert (I': length a' = 2^S (Nat.double m)). unfold a'.
|
|
rewrite firstn_length_le. rewrite I. rewrite Nat.double_S.
|
|
rewrite Nat.pow_succ_r. rewrite Nat.div2_double. reflexivity.
|
|
apply le_0_n. rewrite skipn_length.
|
|
rewrite Nat.mul_le_mono_pos_r with (p := 2).
|
|
rewrite Nat.mul_comm. rewrite <- Nat.add_0_r at 1.
|
|
replace 0 with (Nat.b2n (Nat.odd (length a))) at 2.
|
|
rewrite <- Nat.div2_odd. rewrite Nat.mul_sub_distr_r.
|
|
replace (length (tm_step n) * 2) with (length (tm_step (S n))).
|
|
replace (Nat.div2 (length hd) * 2) with (length hd).
|
|
rewrite H'. rewrite app_length. rewrite Nat.add_sub_swap.
|
|
rewrite Nat.sub_diag. simpl. rewrite app_length.
|
|
rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l.
|
|
apply Nat.le_0_l. apply Nat.le_refl.
|
|
rewrite Nat.mul_comm. symmetry. rewrite <- Nat.add_0_r at 1.
|
|
replace 0 with (Nat.b2n (Nat.odd (length hd))) at 2.
|
|
rewrite <- Nat.div2_odd. reflexivity.
|
|
rewrite <- Nat.negb_even. rewrite L. reflexivity.
|
|
rewrite tm_build. rewrite app_length. rewrite Nat.mul_comm.
|
|
simpl. rewrite Nat.add_0_r. rewrite map_length. reflexivity.
|
|
rewrite <- Nat.negb_even. rewrite K. reflexivity.
|
|
apply Nat.lt_0_2.
|
|
|
|
assert (K': even (length a') = true). rewrite I'.
|
|
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
|
|
apply le_0_n.
|
|
*)
|
|
|
|
(* le motif XX YY -> préfixe congru à 5 ou à 7 modulo 8
|
|
donc double du préfixe congru à 2 modulo 4
|
|
compatible avec ???
|
|
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.
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
(* réduire par la réciproque du morphisme *)
|
|
|
|
|
|
|
|
|
|
Lemma tm_morphism_app : forall (l1 l2 : list bool),
|
|
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
|
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
|
tm_morphism l = hd ++ tl
|
|
-> even (length hd) = true
|
|
-> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
|
|
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
|
|
tm_morphism l = hd ++ tl
|
|
-> even (length hd) = true
|
|
-> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Lemma tm_step_proper_palindrome_center :
|
|
forall (n k m : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
-> length a = 2^(Nat.double m) (* palindrome non propre *)
|
|
-> List.last hd false = List.hd false tl.
|
|
Proof.
|
|
induction m.
|
|
- intros. simpl in H0.
|
|
destruct a. inversion H0. destruct a.
|
|
|
|
(* proof that hd is not nil *)
|
|
destruct hd. assert (odd 0 = true).
|
|
assert (nth_error (tm_step n) (S (2*0) * 2^0)
|
|
= nth_error (tm_step n) (pred (S (2*0) * 2^0))).
|
|
rewrite H. reflexivity. generalize H1.
|
|
assert (S (2*0) * 2^0 < 2^n). destruct n. inversion H.
|
|
rewrite Nat.mul_0_r. rewrite Nat.mul_1_l.
|
|
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_0_succ.
|
|
generalize H2. apply tm_step_pred. inversion H1.
|
|
|
|
(* proof that tl is not nil *)
|
|
destruct tl. destruct n.
|
|
assert (tm_step 0 = rev (tm_step 0)). reflexivity.
|
|
rewrite H in H1 at 2. rewrite rev_app_distr in H1.
|
|
simpl in H1. inversion H1. rewrite <- tm_step_lemma in H.
|
|
assert (rev (tm_morphism (tm_step n)) = rev (tm_morphism (tm_step n))).
|
|
reflexivity. rewrite H in H1 at 2. rewrite tm_morphism_rev in H1.
|
|
rewrite rev_app_distr in H1. simpl in H1.
|
|
destruct (map negb (rev (tm_step n))). inversion H1. simpl in H1.
|
|
inversion H1. destruct b; inversion H4.
|
|
|
|
(* proof that b <> b1 *)
|
|
assert (I: {b=b1} + {~ b=b1}). apply bool_dec. destruct I.
|
|
rewrite e in H.
|
|
replace (rev [b1]) with ([b1]) in H.
|
|
replace (b1::tl) with ([b1] ++ tl) in H.
|
|
assert ([b1] <> [b1]). assert (0 < length [b1]). apply Nat.lt_0_1.
|
|
generalize H1. generalize H. apply tm_step_cubefree.
|
|
contradiction H1. reflexivity. reflexivity. reflexivity.
|
|
|
|
(* proof that b <> last (b0::hd) false *)
|
|
assert (I: {b=last (b0::hd) false} + {~ b=last (b0::hd) false}).
|
|
apply bool_dec. destruct I.
|
|
rewrite app_removelast_last with (l := b0::hd) (d := false) in H.
|
|
rewrite <- e in H. rewrite <- app_assoc in H.
|
|
replace (rev [b]) with ([b]) in H.
|
|
assert ([b] <> [b]). assert (0 < length [b]). apply Nat.lt_0_1.
|
|
generalize H1. generalize H. apply tm_step_cubefree.
|
|
contradiction H1. reflexivity. reflexivity. easy.
|
|
|
|
(* final part of the proof *)
|
|
destruct b; destruct b1; destruct (last (b0::hd) false).
|
|
reflexivity. contradiction n0. reflexivity.
|
|
contradiction n1. reflexivity. reflexivity.
|
|
reflexivity. contradiction n1. reflexivity.
|
|
contradiction n0. reflexivity. reflexivity.
|
|
inversion H0.
|
|
|
|
- intros.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
induction m.
|
|
- intros. simpl in H0.
|
|
|
|
assert (I: a = (List.hd false a)::nil).
|
|
destruct a. inversion H0. destruct a. reflexivity. inversion H0.
|
|
|
|
assert (N: n = 0 \/ 0 < n). apply Nat.eq_0_gt_0_cases.
|
|
destruct N as [N|N]. rewrite N in H.
|
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
|
rewrite H in H1 at 2. rewrite app_length in H1.
|
|
rewrite app_length in H1. rewrite app_length in H1.
|
|
rewrite I in H1.
|
|
rewrite Nat.add_1_l in H1. simpl in H1.
|
|
rewrite Nat.add_comm in H1.
|
|
rewrite Nat.add_succ_l in H1. rewrite Nat.add_succ_l in H1.
|
|
apply Nat.succ_inj in H1. apply O_S in H1. contradiction H1.
|
|
|
|
assert (J: hd <> nil).
|
|
assert ({hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
destruct H1. rewrite e in H.
|
|
|
|
simpl in H. rewrite app_assoc in H.
|
|
assert (count_occ bool_dec (a++rev a) true
|
|
= count_occ bool_dec (a++rev a) false).
|
|
assert (even (length (a++rev a))=true). rewrite I. reflexivity.
|
|
generalize H1. generalize H. apply tm_step_count_occ.
|
|
rewrite I in H1.
|
|
|
|
rewrite tm_step_head_1 in H. rewrite <- app_assoc in H.
|
|
inversion H. rewrite I in H3. inversion H3.
|
|
rewrite <- H4 in H1. inversion H1.
|
|
assumption.
|
|
|
|
assert (K: tl <> nil).
|
|
assert ({tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
|
|
destruct H1. rewrite e in H.
|
|
|
|
assert (count_occ bool_dec (hd++a++rev a) true
|
|
= count_occ bool_dec (hd++a++rev a) false).
|
|
assert (even (length (hd++a++rev a))=true).
|
|
rewrite app_nil_r in H.
|
|
rewrite <- H. rewrite tm_size_power2.
|
|
destruct n. inversion N. rewrite Nat.pow_succ_r.
|
|
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
|
|
rewrite app_assoc in H. rewrite app_assoc in H.
|
|
replace ((hd++a)++rev a) with (hd++a++rev a) in H.
|
|
generalize H1. generalize H. apply tm_step_count_occ.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
assert (count_occ bool_dec hd true
|
|
= count_occ bool_dec hd false).
|
|
assert (even (length hd)=true).
|
|
assert (even (length (tm_step n)) = true).
|
|
rewrite tm_size_power2. destruct n. inversion N. rewrite Nat.pow_succ_r.
|
|
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
|
|
rewrite H in H2. rewrite app_length in H2.
|
|
rewrite Nat.even_add in H2. rewrite I in H2. simpl in H2.
|
|
destruct (Nat.even (length hd)). reflexivity. inversion H2.
|
|
generalize H2. generalize H. apply tm_step_count_occ.
|
|
|
|
rewrite count_occ_app in H1. symmetry in H1.
|
|
rewrite count_occ_app in H1. rewrite H2 in H1.
|
|
rewrite Nat.add_cancel_l in H1.
|
|
destruct a. inversion H0. destruct a. destruct b.
|
|
inversion H1. inversion H1. inversion H0.
|
|
assumption.
|
|
|
|
(* utiliser ici cubefree *)
|
|
assert (last hd false = true).
|
|
assert ({last hd false=true} + {~ last hd false=true}). apply bool_dec.
|
|
destruct H1. assumption.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
assert (List.hd false (List.tl (tm_step n)) = nth 1 (tm_step n) false).
|
|
|
|
|
|
|
|
replace (rev a) with a in H.
|
|
|
|
assert (last hd false = negb (List.hd false a)).
|
|
assert ({last hd false=List.hd false a}
|
|
+ {~ last hd false=List.hd false a}). apply bool_dec.
|
|
destruct H1.
|
|
replace hd with ((removelast hd) ++ a) in H.
|
|
rewrite <- app_assoc in H.
|
|
assert (0 < length a). rewrite H0. apply Nat.lt_0_1.
|
|
assert (a<>a). generalize H1. generalize H. apply tm_step_cubefree.
|
|
contradiction H2. reflexivity.
|
|
|
|
rewrite I. rewrite <- e. symmetry. apply app_removelast_last.
|
|
|
|
|
|
|
|
|
|
|
|
/\ length a = 2^m /\ length (hd ++ a) = k
|
|
/\ last
|
|
)
|
|
-> (tm_step (S (S n)) =
|
|
(tm_morphism (tm_morphism hd)) ++
|
|
|
|
|
|
(*
|
|
Seules les puissances paires de 2 (16, 64, etc.) sont des longueurs
|
|
de palindromes propres (palindromes piles de cette taille pas
|
|
encapsulés dans des plus gros palindromes) :
|
|
|
|
Positions du centre pour 16 :
|
|
|
|
In [25]: [ i+32 for i in range(32, 800) if test_proper_palidrome(T
|
|
...: , i, 64) ]
|
|
Out[25]: [96, 160, 352, 416, 480, 544, 608, 672]
|
|
|
|
In [26]: [ i+8 for i in range(8, 300) if test_proper_palidrome(T,
|
|
...: i, 16) ]
|
|
Out[26]: [24, 40, 88, 104, 120, 136, 152, 168, 216, 232, 280, 296]
|
|
In [27]: [ i+2 for i in range(2, 100) if test_proper_palidrome(T,
|
|
...: i, 4) ]
|
|
Out[27]: [6, 10, 22, 26, 30, 34, 38, 42, 54, 58, 70, 74, 86, 90, 94, 98]
|
|
|
|
Idée de lemme : si k est une position centrale pour un palindrome propre
|
|
de taille 2^j, alors 4*k est une position centrale pour un palindrome
|
|
propre de taille 2^(S (S j))
|
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
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. rewrite tm_step_odd_step. rewrite <- tm_build.
|
|
rewrite Nat.double_S. 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
-
|
|
|
|
|
|
*)
|
|
|
|
(* TODO: reprendre tous les lemmes hd ++ a ++ rev a ++ tl
|
|
et trouver un équivalent pour hd ++ a ++ map negb (rev a) ++ tl *)
|
|
|
|
(*
|
|
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.
|
|
|
|
|
|
|
|
|
|
*)
|