From 5253fb526d7e4d9c9b45657b6c4dd540dfc13624 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Feb 2023 18:44:14 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 1410 +-------------------------------------------- 1 file changed, 2 insertions(+), 1408 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index dfab18d..294430a 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2097,1417 +2097,11 @@ Qed. - destruct m. left. - - assert (K: length a mod 4 = 0). rewrite J. reflexivity. - assert (L: length hd mod 4 = 0). - generalize K. generalize I. generalize H. - apply tm_step_palindromic_length_12_prefix. - - assert (M: hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n)))))). - generalize K. generalize I. generalize H. - apply tm_step_palindromic_even_morphism2. - - destruct M as [N O]. destruct O as [O P]. - rewrite N in H. rewrite O in H. rewrite P in H. - (* - rewrite tm_morphism_twice_rev in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - *) - - pose (hd' := (firstn (length hd / 4) (tm_step (pred (pred n))))). - pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step (pred (pred n)))))). - pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step (pred (pred n))))). - fold hd' in H. fold a' in H. fold tl' in H. - - -Lemma tm_step_palindromic_power2_even : - forall (m n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 - <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. -Proof. - intros m n hd a tl. intros H I J. - - - - - -Lemma xxx : - forall m : nat, - (forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0) - -> (forall (n' : nat) (hd' a' tl' : list bool), - tm_step n' = hd' ++ a' ++ (rev a') ++ tl' - -> 6 < length a' - -> length a' = 2^(Nat.double (S m)) - -> length (hd' ++ a') mod (2 ^ (pred (Nat.double (S m)))) = 0). -Proof. - intro m. intro IH. - intros n hd a tl. intros H I J. - rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl). - rewrite <- pred_Sn. - - destruct m. rewrite J in I. inversion I. inversion H1. - inversion H3. inversion H5. inversion H7. - - assert (W: (length a) mod 4 = 0). - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.mul_assoc in J. - replace (2*2) with 4 in J. rewrite J. - rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. - - assert ( - hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n)))))). - generalize W. generalize I. generalize H. - apply tm_step_palindromic_even_morphism2. - destruct H0 as [K H0]. destruct H0 as [L M]. - - assert (V: 3 < n). generalize I. generalize H. - apply tm_step_palindromic_length_12_n. - destruct n. inversion V. destruct n. inversion V. inversion H1. - - rewrite K in H. rewrite L in H. rewrite M in H. - rewrite tm_morphism_twice_rev in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H. - rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H. - rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H. - - pose (hd' := (firstn (length hd / 4) (tm_step n))). - pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))). - pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))). - fold hd' in H. fold a' in H. fold tl' in H. - - rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K. - rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L. - fold hd' in K. fold a' in L. - assert (N: length a = length a). reflexivity. rewrite L in N at 2. - rewrite tm_morphism_length in N. rewrite tm_morphism_length in N. - rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. - assert (O: length hd = length hd). reflexivity. rewrite K in O at 2. - rewrite tm_morphism_length in O. rewrite tm_morphism_length in O. - rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O. - - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. rewrite <- app_length. - rewrite Nat.mul_comm. rewrite Nat.div_mul. - apply IH with (n := n) (tl := tl'). assumption. - - - - - - - - replace (2^ pred (Nat.double 2)) with (4*2). - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - rewrite Nat.mul_eq_0. right. rewrite <- app_length. - - assert (U: even (length (hd' ++ a')) = true). - assert (0 < length a'). - apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. - rewrite N in I. - rewrite <- Nat.mul_1_r in I at 1. - rewrite <- Nat.mul_lt_mono_pos_l in I. - apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ. - generalize H0. generalize H. apply tm_step_palindromic_even_center. - - - - -Lemma tm_step_palindromic_even_morphism2 : - forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> (length a) mod 4 = 0 - -> hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n))))). - - - rewrite Nat.double_S. - replace (pred (S (S (Nat.double m)))) with (S (S (pred (Nat.double m)))). - rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. - replace (2*2) with 4. - -Lemma tm_step_palindromic_power2_even : - forall (m n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 - <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. - - - -Lemma tm_step_palindromic_power2_even : - forall (m n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 - - - - - -Lemma xxx : - forall (m n k : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0. -Proof. - intros m n k hd a tl. intros H I J. - assert (R := H). - - destruct m. rewrite J in I. inversion I. inversion H1. - destruct m. rewrite J in I. inversion I. inversion H1. - inversion H3. inversion H5. inversion H7. - - generalize dependent a. generalize dependent hd. - induction m. intros hd a H I J H'. - - assert (W: (length a) mod 4 = 0). - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.mul_assoc in J. - replace (2*2) with 4 in J. rewrite J. - rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. - - assert ( - hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n)))))). - generalize W. generalize I. generalize H. - apply tm_step_palindromic_even_morphism2. - destruct H0 as [K H0]. destruct H0 as [L M]. - - assert (V: 3 < n). generalize I. generalize H. - apply tm_step_palindromic_length_12_n. - destruct n. inversion V. destruct n. inversion V. inversion H1. - - rewrite K in H. rewrite L in H. rewrite M in H. - rewrite tm_morphism_twice_rev in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H. - rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H. - rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H. - - pose (hd' := (firstn (length hd / 4) (tm_step n))). - pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))). - pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))). - fold hd' in H. fold a' in H. fold tl' in H. - - (* - assert (U: even (length (hd ++ a)) = true). - 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. - generalize I. generalize H'. - apply tm_step_palindromic_even_center. - *) - - rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K. - rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L. - fold hd' in K. fold a' in L. - assert (N: length a = length a). reflexivity. rewrite L in N at 2. - rewrite tm_morphism_length in N. rewrite tm_morphism_length in N. - rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. - assert (O: length hd = length hd). reflexivity. rewrite K in O at 2. - rewrite tm_morphism_length in O. rewrite tm_morphism_length in O. - rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O. - - replace (2^ pred (Nat.double 2)) with (4*2). - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - rewrite Nat.mul_eq_0. right. rewrite <- app_length. - - assert (U: even (length (hd' ++ a')) = true). - assert (0 < length a'). - apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. - rewrite N in I. - rewrite <- Nat.mul_1_r in I at 1. - rewrite <- Nat.mul_lt_mono_pos_l in I. - apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ. - generalize H0. generalize H. apply tm_step_palindromic_even_center. - - replace (length (hd' ++ a')) - with (2 * Nat.div2 (length (hd' ++ a')) - + Nat.b2n (Nat.odd (length (hd' ++ a')))). - rewrite <- Nat.negb_even. rewrite U. rewrite Nat.add_0_r. - rewrite Nat.mul_mod. reflexivity. easy. symmetry. apply Nat.div2_odd. - easy. easy. reflexivity. reflexivity. reflexivity. - - intros hd a H I J H'. rewrite Nat.double_S. - replace (pred (S (S (Nat.double (S (S m)))))) - with (S (S (pred (Nat.double (S (S m)))))). - rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - - assert (W: (length a) mod 4 = 0). - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.mul_assoc in J. - replace (2*2) with 4 in J. rewrite J. - rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. - - assert ( - hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n)))))). - generalize W. generalize I. generalize H. - apply tm_step_palindromic_even_morphism2. - destruct H0 as [K H0]. destruct H0 as [L M]. - - assert (V: 3 < n). generalize I. generalize H. - apply tm_step_palindromic_length_12_n. - destruct n. inversion V. destruct n. inversion V. inversion H1. - - rewrite K in H. rewrite L in H. rewrite M in H. - rewrite tm_morphism_twice_rev in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. - rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H. - rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H. - rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H. - rewrite <- pred_Sn in K. rewrite <- pred_Sn in K. - rewrite <- pred_Sn in L. rewrite <- pred_Sn in L. - - pose (hd' := (firstn (length hd / 4) (tm_step n))). - pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))). - pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))). - fold hd' in H. fold a' in H. fold tl' in H. - fold hd' in K. fold a' in L. - - assert (N: length a = length a). reflexivity. rewrite L in N at 2. - rewrite tm_morphism_length in N. rewrite tm_morphism_length in N. - rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N. - assert (O: length hd = length hd). reflexivity. rewrite K in O at 2. - rewrite tm_morphism_length in O. rewrite tm_morphism_length in O. - rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O. - - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - rewrite Nat.mul_eq_0. right. rewrite <- app_length. - apply IHm. - - -Lemma tm_step_palindromic_power2_even : - forall (m n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a = 2^(Nat.double m) - -> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0 - <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. - - - rewrite Nat.mul_comm. rewrite Nat.div_mul. - rewrite <- app_length. apply IHm with (n := S (S n)) (tl := tl'). - - - (* - generalize dependent a. generalize dependent hd. - generalize dependent tl. generalize dependent n. - *) - induction m. - - - rewrite tm_step_palindromic_power2_even with (n := S (S n)) (tl := tl). - rewrite app_length. rewrite N. - rewrite Nat.mul_comm. rewrite Nat.div_add. - rewrite O. rewrite Nat.mul_comm. rewrite Nat.div_mul. - rewrite <- app_length. - assert (even (length (hd' ++ a')) = true). - assert (0 < length a'). - apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. - rewrite N in I. - rewrite <- Nat.mul_1_r in I at 1. - rewrite <- Nat.mul_lt_mono_pos_l in I. - apply Nat.lt_succ_l in I. assumption. - apply Nat.lt_0_succ. generalize H0. generalize H. - apply tm_step_palindromic_even_center. - replace (length (hd' ++ a')) - with (2 * Nat.div2 (length (hd' ++ a')) - + Nat.b2n (Nat.odd (length (hd' ++ a')))). - rewrite <- Nat.negb_even. rewrite H0. - rewrite Nat.add_0_r. - rewrite Nat.mul_mod. reflexivity. simpl. - apply Nat.neq_succ_0. symmetry. apply Nat.div2_odd. - easy. easy. assumption. assumption. assumption. - (* intros n V tl hd hd' K O a a' tl' H I J R W L M N. *) - (* - replace (S (S (S m))) with (pred (S (S (S (S m))))). - rewrite Nat.double_S. - replace (S (S m)) with (pred (S (S (S m)))). - replace (pred (S (S (Nat.double (pred (S (S (S m)))))))) - with (S (S (pred (Nat.double (pred (S (S (S m)))))))). - rewrite Nat.pow_succ_r. - rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - replace (length (hd ++ a)) - with ((length ((tm_morphism (tm_morphism hd)) - ++ (tm_morphism (tm_morphism a))))/4). - rewrite <- tm_step_palindromic_power2_even - with (n := S (S (S (S n)))) (tl := tm_morphism (tm_morphism tl)). - rewrite Nat.double_S. rewrite Nat.double_S. - *) - - - - rewrite tm_step_palindromic_power2_even with (n := (S (S n))) (tl := tl). - rewrite <- pred_Sn. - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. - rewrite Nat.mul_comm. rewrite Nat.div_mul. - rewrite <- app_length. apply IHm with (n := S (S n)) (tl := tl'). - - - - rewrite Nat.double_S. - replace (pred (S (S (Nat.double (S (S m)))))) - with (S (S (pred (Nat.double (S (S m)))))). - rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - rewrite app_length. rewrite O. rewrite N. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - rewrite Nat.mul_eq_0. right. rewrite <- app_length. - apply IHm with (n := n) (tl := tl'). - - - - - induction m. - - (* intros n V tl hd hd' K O a a' tl' H I J R W L M N. *) - rewrite tm_step_palindromic_power2_even with (n := S (S n)) (tl := tl). - rewrite app_length. rewrite N. - rewrite Nat.mul_comm. rewrite Nat.div_add. - rewrite O. rewrite Nat.mul_comm. rewrite Nat.div_mul. - rewrite <- app_length. - assert (even (length (hd' ++ a')) = true). - assert (0 < length a'). - apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I. - rewrite N in I. - rewrite <- Nat.mul_1_r in I at 1. - rewrite <- Nat.mul_lt_mono_pos_l in I. - apply Nat.lt_succ_l in I. assumption. - apply Nat.lt_0_succ. generalize H0. generalize H. - apply tm_step_palindromic_even_center. - replace (length (hd' ++ a')) - with (2 * Nat.div2 (length (hd' ++ a')) - + Nat.b2n (Nat.odd (length (hd' ++ a')))). - rewrite <- Nat.negb_even. rewrite H0. - rewrite Nat.add_0_r. - rewrite Nat.mul_mod. reflexivity. simpl. - apply Nat.neq_succ_0. symmetry. apply Nat.div2_odd. - easy. easy. assumption. assumption. assumption. - - (* intros n V tl hd hd' K O a a' tl' H I J R W L M N. *) - (* - replace (S (S (S m))) with (pred (S (S (S (S m))))). - rewrite Nat.double_S. - replace (S (S m)) with (pred (S (S (S m)))). - replace (pred (S (S (Nat.double (pred (S (S (S m)))))))) - with (S (S (pred (Nat.double (pred (S (S (S m)))))))). - rewrite Nat.pow_succ_r. - rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - replace (length (hd ++ a)) - with ((length ((tm_morphism (tm_morphism hd)) - ++ (tm_morphism (tm_morphism a))))/4). - rewrite <- tm_step_palindromic_power2_even - with (n := S (S (S (S n)))) (tl := tm_morphism (tm_morphism tl)). - rewrite Nat.double_S. rewrite Nat.double_S. - *) - - rewrite tm_step_palindromic_power2_even with (n := (S (S n))) (tl := tl). - rewrite <- pred_Sn. - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. - rewrite Nat.mul_comm. rewrite Nat.div_mul. - rewrite <- app_length. apply IHm with (n := S (S n)) (tl := tl'). - - - - rewrite Nat.double_S. - replace (pred (S (S (Nat.double (S (S m)))))) - with (S (S (pred (Nat.double (S (S m)))))). - rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - rewrite app_length. rewrite O. rewrite N. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - rewrite Nat.mul_eq_0. right. rewrite <- app_length. - apply IHm with (n := n) (tl := tl'). - - - - - - - -Nat.div2_odd: forall a : nat, a = 2 * Nat.div2 a + Nat.b2n (Nat.odd a) - - - -Nat.div_str_pos: forall a b : nat, 0 < b <= a -> 0 < a / b - - - 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. - generalize I. -Theorem tm_step_palindromic_even_center : - forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 0 < length a - -> even (length (hd ++ a)) = true. - - - - rewrite <- Nat.mul_cancel_l with (p := 4). - rewrite <- Nat.mul_mod_distr_l. - - replace (4 * (length (hd ++ a) / 4)) - with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4). - rewrite <- Nat.div_mod_eq. assumption. - rewrite H0. rewrite Nat.add_0_r. reflexivity. - rewrite app_length. - replace (4 * (length (hd ++ a) / 4)) - with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4). - rewrite <- Nat.div_mod_eq. assumption. - rewrite H0. rewrite Nat.add_0_r. reflexivity. - - - - - - generalize dependent a. - generalize dependent hd. - induction m. - - intros hd hd' K O a a' tl'. intros H I J W L M N. - assert (even (length (hd' ++ a')) = true). - assert (0 < length a'). rewrite J in N. - replace (2 ^ (Nat.double 2)) with (4*4) in N. - rewrite Nat.mul_cancel_l in N. rewrite <- N. - apply Nat.lt_0_succ. easy. reflexivity. generalize H0. - generalize H. apply tm_step_palindromic_even_center. - - replace (2^pred (Nat.double 2)) with (4*2). - replace (length (hd ++ a)) with (4 * length (hd' ++ a')). - rewrite Nat.mul_mod_distr_l. rewrite Nat.mul_eq_0. right. - - rewrite <- Nat.div_exact. rewrite <- Nat.div2_div. - rewrite <- Nat.add_0_r. - replace 0 with (Nat.b2n (odd (length (hd' ++ a')))) at 2. - rewrite <- Nat.div2_odd. reflexivity. rewrite <- Nat.negb_even. - rewrite H0. reflexivity. easy. easy. easy. - rewrite app_length. rewrite app_length. rewrite N. - rewrite Nat.mul_add_distr_l. rewrite K. - rewrite <- K. rewrite O. reflexivity. reflexivity. - - intros hd hd' K O a a' tl'. intros H I J W L M N. - rewrite Nat.double_S. - replace (pred (S (S (Nat.double (S (S m)))))) - with (S (S (pred (Nat.double (S (S m)))))). - rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. - rewrite Nat.mul_assoc. replace (2*2) with 4. - - rewrite Nat.mod_mul_r. - assert (length (hd ++ a) mod 4 = 0). - assert (length hd mod 4 = 0). rewrite O. rewrite Nat.mul_comm. - rewrite Nat.mod_mul. reflexivity. easy. - rewrite app_length. rewrite Nat.add_mod. - rewrite H0. rewrite W. reflexivity. easy. rewrite H0. - rewrite Nat.add_0_l. rewrite Nat.mul_eq_0. right. - - -Nat.mod_mul_r: - forall a b c : nat, - b <> 0 -> c <> 0 -> a mod (b * c) = a mod b + b * ((a / b) mod c) - - - - - rewrite Nat.mod_mul_r. - assert (length (hd ++ a) mod 4 = 0). - assert (length hd mod 4 = 0). rewrite O. rewrite Nat.mul_comm. - rewrite Nat.mod_mul. reflexivity. easy. - rewrite app_length. rewrite Nat.add_mod. - rewrite H0. rewrite W. reflexivity. easy. rewrite H0. - rewrite Nat.add_0_l. rewrite Nat.mul_eq_0. right. - - -Nat.mod_mul_r: - forall a b c : nat, - b <> 0 -> c <> 0 -> a mod (b * c) = a mod b + b * ((a / b) mod c) - -Theorem tm_step_palindromic_length_12_prefix : - forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a mod 4 = 0 <-> length hd mod 4 = 0. - - - - rewrite app_length. rewrite N. rewrite O. - rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l. - apply Nat.mul_eq_0. right. rewrite <- app_length. - apply IHm with (tl := tl'). - - - - - -Theorem tm_step_palindromic_length_12_prefix : - forall (n : nat) (hd a tl : list bool), - tm_step n = hd ++ a ++ (rev a) ++ tl - -> 6 < length a - -> length a mod 4 = 0 <-> length hd mod 4 = 0. - - - - - unfold hd' at 2. - - - - - induction m. - - assert (even (length (hd' ++ a')) = true). - assert (0 < length a'). rewrite J in N. - replace (2 ^ (Nat.double 2)) with (4*4) in N. - rewrite Nat.mul_cancel_l in N. rewrite <- N. - apply Nat.lt_0_succ. easy. reflexivity. generalize H0. - generalize H. apply tm_step_palindromic_even_center. - - replace (2^pred (Nat.double 2)) with (4*2). - replace (length (hd ++ a)) with (4 * length (hd' ++ a')). - rewrite Nat.mul_mod_distr_l. rewrite Nat.mul_eq_0. right. - - rewrite <- Nat.div_exact. rewrite <- Nat.div2_div. - rewrite <- Nat.add_0_r. - replace 0 with (Nat.b2n (odd (length (hd' ++ a')))) at 2. - rewrite <- Nat.div2_odd. reflexivity. rewrite <- Nat.negb_even. - rewrite H0. reflexivity. easy. easy. easy. - rewrite app_length. rewrite app_length. rewrite N. - rewrite Nat.mul_add_distr_l. rewrite K. - rewrite <- K. rewrite O. reflexivity. reflexivity. - - - - - - - +(* Lemma tm_step_proper_palindrome_center : forall (m n k : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl -> 6 < length a -> length a = 2^(Nat.double m) (* palindrome non propre *) -> skipn (length hd - length a) hd = rev (firstn (length a) tl). -Proof. - intros m n k hd a tl. intros H I J. - - assert (W: (length a) mod 4 = 0). rewrite J in I. - destruct m. inversion I. inversion H1. - destruct m. inversion I. inversion H1. - inversion H3. inversion H5. inversion H7. - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J. - rewrite Nat.mul_assoc in J. - replace (2*2) with 4 in J. rewrite J. - rewrite <- Nat.mul_mod_idemp_l. reflexivity. - easy. reflexivity. apply le_0_n. apply le_0_n. - - assert ( - hd = tm_morphism (tm_morphism (firstn (length hd / 4) - (tm_step (pred (pred n))))) - /\ a = tm_morphism (tm_morphism - (firstn (length a / 4) (skipn (length hd / 4) - (tm_step (pred (pred n)))))) - /\ tl = tm_morphism (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred n)))))). - generalize W. generalize I. generalize H. - apply tm_step_palindromic_even_morphism2. - destruct H0 as [K H0]. destruct H0 as [L M]. - - - - - - - - - - - - - - -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. - - - - - *) +*)