diff --git a/src/thue_morse2.v b/src/thue_morse2.v index bca9501..09c16e0 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1535,18 +1535,6 @@ Proof. assert (K: even (length a') = true). rewrite <- Nat.negb_odd. rewrite n0. reflexivity. - (* - assert (L: even (length (hd ++ a')) = true). - rewrite Nat.le_succ_l in J. apply Nat.lt_succ_l in J. - apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J. - generalize J. generalize H. apply tm_step_square_pos. - - assert (M: even (length hd) = true). - rewrite app_length in L. rewrite Nat.even_add_even in L. - assumption. - apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. - *) - assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec. destruct W. rewrite e in H. right. destruct n. inversion H. rewrite app_nil_l in H. @@ -1634,3 +1622,31 @@ Proof. simpl. rewrite Nat.add_0_r. reflexivity. left. assumption. Qed. + +Theorem tm_step_square_prefix_not_nil : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil. +Proof. + intros n hd a tl. intros H I. + + assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec. + destruct W. rewrite e in H. rewrite app_nil_l in H. + generalize dependent a. + generalize dependent tl. + induction n. + - intros tl a. intros H I. + destruct a. inversion I. inversion H. + assert (length (nil : list bool) = length (nil : list bool)). + reflexivity. rewrite H2 in H0 at 2. rewrite app_length in H0. + rewrite Nat.add_comm in H0. inversion H0. + - intros tl a. intros H I. + assert (hd <> nil + \/ exists a' tl', tm_step (pred (S n)) = a' ++ a' ++ tl' /\ 0 < length a'). + generalize I. generalize H. replace (a++a++tl) with (hd ++ a ++ a ++ tl). + apply tm_step_square_prefix_not_nil0. rewrite e. reflexivity. + destruct H0. assumption. destruct H0. destruct H0. + rewrite <- pred_Sn in H0. + destruct H0. + generalize H1. generalize H0. apply IHn. + - assumption. +Qed.