baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-11 13:54:07 +01:00
parent 965a3dfb29
commit 47686ee05f
1 changed files with 98 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

110
src/thue_morse2.v
View File

@ -457,25 +457,111 @@ Proof.
assumption. assumption. assumption. assumption.
Qed.
Lemma tm_step_normalize_prefix_even_squares :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> even (length a) = true
-> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
/\ even (length hd') = true /\ length a = length b.
Proof.
intros n hd a tl. intros H I.
assert (odd (length hd) = true \/ odd (length hd) = false).
destruct (odd (length hd)). left. reflexivity. right. reflexivity.
destruct H0.
generalize H0. generalize I. generalize H.
apply tm_step_shift_odd_prefix_even_squares.
exists hd. exists a. exists tl.
split. assumption. split. rewrite <- Nat.negb_odd. rewrite H0.
reflexivity. reflexivity.
Qed.
Lemma tm_step_square_half : forall (n : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ a ++ tl
-> even (length a) = true
-> exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length a = Nat.double (length a').
Proof.
intros n hd a tl. intros H I.
assert (
exists (hd' b tl': list bool), tm_step (S n) = hd' ++ b ++ b ++ tl'
/\ even (length hd') = true /\ length a = length b).
generalize I. generalize H. apply tm_step_normalize_prefix_even_squares.
destruct H0. destruct H0. destruct H0.
destruct H0. destruct H1. rewrite H2 in I.
rewrite <- tm_step_lemma in H0.
assert (x = tm_morphism (firstn (Nat.div2 (length x)) (tm_step n))).
apply tm_morphism_app2 with (tl := x0 ++ x0 ++ x1). apply H0.
assumption.
assert (x0 ++ x0 ++ x1 = tm_morphism (skipn (Nat.div2 (length x)) (tm_step n))).
apply tm_morphism_app3. apply H0. assumption.
assert (Z := H0).
assert (H7: length (tm_morphism (tm_step n)) = length (tm_morphism (tm_step n))).
reflexivity. rewrite Z in H7 at 2. rewrite tm_morphism_length in H7.
rewrite app_length in H7.
rewrite app_length in H7.
rewrite Nat.Even_double with (n := length x) in H7.
rewrite Nat.Even_double with (n := length x0) in H7.
rewrite Nat.Even_double with (n := length (x0 ++ x1)) in H7.
rewrite Nat.double_twice in H7.
rewrite Nat.double_twice in H7.
rewrite Nat.double_twice in H7.
rewrite <- Nat.mul_add_distr_l in H7.
rewrite <- Nat.mul_add_distr_l in H7.
rewrite Nat.mul_cancel_l in H7.
assert (x0 = tm_morphism (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n)))).
apply tm_morphism_app2 with (tl := x0 ++ x1). symmetry. assumption.
assumption.
assert (x1 = tm_morphism (skipn (Nat.div2 (length (x0++x0)))
(skipn (Nat.div2 (length x)) (tm_step n)))).
apply tm_morphism_app3. symmetry. rewrite app_assoc_reverse. apply H4.
rewrite app_length. rewrite Nat.even_add_even. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite H3 in H0. rewrite H5 in H0. rewrite H6 in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_app in H0.
rewrite <- tm_morphism_eq in H0.
rewrite H0.
exists (firstn (Nat.div2 (length x)) (tm_step n)).
exists (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n))).
exists (skipn (Nat.div2 (length (x0 ++ x0))) (skipn (Nat.div2 (length x)) (tm_step n))).
split. reflexivity.
rewrite firstn_length_le. rewrite <- Nat.Even_double. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite skipn_length.
rewrite H7. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite Nat.add_0_l. rewrite <- Nat.add_0_r at 1.
rewrite <- Nat.add_le_mono_l.
apply le_0_n. apply le_n. easy.
rewrite <- Nat.Even_double in H7. rewrite <- Nat.Even_double in H7.
rewrite Nat.add_assoc in H7.
assert (Nat.even (2 * (length (tm_step n))) = true).
apply Nat.even_mul. rewrite H7 in H5.
rewrite Nat.even_add in H5.
rewrite Nat.even_add in H5.
rewrite I in H5. rewrite H1 in H5.
apply Nat.EvenT_Even. apply Nat.even_EvenT.
destruct (Nat.even (length (x0 ++ x1))). reflexivity.
inversion H5.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
Qed.
(*
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 !
Carré de taille 3 :
AABAAB (impossible)
ABBABB (impossible)
ABAABA (OK)
BABBAB
T[2:6] : carré (répété) de taille 2 (mais aussi T[10:14])
T[4:12] : carré (répété) de taille 4 (mais aussi T[20:28])
T[8:24] : carré (répété) de taille 8 (mais aussi T[40:56])