diff --git a/src/thue_morse3.v b/src/thue_morse3.v index a75ed4a..2a050ef 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1479,65 +1479,133 @@ Qed. +Lemma tm_step_palindromic_even_morphism2 : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> length a > 6 + -> (length a) mod 4 = 0 + -> 11 = 42. +Proof. + intros n hd a tl. intros H W J0. + assert (Z: 0 < length a). + apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. + apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. + assumption. + (* proof that n <> 0 *) + destruct n. assert (length (tm_step 0) <= length (tm_step 0)). + apply Nat.le_refl. + rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0. + rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0. simpl in H0. + apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0. + rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0. + assert (K: 1 <= length a + (length tl + length hd)). + rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption. + rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0. + rewrite H0 in Z. inversion Z. + assert (J1: length hd mod 4 = 0). generalize J0. generalize W. + generalize H. apply tm_step_palindromic_length_12_prefix. + assert (EVEN: forall m, m mod 4 = 0 -> even m = true). + intro m. intro U. rewrite <- Nat.div_exact in U. + rewrite U. rewrite Nat.even_mul. reflexivity. easy. - assert (tm_step (S n) = tm_morphism - (firstn (Nat.div2 (length hd)) (tm_step n) ++ - firstn (Nat.div2 (length a)) - (skipn (Nat.div2 (length hd)) (tm_step n)) ++ - firstn (Nat.div2 (length (rev a))) - (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ - skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) (tm_step n))). - assert (K : even (length (rev a)) = true). - rewrite rev_length. assumption. - generalize K. generalize J. generalize H1. generalize H. - apply tm_step_morphism4. rewrite rev_length in H2. + assert (J: even (length a) = true). + apply EVEN in J0. assumption. - rewrite <- pred_Sn. - - - - - - - - assert (even (length (hd ++ a)) = true). generalize I. generalize H. + assert (even (length (hd ++ a)) = true). generalize Z. generalize H. apply tm_step_palindromic_even_center. - assert (even (length hd) = true). rewrite app_length in H0. + assert (I: even (length hd) = true). rewrite app_length in H0. rewrite Nat.even_add in H0. rewrite J in H0. destruct (even (length hd)). reflexivity. inversion H0. - rewrite <- tm_step_lemma in H. + assert (K: even (length (rev a)) = true). rewrite rev_length. assumption. + + rewrite app_assoc in H. rewrite <- tm_step_lemma in H. + + assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a))) + (tm_step n))). + generalize H0. generalize H. apply tm_morphism_app2. + + rewrite <- app_assoc in H. symmetry in H1. + assert (even (length (hd ++ a ++ (rev a))) = true). + rewrite app_length. rewrite Nat.even_add. rewrite I. + rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K. + reflexivity. + + assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a)))) + (tm_step n))). + replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H. + generalize H2. generalize H. apply tm_morphism_app3. + rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). - generalize H1. generalize H. apply tm_morphism_app2. + generalize I. generalize H. apply tm_morphism_app2. - assert (a ++ (rev a) ++ tl - = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))). - generalize H1. generalize H. apply tm_morphism_app3. symmetry in H3. + assert (a = tm_morphism (skipn (Nat.div2 (length hd)) + (firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))). + generalize I. generalize H1. apply tm_morphism_app3. - assert (a = tm_morphism (firstn (Nat.div2 (length a)) - (skipn (Nat.div2 (length hd)) (tm_step n)))). - generalize J. generalize H3. apply tm_morphism_app2. + rewrite skipn_firstn_comm in H5. rewrite app_length in H5. - assert (tl = tm_morphism (skipn (Nat.div2 (length (a ++ (rev a)))) - (skipn (Nat.div2 (length hd)) (tm_step n)))). - assert (even (length (a ++ (rev a))) = true). rewrite app_length. - rewrite rev_length. rewrite Nat.even_add. rewrite J. reflexivity. - generalize H5. rewrite app_assoc in H3. generalize H3. - apply tm_morphism_app3. + replace (Nat.div2 (length hd + length a)) + with ((length hd) / 2 + Nat.div2 (length a)) in H5. + rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5. + rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5. - rewrite H2 in H. rewrite H4 in H. rewrite tm_morphism_rev in H. - rewrite H5 in H. rewrite <- tm_morphism_app in H. + rewrite H4 in H. rewrite H5 in H. rewrite H3 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. + + rewrite app_length in H. rewrite app_length in H. rewrite rev_length in H. + replace (length a + length a) with ((length a)*2) in H. + replace (Nat.div2 (length hd + length a * 2)) + with ((length hd + length a * 2) / 2) in H. + rewrite Nat.div_add in H. rewrite <- Nat.div2_div 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 hd) + length a) (tm_step n)). + fold hd' in H. fold a' in H. fold tl' in H. + + assert (EVEN2: forall m, m mod 4 = 0 -> even (Nat.div2 m) = true). + intro m. intro U. rewrite <- Nat.div_exact in U. + rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc. + rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy. + + assert (I': even (length hd') = true). + unfold hd'. rewrite firstn_length_le. apply EVEN2. assumption. + + + + + + + assumption. easy. + rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl. + rewrite Nat.add_0_r. reflexivity. + + apply Nat.le_refl. + rewrite <- Nat.div_add. rewrite <- Nat.div2_div. + rewrite Nat.mul_comm. + + rewrite Nat.div2_odd with (a := length a) at 2. + rewrite <- Nat.negb_even. rewrite J. simpl. + rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy. +Qed. + + + + + + + - rewrite app_length in H. rewrite rev_length in H. - replace (Nat.div2 (length a + length a)) with (length a) in H. - rewrite <- pred_Sn.