Update
This commit is contained in:
Thomas Baruchel
parent
76efd13e3e
commit
bf2e7e5575
|
|
@ -8,6 +8,12 @@ Require Import Bool.
|
|||
Import ListNotations.
|
||||
|
||||
|
||||
(**
|
||||
The following lemma, while not of truly general use, is
|
||||
used in several proofs and has therefore its own dedicated
|
||||
section here.
|
||||
*)
|
||||
|
||||
Lemma tm_step_consecutive_identical :
|
||||
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
|
||||
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
|
||||
|
|
@ -79,6 +85,11 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
(**
|
||||
The following lemmas and theorems are all related to
|
||||
squares of odd length in the Thue-Morse sequence.
|
||||
*)
|
||||
|
||||
Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ tl -> length a = 5
|
||||
-> a <> [ true; false; true; false; true].
|
||||
|
|
@ -282,7 +293,7 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
Lemma tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
|
||||
Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
|
@ -316,144 +327,9 @@ Qed.
|
|||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
|
||||
tm_step n = hd ++ pat ++ tl
|
||||
-> length pat <= 2^k
|
||||
-> exists (hd2 tl2 : list bool), tm_step (S (S k)) = hd2 ++ pat ++ tl2.
|
||||
Proof.
|
||||
intros n k hd pat tl. intros H I.
|
||||
assert (exists (m : nat),
|
||||
(m * 2^(S (S (S k))) <= length hd /\ length (hd++pat) < (S m) * 2^(S (S (S k))))).
|
||||
induction n.
|
||||
- simpl in H. exists 0. rewrite Nat.mul_0_l. rewrite Nat.mul_1_l.
|
||||
split. apply Nat.le_0_l.
|
||||
assert (J: length [false] = length (hd ++ pat ++ tl)).
|
||||
rewrite H. reflexivity. simpl in J. rewrite app_assoc in J.
|
||||
rewrite app_length in J.
|
||||
assert (K: length (hd++pat) <= 1). destruct tl. simpl in J.
|
||||
rewrite Nat.add_0_r in J. rewrite <- J. apply Nat.le_refl.
|
||||
simpl in J. rewrite <- Nat.add_comm in J. symmetry in J.
|
||||
rewrite <- Nat.add_1_l in J. rewrite <- Nat.add_0_r in J.
|
||||
rewrite <- Nat.add_assoc in J. rewrite Nat.add_cancel_l in J.
|
||||
apply Nat.eq_add_0 in J. destruct J. rewrite H1. apply Nat.le_0_1.
|
||||
assert (L: 1 < 2^(S (S (S k)))).
|
||||
rewrite <- Nat.le_succ_l. rewrite Nat.pow_succ_r'.
|
||||
rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l.
|
||||
rewrite Nat.le_succ_l.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
generalize L. generalize K. apply Nat.le_lt_trans.
|
||||
-
|
||||
|
||||
|
||||
ABCDABCDABCD
|
||||
-> prouver ensuite length (hd3 ++ pat) < 5 * 2^k
|
||||
ou length (hd3) < 4 * 2^k
|
||||
|
||||
|
||||
soit le motif se trouve dans un bloc de 2 répété depuis l'origine,
|
||||
soit il se trouve dans un bloc de 4 répété depuis l'origine
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma tm_step_repeating_patterns :
|
||||
forall (n m i j : nat),
|
||||
i < 2^m -> j < 2^m
|
||||
-> forall k, k < 2^n -> nth_error (tm_step m) i
|
||||
= nth_error (tm_step m) j
|
||||
<-> nth_error (tm_step (m+n)) (k * 2^m + i)
|
||||
= nth_error (tm_step (m+n)) (k * 2^m + j).
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma xxx : forall (k : nat) (hd pat tl : list bool),
|
||||
tm_step (S (S k)) = hd ++ pat ++ tl
|
||||
-> length pat <= 2^k
|
||||
-> (exists (hd2 tl2 : list bool),
|
||||
map negb (tm_step (S (S k))) = hd2 ++ pat ++ tl2).
|
||||
Proof.
|
||||
intros k hd pat tl. intros H I.
|
||||
assert (length (hd++pat) <= 2^(S k)
|
||||
\/ (length (hd++pat) > 2^(S k) /\ length (hd++pat) <= 3 * 2^k)
|
||||
\/ length (hd++pat) > 3 * 2^k).
|
||||
assert (length (hd++pat) <= 2^(S k) \/ 2^(S k) < length (hd++pat)).
|
||||
apply Nat.le_gt_cases.
|
||||
assert (length (hd++pat) <= 3*2^k \/ 3*2^k < length (hd++pat)).
|
||||
apply Nat.le_gt_cases.
|
||||
assert (2^(S k) < length (hd++pat) <->
|
||||
((length (hd++pat) > 2^(S k) /\ length (hd++pat) <= 3 * 2^k)
|
||||
\/ 3 * 2^k < length (hd++pat))).
|
||||
split. intro J.
|
||||
destruct H1.
|
||||
left. split. apply J. assumption.
|
||||
right. assumption.
|
||||
intro J. destruct J. destruct H2. apply H2.
|
||||
assert (2^(S k) < 3 * 2^k). simpl. rewrite Nat.add_0_r.
|
||||
rewrite <- Nat.add_lt_mono_l. rewrite <- Nat.add_0_r at 1.
|
||||
rewrite <- Nat.add_lt_mono_l.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
generalize H2. generalize H3. apply Nat.lt_trans.
|
||||
rewrite H2 in H0. apply H0.
|
||||
destruct H0.
|
||||
- assert (J: exists (tl3 : list bool), tm_step (S k) = hd ++ pat ++ tl3).
|
||||
exists (firstn (2^(S k) - (length (hd++pat))) tl).
|
||||
rewrite tm_build in H. rewrite <- firstn_app_2. rewrite <- firstn_app_2.
|
||||
rewrite app_length. rewrite Nat.add_assoc.
|
||||
rewrite Nat.add_comm. rewrite Nat.sub_add.
|
||||
assert (firstn (2^(S k)) (hd++pat++tl) = firstn (2^(S k)) (hd++pat++tl)).
|
||||
reflexivity. rewrite <- H in H1 at 1.
|
||||
rewrite firstn_app in H1. rewrite tm_size_power2 in H1.
|
||||
rewrite Nat.sub_diag in H1. rewrite firstn_O in H1.
|
||||
rewrite app_nil_r in H1. rewrite <- tm_size_power2 in H1 at 1.
|
||||
rewrite firstn_all in H1. assumption.
|
||||
rewrite <- app_length. assumption.
|
||||
rewrite tm_build. rewrite map_app.
|
||||
rewrite map_map.
|
||||
assert (forall l, map (fun x : bool => negb (negb x)) l = l).
|
||||
intro. induction l. reflexivity.
|
||||
simpl. rewrite IHl. rewrite negb_involutive. reflexivity.
|
||||
rewrite H1. destruct J. rewrite H2.
|
||||
exists (map negb (hd ++ pat ++ x) ++ hd). exists (x).
|
||||
rewrite app_assoc. reflexivity.
|
||||
- destruct H0. destruct H0.
|
||||
|
||||
|
||||
left. assumption.
|
||||
- destruct H0.
|
||||
+ destruct H0. right.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
replace (tl)
|
||||
with ((firstn (2^(S k) - (length (hd++pat))) tl)
|
||||
++ (skipn (2^(S k) - (length (hd++pat))) tl)) in H.
|
||||
|
||||
replace (tm_step (S k))
|
||||
with (hd ++ pat ++ (firstn (2^(S k) - (length (hd++pat))) tl)) in H.
|
||||
rewrite <- app_assoc in H. apply app_inv_head_iff in H.
|
||||
rewrite <- app_assoc in H. apply app_inv_head_iff in H.
|
||||
apply app_inv_head_iff in H.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
rewrite tm_build. rewrite map_app. rewrite map_map.
|
||||
|
||||
|
||||
|
||||
|
||||
right.
|
||||
replace (length (tl ++ pat) > 2^(S k)) with (True).
|
||||
apply Nat.le_gt_cases.
|
||||
(**
|
||||
New section
|
||||
*)
|
||||
|
||||
|
||||
|
||||
|
|
@ -461,19 +337,7 @@ Proof.
|
|||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
|
||||
tm_step n = hd ++ pat ++ tl
|
||||
-> length pat <= 2^k
|
||||
-> exists (hd2 tl2 : list bool),
|
||||
tm_step (S (S k)) = hd2 ++ pat ++ tl2 /\ length (hd2 ++ pat) < 3 * (2^k).
|
||||
Proof.
|
||||
intros n k hd pat tl. intros H I.
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
L'inégalité finale doit être stricte, car si le motif fait exactement 2^k
|
||||
et se situe à la fin des 3 * (2^k) termes, il est aussi au début !
|
||||
|
||||
|
|
@ -493,3 +357,4 @@ T[8:24] : carré (répété) de taille 8 (mais aussi T[40:56])
|
|||
Termes de 11 à 17 (exclus) : carré (répété) de taille 3
|
||||
Termes de 22 à 34 (exclus) : carré (répété) de taille 6
|
||||
Termes de 44 à 68 (exclus) : carré (répété) de taille 12
|
||||
*)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user