From 03eed617c7982d81c5c61552c788e0146ee7feab Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 15 Jan 2023 15:23:55 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 250 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 220 insertions(+), 30 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 772fb92..fff3127 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -629,6 +629,7 @@ Proof. 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 (L0 := L1). assert (M0 := M1). assert (N: 0 < n). generalize K. generalize I. generalize H. apply tm_step_not_nil_factor_even. @@ -690,42 +691,231 @@ Proof. 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. + (* now we easily discard the case where a'0 would be odd since we + can freely choose either L1 or M1 to find an even prefix *) + assert (Nat.Even (Nat.div2 (length a)) \/ Nat.Odd (Nat.div2 (length a))). + apply Nat.Even_or_Odd. destruct H0 as [Z | Z]. + - (* first case, a'0 is even and we are looking for an odd prefix *) + 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. + + (* case Nat.div2 (length hd'') has an odd length *) + exists (firstn (Nat.div2 (length hd'')) (tm_step n)). + exists (firstn (Nat.div2 (length a'')) + (skipn (Nat.div2 (length hd'')) (tm_step n))). + exists (skipn (Nat.div2 (length (a'' ++ a''))) + (skipn (Nat.div2 (length hd'')) (tm_step n)) + ++ map negb (tm_step n)). + split. rewrite tm_build. rewrite M1 at 1. + rewrite <- app_assoc. rewrite <- app_assoc. + rewrite <- app_assoc. reflexivity. + + assert (Nat.div2 (length hd'') <= length (tm_step n)). + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. + rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'. + rewrite <- tm_size_power2. rewrite M0. + rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. + apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + assumption. apply Nat.lt_0_2. + + split. + + rewrite firstn_length_le. + 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. + rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0. + apply Nat.Even_succ in H0. apply Nat.Odd_OddT in H0. + apply Nat.OddT_odd in H0. apply H0. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ. + assumption. + destruct (length hd). inversion J. apply Nat.lt_0_succ. + + assumption. + + split. rewrite firstn_length_le. + rewrite M3. apply Nat.EvenT_even. apply Nat.Even_EvenT. + assumption. rewrite skipn_length. + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + + rewrite firstn_length. + assert (min (Nat.div2 (length a'')) + (length (skipn (Nat.div2 (length hd'')) (tm_step n))) + <= (Nat.div2 (length a''))). + apply Nat.le_min_l. + assert (Nat.div2 (length a'') < length a). rewrite M3. + apply Nat.lt_div2. assumption. + generalize H3. generalize H2. apply Nat.le_lt_trans. + + (* case Nat.div2 (length hd') has an odd length *) + exists (firstn (Nat.div2 (length hd')) (tm_step n)). + exists (firstn (Nat.div2 (length a')) + (skipn (Nat.div2 (length hd')) (tm_step n))). + exists (skipn (Nat.div2 (length (a' ++ a'))) + (skipn (Nat.div2 (length hd')) (tm_step n)) + ++ map negb (tm_step n)). + split. rewrite tm_build. rewrite L1 at 1. + rewrite <- app_assoc. rewrite <- app_assoc. + rewrite <- app_assoc. reflexivity. + + assert (Nat.div2 (length hd') <= length (tm_step n)). + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. + rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'. + rewrite <- tm_size_power2. rewrite L0. + rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. + apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + assumption. apply Nat.lt_0_2. + + split. + + rewrite firstn_length_le. + apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption. + assumption. + + split. rewrite firstn_length_le. + rewrite L3. apply Nat.EvenT_even. apply Nat.Even_EvenT. + assumption. rewrite skipn_length. + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + + rewrite firstn_length. + assert (min (Nat.div2 (length a')) + (length (skipn (Nat.div2 (length hd')) (tm_step n))) + <= (Nat.div2 (length a'))). + apply Nat.le_min_l. + assert (Nat.div2 (length a') < length a). rewrite L3. + apply Nat.lt_div2. assumption. + generalize H3. generalize H2. apply Nat.le_lt_trans. + - (* second case, a'0 is odd and we are looking for an even prefix *) + assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))). + apply Nat.Even_or_Odd. destruct H0. + + assert (Nat.div2 (length hd') <= length (tm_step n)). + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. + rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'. + rewrite <- tm_size_power2. rewrite L0. + rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. + apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + assumption. apply Nat.lt_0_2. + + assert (even (length (firstn (Nat.div2 (length hd')) (tm_step n))) = false). + assert (odd (length (firstn (Nat.div2 (length a')) + (skipn (Nat.div2 (length hd')) (tm_step n)))) = true). + rewrite firstn_length_le. rewrite L3. + apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption. + rewrite skipn_length. + + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + generalize H2. generalize L1. apply tm_step_odd_prefix_square. + + rewrite firstn_length_le in H2. + apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0. + rewrite H0 in H2. inversion H2. assumption. + + assert (Nat.div2 (length hd'') <= length (tm_step n)). + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. + rewrite tm_size_power2. rewrite <- Nat.pow_succ_r'. + rewrite <- tm_size_power2. rewrite M0. + rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. apply Nat.eq_le_incl. reflexivity. + apply le_0_n. apply Nat.EvenT_Even. apply Nat.even_EvenT. + assumption. apply Nat.lt_0_2. + + assert (even (length (firstn (Nat.div2 (length hd'')) (tm_step n))) = false). + assert (odd (length (firstn (Nat.div2 (length a'')) + (skipn (Nat.div2 (length hd'')) (tm_step n)))) = true). + rewrite firstn_length_le. rewrite M3. + apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption. + rewrite skipn_length. + + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + generalize H2. generalize M1. apply tm_step_odd_prefix_square. + + rewrite firstn_length_le in H2. - - (* - 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). + 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. + rewrite <- Nat.Odd_div2 in H0. rewrite <- Nat.Even_div2 in H0. + apply Nat.Even_succ in H0. rewrite Nat.Even_succ_succ in H0. + apply Nat.Even_EvenT in H0. apply Nat.EvenT_even in H0. + rewrite H0 in H2. inversion H2. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.OddT_Odd. apply Nat.odd_OddT. rewrite Nat.odd_succ. + assumption. + destruct (length hd). inversion J. apply Nat.lt_0_succ. + assumption. +Qed.