From acdc1a613c790a70e4a4fc814022d1a4a93558ce Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 23 Jan 2023 21:56:54 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 8644b04..75a0b03 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1153,6 +1153,28 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity. rewrite Y''. apply Nat.le_succ_diag_r. reflexivity. + (* destructuring n *) + destruct n. inversion H0. rewrite <- tm_step_lemma in H. + + (* inverting tm_morphism in tm_step n *) + assert (hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))). + generalize H11. generalize H. apply tm_morphism_app2. + + assert (s ++ tl = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))). + generalize H11. generalize H. apply tm_morphism_app3. symmetry in H13. + + assert (even (length s) = true). unfold s. reflexivity. + assert (s = tm_morphism (firstn (Nat.div2 (length s)) + (skipn (Nat.div2 (length hd'')) (tm_step n)))). + generalize H14. generalize H13. apply tm_morphism_app2. + + assert (tl = tm_morphism (skipn (Nat.div2 (length s)) + (skipn (Nat.div2 (length hd'')) (tm_step n)))). + generalize H14. generalize H13. apply tm_morphism_app3. + + rewrite H12 in H. rewrite H15 in H. rewrite H16 in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_eq in H.