Update

thue-morse.v

@@ -872,37 +872,6 @@ Proof.
   apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
 Qed.
 
-Lemma tm_step_next_range2 :
-  forall (n : nat) (l1 l2 : list bool) (b : bool),
-  tm_step n = l1 ++ b :: l2
-    -> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b).
-Proof.
-  intros n l1 l2 b. intros H.
-  assert (nth_error (tm_step n) (length l1) = Some b).
-  generalize H. apply list_concat_to_pos.
-  rewrite tm_build.
-  assert (I: length l1 < 2^n).
-    rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
-  rewrite nth_error_app2. rewrite tm_size_power2.
-  rewrite Nat.add_sub. apply map_nth_error. apply H0.
-  rewrite tm_size_power2. apply Nat.le_add_l.
-Qed.
-
-Lemma tm_step_next_range2' :
-  forall (n k : nat) (b : bool),
-  nth_error (tm_step n) k = Some b
-    -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
-Proof.
-  intros n k b. intros H. assert (I := H).
-  apply nth_error_split in H. destruct H. destruct H. inversion H.
-  rewrite tm_build.
-  assert (J: k < 2^n).
-  rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt.
-  rewrite nth_error_app2. rewrite tm_size_power2.
-  rewrite Nat.add_sub. apply map_nth_error. apply I.
-  rewrite tm_size_power2. apply Nat.le_add_l.
-Qed.
-
 Lemma tm_add_range : forall (n m k : nat),
   k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
 Proof.
@@ -939,7 +908,78 @@ Proof.
     reflexivity.
 Qed.
 
+Lemma tm_step_next_range2 :
+  forall (n : nat) (l1 l2 : list bool) (b : bool),
+  tm_step n = l1 ++ b :: l2
+    -> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b).
+Proof.
+  intros n l1 l2 b. intros H.
+  assert (nth_error (tm_step n) (length l1) = Some b).
+  generalize H. apply list_concat_to_pos.
+  rewrite tm_build.
+  assert (I: length l1 < 2^n).
+    rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
+  rewrite nth_error_app2. rewrite tm_size_power2.
+  rewrite Nat.add_sub. apply map_nth_error. apply H0.
+  rewrite tm_size_power2. apply Nat.le_add_l.
+Qed.
 
+Lemma tm_step_next_range2' :
+  forall (n k : nat) (b : bool),
+  nth_error (tm_step n) k = Some b
+    -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
+Proof.
+  intros n k b. intros H. assert (I := H).
+  apply nth_error_split in H. destruct H. destruct H. inversion H.
+  rewrite tm_build.
+  assert (J: k < 2^n).
+  rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt.
+  rewrite nth_error_app2. rewrite tm_size_power2.
+  rewrite Nat.add_sub. apply map_nth_error. apply I.
+  rewrite tm_size_power2. apply Nat.le_add_l.
+Qed.
+
+Lemma tm_step_next_range2_neighbor : forall (n m k : nat),
+  S k < 2^n ->
+    eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
+    = eqb
+    (nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
+Proof.
+  intros n m k. intros H. rewrite <- tm_size_power2 in H.
+  assert (I := H). apply Nat.lt_succ_l in I.
+  assert (J : nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
+  generalize I. apply nth_error_nth'.
+  assert (K : nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
+  generalize H. apply nth_error_nth'.
+  assert (L := J). apply tm_step_next_range2' in L.
+  assert (M := K). apply tm_step_next_range2' in M.
+  destruct (nth k (tm_step n) false).
+  destruct (nth (S k) (tm_step n) false).
+  apply nth_error_nth with (d :=false) in L.
+  apply nth_error_nth with (d :=false) in M.
+  rewrite L. rewrite M. reflexivity.
+  apply nth_error_nth with (d :=false) in L.
+  apply nth_error_nth with (d :=false) in M.
+  rewrite L. rewrite M. reflexivity.
+  destruct (nth (S k) (tm_step n) false).
+  apply nth_error_nth with (d :=false) in L.
+  apply nth_error_nth with (d :=false) in M.
+  rewrite L. rewrite M. reflexivity.
+  apply nth_error_nth with (d :=false) in L.
+  apply nth_error_nth with (d :=false) in M.
+  rewrite L. rewrite M. reflexivity.
+Qed.
+
+
+
+
+
+
+
+
+nth_error_nth':
+  forall [A : Type] (l : list A) [n : nat] (d : A),
+  n < length l -> nth_error l n = Some (nth n l d)