diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 09c16e0..440300f 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1650,3 +1650,54 @@ Proof. generalize H1. generalize H0. apply IHn. - assumption. Qed. + +(* +Theorem tm_step_repeating_patterns_no_square : + forall (n m : nat) (hd a b tl : list bool), + tm_step n = hd ++ a ++ b ++ tl -> length a = 2^m + -> (forall k, length hd = k * 2 ^ S m -> a <> b). +Proof. + intros n m hd a b tl. intros H I. + induction n. + - assert (m = 0). + destruct m. reflexivity. + assert (length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in H0 at 2. rewrite app_length in H0. rewrite Nat.add_comm in H0. + rewrite app_length in H0. rewrite <- Nat.add_assoc in H0. + rewrite I in H0. rewrite Nat.pow_succ_r in H0. symmetry in H0. + apply Nat.eq_add_1 in H0. destruct H0; destruct H0. + apply Nat.mul_eq_1 in H0. destruct H0. inversion H0. + apply Nat.mul_eq_0 in H0. destruct H0. inversion H0. + apply Nat.pow_nonzero in H0. contradiction H0. easy. apply le_0_n. + intro k. intro J. rewrite H0 in J. rewrite Nat.pow_1_r in J. + assert (k = 0). + assert (length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in H1 at 2. rewrite app_length in H1. rewrite J in H1. + symmetry in H1. apply Nat.eq_add_1 in H1. destruct H1; destruct H1. + apply Nat.mul_eq_1 in H1. destruct H1. inversion H3. + apply Nat.mul_eq_0 in H1. destruct H1. assumption. inversion H1. + rewrite H1 in J. rewrite Nat.mul_0_l in J. rewrite length_zero_iff_nil in J. + assert ({a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec. + destruct H2. rewrite <- e in H. + + assert (0 < length a). rewrite I. rewrite H0. apply Nat.lt_0_1. + + assert (hd <> nil). generalize H2. generalize H. + apply tm_step_square_prefix_not_nil. rewrite J in H3. + contradiction H3. reflexivity. assumption. + - + + Reformulation: +forall (n : nat) (hd a tl : list bool), +tm_step n = hd ++ a ++ a ++ tl + -> 0 < length a + -> (length hd) mod (length (a ++ a)) <> 0. + PB : manque l'idée d'une puissance de 2 ! + + + + +Theorem tm_step_square_prefix_not_nil : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil. + *) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 13204d9..35aceb7 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1819,6 +1819,80 @@ Proof. Qed. +Lemma tm_step_palindromic_power2_even : + 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 + <-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0. +Proof. + intros m n k hd a tl. intros H I J. + + 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. + + 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 (length (hd ++ a) mod 4 = 0). + assert (W' := W). + rewrite tm_step_palindromic_length_12_prefix + with (hd := hd) (n := n) (tl := tl) in W'. + rewrite app_length. rewrite Nat.add_mod. + rewrite W. rewrite W'. reflexivity. easy. assumption. assumption. + + split. + - intro P. + rewrite <- Nat.mul_cancel_l with (p := 4). + rewrite <- Nat.mul_mod_distr_l. + replace 4 with (2*2) at 3. rewrite <- Nat.mul_assoc. + rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r. + + replace (S (S (pred (Nat.double (pred (S (S m))))))) + with (pred (Nat.double (S (S m)))). + 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 <- pred_Sn. rewrite Nat.double_S. + rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity. + rewrite Nat.neq_0_lt_0. rewrite Nat.double_S. + apply Nat.lt_0_succ. apply le_0_n. apply le_0_n. + reflexivity. + + apply Nat.pow_nonzero. easy. easy. easy. + - intro P. + rewrite <- Nat.mul_cancel_l with (p := 4) in P. + rewrite <- Nat.mul_mod_distr_l in P. + replace 4 with (2*2) in P at 3. rewrite <- Nat.mul_assoc in P. + rewrite <- Nat.pow_succ_r in P. rewrite <- Nat.pow_succ_r in P. + + replace (S (S (pred (Nat.double (pred (S (S m))))))) + with (pred (Nat.double (S (S m)))) in P. + replace (4 * (length (hd ++ a) / 4)) + with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4) in P. + rewrite <- Nat.div_mod_eq in P. assumption. + rewrite H0. rewrite Nat.add_0_r. reflexivity. + + rewrite <- pred_Sn. rewrite Nat.double_S. + rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity. + rewrite Nat.neq_0_lt_0. rewrite Nat.double_S. + apply Nat.lt_0_succ. apply le_0_n. apply le_0_n. + reflexivity. + + apply Nat.pow_nonzero. easy. easy. easy. +Qed. + + + Lemma xxx : forall (m n k : nat) (hd a tl : list bool), @@ -1912,33 +1986,64 @@ Proof. 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'). -m, n, k : nat -hd, a, tl : list bool -hd' := firstn (length hd / 4) (tm_step n) : list bool -a' := firstn (length a / 4) (skipn (length hd / 4) (tm_step n)) : list bool -tl' := skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n) : list bool -H : tm_step n = hd' ++ a' ++ rev a' ++ tl' -I : 6 < length a -J : length a = 2 ^ Nat.double (S (S m)) -W : length a mod 4 = 0 -K : hd = tm_morphism (tm_morphism hd') -L : a = tm_morphism (tm_morphism a') -M : tl = - tm_morphism - (tm_morphism - (skipn (length hd / 4 + Nat.div2 (length a)) - (tm_step (pred (pred (S (S n))))))) -V : 3 < S (S n) -N : length a = 4 * length a' -O : length hd = 4 * length hd' +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. +