diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 3b0f694..83b4b25 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1061,17 +1061,17 @@ 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' + tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl' /\ odd (length hd') = true /\ even (length a') = true - /\ length a' < length a - /\ 0 < length a'. + /\ length a' < length a. Proof. intros n hd a tl. intros H I J K. @@ -1166,11 +1166,8 @@ Proof. 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. + (skipn (Nat.div2 (length hd'')) (tm_step n))). + split. rewrite <- pred_Sn. rewrite M1 at 1. reflexivity. assert (Nat.div2 (length hd'') <= length (tm_step n)). rewrite Nat.mul_le_mono_pos_l with (p := 2). @@ -1218,8 +1215,6 @@ Proof. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. assumption. - split. - rewrite firstn_length. assert (min (Nat.div2 (length a'')) (length (skipn (Nat.div2 (length hd'')) (tm_step n))) @@ -1229,41 +1224,13 @@ Proof. apply Nat.lt_div2. assumption. generalize H3. generalize H2. apply Nat.le_lt_trans. - rewrite firstn_length_le. rewrite M3. - rewrite Nat.mul_lt_mono_pos_l with (p := 2). - rewrite Nat.mul_0_r. rewrite <- Nat.double_twice. - rewrite <- Nat.Even_double. assumption. - apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. - apply Nat.lt_0_2. - - 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. - + (* 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. + (skipn (Nat.div2 (length hd')) (tm_step n))). + split. rewrite <- pred_Sn. rewrite L1 at 1. reflexivity. assert (Nat.div2 (length hd') <= length (tm_step n)). rewrite Nat.mul_le_mono_pos_l with (p := 2). @@ -1302,8 +1269,6 @@ Proof. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. assumption. - split. - rewrite firstn_length. assert (min (Nat.div2 (length a')) (length (skipn (Nat.div2 (length hd')) (tm_step n))) @@ -1312,31 +1277,6 @@ Proof. assert (Nat.div2 (length a') < length a). rewrite L3. apply Nat.lt_div2. assumption. generalize H3. generalize H2. apply Nat.le_lt_trans. - - rewrite firstn_length_le. rewrite L3. - rewrite Nat.mul_lt_mono_pos_l with (p := 2). - rewrite Nat.mul_0_r. rewrite <- Nat.double_twice. - rewrite <- Nat.Even_double. assumption. - apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. - apply Nat.lt_0_2. - - 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. - (* 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. @@ -1434,9 +1374,6 @@ Qed. - - - (* Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl @@ -1444,11 +1381,10 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), -> odd (length hd) = true -> even (length a) = true -> exists (hd' a' tl' : list bool), - tm_step n = hd' ++ a' ++ a' ++ tl' + tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl' /\ odd (length hd') = true /\ even (length a') = true - /\ length a' < length a - /\ 0 < length a'. + /\ length a' < length a. *)