From afc01a49bf33445504ab9973327ce6962b0740a7 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 19 Jan 2023 22:20:25 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 4064baa..24a688f 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -402,6 +402,41 @@ Proof. generalize K. generalize N. apply tm_morphism_app3. symmetry in P. + assert (even (length (rev a)) = true). rewrite rev_length. assumption. + + assert (R: tl = tm_morphism (skipn (Nat.div2 (length (rev a))) + (skipn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n))))). + generalize H0. generalize P. apply tm_morphism_app3. + + rewrite M in H. rewrite O in H. rewrite R in H. + rewrite tm_morphism_rev in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. + rewrite <- tm_morphism_eq in H. + pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)). + pose (a' := firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n))). + pose (tl' := skipn (Nat.div2 (length (rev a))) + (skipn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)))). + fold hd' in H. fold a' in H. fold tl' in H. + + assert (length a' = 2^S (Nat.double m)). unfold a'. + rewrite firstn_length_le. rewrite I. rewrite Nat.double_S. + rewrite Nat.pow_succ_r. rewrite Nat.div2_double. reflexivity. + apply le_0_n. rewrite skipn_length. + rewrite Nat.mul_le_mono_pos_r with (p := 2). + rewrite Nat.mul_comm. rewrite <- Nat.add_0_r at 1. + replace 0 with (Nat.b2n (Nat.odd (length a))) at 2. + rewrite <- Nat.div2_odd. rewrite Nat.mul_sub_distr_r. + + + re + + + + + (* réduire par la réciproque du morphisme *)