Update

src/thue_morse2.v

@@ -79,6 +79,177 @@ Proof.
 Qed.
 
 
+Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl -> length a = 5
+  -> a <> [ true; false; true; false; true].
+Proof.
+  intros n hd a tl. intros H I.
+
+  destruct n.
+  assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
+  rewrite H in H0 at 2. simpl in H0.
+  rewrite app_length in H0. rewrite app_length in H0.
+  rewrite I in H0. rewrite Nat.add_shuffle3 in H0.
+  apply Nat.succ_inj in H0. inversion H0.
+
+  assert (even (length (tm_step (S n))) = true).
+  rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul.
+  apply Nat.le_0_l.
+
+  assert (J: even (length hd) = negb (even (length tl))).
+  rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
+  rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0.
+  destruct (even (length hd)); destruct (even (length tl)).
+  inversion H0. reflexivity. reflexivity. inversion H0.
+
+  assert (K: {a=[true; false; true; false; true]}
+           + {~ a=[ true; false; true; false; true]}).
+  apply list_eq_dec. apply bool_dec. destruct K.
+
+  assert ({even (length hd) = true} + {even (length hd) <> true}).
+  apply bool_dec. destruct H1.
+
+  (* case length hd is even *)
+  rewrite e0 in J. rewrite Nat.negb_even in J.
+  destruct tl. inversion J.
+  destruct b.
+
+  assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
+  generalize e0. generalize H. apply tm_step_count_occ.
+
+  assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true
+        = count_occ Bool.bool_dec (hd ++ a ++ [true]) false).
+  assert (even (length (hd ++ a ++ [true])) = true).
+  rewrite app_length. rewrite app_length.
+  rewrite Nat.even_add. rewrite Nat.even_add.
+  rewrite e0. rewrite e. reflexivity.
+  replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H.
+  generalize H2. generalize H. apply tm_step_count_occ.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+
+  rewrite count_occ_app in H2. rewrite H1 in H2.
+  symmetry in H2.
+  rewrite count_occ_app in H2. rewrite Nat.add_cancel_l in H2.
+
+  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
+  rewrite e in H2. simpl in H2. inversion H2.
+
+  replace (hd ++ a ++ false::tl)
+    with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  simpl. apply Nat.lt_0_2.
+
+  rewrite e. reflexivity.
+
+  (* case length hd is odd *)
+  apply not_true_is_false in n0.
+  rewrite app_removelast_last with (l := hd) (d := true) in H.
+  rewrite app_removelast_last with (l := hd) (d := true) in n0.
+  rewrite app_length in n0. simpl in n0.
+  rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0.
+  rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0.
+
+  destruct (last hd true).
+  rewrite <- app_assoc in H.
+  assert (count_occ Bool.bool_dec (removelast hd) true
+        = count_occ Bool.bool_dec (removelast hd) false).
+  generalize n0. generalize H. apply tm_step_count_occ.
+  replace (removelast hd ++ [true] ++ a ++ tl)
+    with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H.
+  assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true
+        = count_occ Bool.bool_dec (removelast hd ++ [true;true]) false).
+  assert (even (length (removelast hd ++ [true;true])) = true).
+  rewrite app_length. rewrite Nat.even_add_even. assumption.
+  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
+  generalize H2. generalize H. apply tm_step_count_occ.
+
+  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
+  rewrite H1 in H2. rewrite Nat.add_cancel_l in H2.
+  simpl in H2. inversion H2.
+
+  rewrite e. rewrite app_assoc_reverse. reflexivity.
+
+  replace ((removelast hd ++ [false]) ++ a ++ tl)
+    with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  simpl. apply Nat.lt_0_2.
+
+  rewrite e. rewrite app_assoc_reverse. reflexivity.
+
+  assert (length hd <> 0). destruct hd. inversion n0.
+  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
+  assert (length hd <> 0). destruct hd. inversion n0.
+  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
+
+  assumption.
+Qed.
+
+Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl -> length a = 5
+  -> a <> [ false; true; false; true; false].
+Proof.
+
+
+
+
+
+
+
+
+  assert ({last (b :: hd) true = true} + {last (b :: hd) true <> true}).
+  apply bool_dec.
+  assert (last (b::hd) true = true). destruct H1. assumption.
+  apply not_true_is_false in n0.
+
+  replace ((removelast (b :: hd) ++ [last (b :: hd) true]) ++ a ++ tl)
+    with ((removelast (b :: hd)) ++ [false;true] ++ [false;true]
+                                 ++ [false;true] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  simpl. apply Nat.lt_0_2.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite n0. rewrite e. reflexivity.
+  rewrite H1 in H.
+
+
+
+
+Lemma two_step_consecutive_identical_length :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl -> length a = 5
+  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
+Proof.
+  intros n hd a tl. intros H I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I.
+
+  assert (a = nil). simpl in I.
+  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
+  apply Nat.succ_inj in I.
+  apply length_zero_iff_nil in I. assumption.
+  rewrite H0. rewrite H0 in H. rewrite H0 in I.
+
+  destruct b; destruct b0; destruct b1; destruct b2; destruct b3.
+
+  exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity.
+  exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity.
+  exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity.
+  exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity.
+  exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity.
+  exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity.
+  exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity.
+  exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity.
+
+  exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
+  exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
+
+
+
+
+
+
 Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl -> length a = 3
   -> a = true::false::true::nil \/ a = false::true::false::nil.