Update
This commit is contained in:
Thomas Baruchel
parent
4fcaba8c73
commit
36b7d26757
|
|
@ -10,9 +10,11 @@
|
|||
But some powerful theorems are provided here:
|
||||
|
||||
- tm_step_cubefree (there is no cube in the sequence)
|
||||
- tm_step_square_size (about length of squared factrs)
|
||||
- tm_step_square_size (about length of squared factors)
|
||||
- tm_step_square_pos (length of the prefix has the same
|
||||
parity than the length of the factor being squared)
|
||||
- tm_step_square_prefix_not_nil (no square at the beginning
|
||||
of the sequence)
|
||||
*)
|
||||
|
||||
Require Import thue_morse.
|
||||
|
|
@ -1622,82 +1624,3 @@ Proof.
|
|||
simpl. rewrite Nat.add_0_r. reflexivity.
|
||||
left. assumption.
|
||||
Qed.
|
||||
|
||||
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.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
||||
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
||||
destruct W. rewrite e in H. rewrite app_nil_l in H.
|
||||
generalize dependent a.
|
||||
generalize dependent tl.
|
||||
induction n.
|
||||
- intros tl a. intros H I.
|
||||
destruct a. inversion I. inversion H.
|
||||
assert (length (nil : list bool) = length (nil : list bool)).
|
||||
reflexivity. rewrite H2 in H0 at 2. rewrite app_length in H0.
|
||||
rewrite Nat.add_comm in H0. inversion H0.
|
||||
- intros tl a. intros H I.
|
||||
assert (hd <> nil
|
||||
\/ exists a' tl', tm_step (pred (S n)) = a' ++ a' ++ tl' /\ 0 < length a').
|
||||
generalize I. generalize H. replace (a++a++tl) with (hd ++ a ++ a ++ tl).
|
||||
apply tm_step_square_prefix_not_nil0. rewrite e. reflexivity.
|
||||
destruct H0. assumption. destruct H0. destruct H0.
|
||||
rewrite <- pred_Sn in H0.
|
||||
destruct H0.
|
||||
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.
|
||||
*)
|
||||
|
|
|
|||
|
|
@ -1820,14 +1820,14 @@ Qed.
|
|||
|
||||
|
||||
Lemma tm_step_palindromic_power2_even :
|
||||
forall (m n k : nat) (hd a tl : list bool),
|
||||
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 k hd a tl. intros H I J.
|
||||
intros m n 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.
|
||||
|
|
@ -1902,11 +1902,15 @@ Lemma xxx :
|
|||
-> 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.
|
||||
|
|
@ -1946,6 +1950,15 @@ Proof.
|
|||
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.
|
||||
|
|
@ -1956,6 +1969,271 @@ Proof.
|
|||
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.
|
||||
|
||||
|
||||
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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue