From de483aef11ca9b8d6491da101ee45f0c5916ee1a Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 15 Jan 2023 11:39:53 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 142 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 132 insertions(+), 10 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 96901a8..772fb92 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -392,14 +392,7 @@ Proof. Qed. - - - - - - - -Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool), +Lemma tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> odd (length hd) = true @@ -495,8 +488,7 @@ Proof. Qed. - -Theorem tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool), +Lemma tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> odd (length hd) = true @@ -608,6 +600,136 @@ Proof. Qed. +Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl + -> 0 < length a + -> odd (length hd) = true + -> even (length a) = true + -> exists (hd' a' tl' : list bool), + tm_step n = hd' ++ a' ++ a' ++ tl' + /\ odd (length hd') = true + /\ even (length a') = true + /\ length a' < length a. +Proof. + intros n hd a tl. intros H I J K. + + assert (L: exists (hd' a' tl' : list bool), + tm_step n = hd' ++ a' ++ a' ++ tl' + /\ length hd' = S (length hd) /\ length a' = length a). + generalize K. generalize J. generalize I. generalize H. + apply tm_step_square_pos_even. + + assert (M: exists (hd' a' tl' : list bool), + tm_step n = hd' ++ a' ++ a' ++ tl' + /\ length hd' = Nat.pred (length hd) /\ length a' = length a). + generalize K. generalize J. generalize I. generalize H. + apply tm_step_square_pos_even'. + + destruct L as [hd' L2]. destruct L2 as [a' L3]. destruct L3 as [tl' L]. + destruct M as [hd'' M2]. destruct M2 as [a'' M3]. destruct M3 as [tl'' M]. + destruct L as [L1 L2]. destruct L2 as [L2 L3]. + destruct M as [M1 M2]. destruct M2 as [M2 M3]. + + assert (N: 0 < n). + generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even. + destruct n. inversion N. + + assert (L4: even (length hd') = true). rewrite L2. rewrite Nat.even_succ. + assumption. + assert (M4: even (length hd'') = true). rewrite M2. rewrite Nat.even_pred. + assumption. destruct hd. inversion J. easy. + + rewrite <- tm_step_lemma in L1. + assert (L5: hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))). + generalize L4. generalize L1. apply tm_morphism_app2. + + rewrite <- tm_step_lemma in M1. + assert (M5: hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))). + generalize M4. generalize M1. apply tm_morphism_app2. + + assert (L6: a' ++ a' ++ tl' + = tm_morphism (skipn (Nat.div2 (length hd')) (tm_step n))). + generalize L4. generalize L1. apply tm_morphism_app3. + + assert (M6: a'' ++ a'' ++ tl'' + = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))). + generalize M4. generalize M1. apply tm_morphism_app3. + + assert (L7: even (length a') = true). rewrite L3. assumption. + assert (L8: a' = tm_morphism (firstn (Nat.div2 (length a')) + (skipn (Nat.div2 (length hd')) (tm_step n)))). + generalize L7. symmetry in L6. generalize L6. apply tm_morphism_app2. + + assert (M7: even (length a'') = true). rewrite M3. assumption. + assert (M8: a'' = tm_morphism (firstn (Nat.div2 (length a'')) + (skipn (Nat.div2 (length hd'')) (tm_step n)))). + generalize M7. symmetry in M6. generalize M6. apply tm_morphism_app2. + + rewrite app_assoc in L6. symmetry in L6. + rewrite app_assoc in M6. symmetry in M6. + + assert (L9: even (length (a' ++ a')) = true). rewrite app_length. + rewrite Nat.even_add. rewrite L7. reflexivity. + + assert (M9: even (length (a'' ++ a'')) = true). rewrite app_length. + rewrite Nat.even_add. rewrite M7. reflexivity. + + assert (L10: tl' = tm_morphism (skipn (Nat.div2 (length (a' ++ a'))) + (skipn (Nat.div2 (length hd')) (tm_step n)))). + generalize L9. generalize L6. apply tm_morphism_app3. + + assert (M10: tl'' = tm_morphism (skipn (Nat.div2 (length (a'' ++ a''))) + (skipn (Nat.div2 (length hd'')) (tm_step n)))). + generalize M9. generalize M6. apply tm_morphism_app3. + + rewrite L5 in L1. rewrite L8 in L1. rewrite L10 in L1. + rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_app in L1. + rewrite <- tm_morphism_app in L1. rewrite <- tm_morphism_eq in L1. + + rewrite M5 in M1. rewrite M8 in M1. rewrite M10 in M1. + rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_app in M1. + rewrite <- tm_morphism_app in M1. rewrite <- tm_morphism_eq in M1. + + assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))). + apply Nat.Even_or_Odd. destruct H0. + + (* case Nat.div2 (length hd'') has an odd length *) + - assert( odd (Nat.div2 (length hd'')) = true). + apply eq_S in M2. rewrite Nat.succ_pred_pos in M2. + apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0. + + + + (* + assert (L9: a' ++ a' = a' ++ a'). reflexivity. + rewrite L8 in L9 at 4. rewrite L8 in L9 at 3. + rewrite <- tm_morphism_app in L9. + + assert (M9: a'' ++ a'' = a'' ++ a''). reflexivity. + rewrite M8 in M9 at 4. rewrite M8 in M9 at 3. + rewrite <- tm_morphism_app in M9. + *) + + + + + +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). + + + + + + + (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *) (* TODO: la taille du facteur divise la taille du préfixe ? *) (* TODO : le cas de la taille 2 est un cas pair facile