Update

thue-morse.v

@@ -970,6 +970,138 @@ Proof.
   rewrite L. rewrite M. reflexivity.
 Qed.
 
+Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
+  S k < 2^n ->
+    nth_error (tm_step n) k = nth_error (tm_step n) (S k)
+    <->
+    nth_error (tm_step (S n+m)) (k + 2^(n+m))
+      = nth_error (tm_step (S n+m)) (S k + 2^(n+m)).
+Proof.
+  intros n m k. intros H.
+  assert (I := H). apply Nat.lt_succ_l in I.
+
+  split.
+  - assert (k < length (tm_step n)). rewrite tm_size_power2. apply I.
+    apply nth_error_nth' with (d :=false) in H0.
+    assert (S k < length (tm_step n)). rewrite tm_size_power2. apply H.
+    apply nth_error_nth' with (d :=false) in H1.
+    intros J. rewrite H0 in J. rewrite H1 in J.
+    apply tm_step_next_range2' in H0. apply tm_step_next_range2' in H1.
+    induction m.
+    + rewrite Nat.add_0_r. rewrite Nat.add_0_r.
+      rewrite H0. rewrite H1. inversion J. rewrite H3. reflexivity.
+    + 
+      assert (U: S k < 2^(S n+ m)).
+      assert (N: k < 2^n). apply I.
+      assert (L: 2^n < 2^(S n + m)).
+      assert (M: n < S n + m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
+      generalize L. generalize H. apply Nat.lt_trans.
+      assert (K := U). apply Nat.lt_succ_l in K.
+
+      assert (k < length (tm_step (S n + m))).
+      rewrite tm_size_power2. apply K.
+    apply nth_error_nth' with (d :=false) in H2.
+      assert (S k < length (tm_step (S n + m))).
+      rewrite tm_size_power2. apply U.
+    apply nth_error_nth' with (d :=false) in H3.
+    apply tm_step_next_range2' in H2. apply tm_step_next_range2' in H3.
+
+    rewrite Nat.add_succ_comm in H2. rewrite <- Nat.add_succ_l in H2.
+ rewrite Nat.add_succ_comm in H3. rewrite <- Nat.add_succ_l in H3.
+
+ rewrite H2. rewrite H3.
+
+     assert (nth_error (tm_step (n + S m)) k
+              = Some (nth k (tm_step (n + S m)) false)).
+              rewrite <- Nat.add_succ_comm. generalize K. rewrite <- tm_size_power2.
+              apply nth_error_nth'.
+     assert (nth_error (tm_step (n + S m)) (S k)
+              = Some (nth (S k) (tm_step (n + S m)) false)).
+              rewrite <- Nat.add_succ_comm. generalize U. rewrite <- tm_size_power2.
+              apply nth_error_nth'.
+
+
+Some (negb (nth (S k) (tm_step (n + S m)) false))
+
+Theorem tm_step_stable : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
+
+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)
+
+
+
+
+      assert (V: S k < 2^(n+m)).
+      assert (N: k < 2^n). apply I.
+      assert (L: 2^n <= 2^(n + m)).
+      assert (M: n <= n + m). apply Nat.le_add_r.
+      apply Nat.pow_le_mono_r. easy. apply M.
+      generalize L. generalize H. apply Nat.lt_le_trans.
+      assert (L := V). apply Nat.lt_succ_l in L.
+
+
+
+
+      assert (k < length (tm_step (n + S m))).
+      rewrite tm_size_power2. apply L.
+    apply nth_error_nth' with (d :=false) in H2.
+      assert (S k < length (tm_step (n + S m))).
+      rewrite tm_size_power2. apply V.
+    apply nth_error_nth' with (d :=false) in H3.
+
+
+      rewrite <- Nat.add_succ_comm in V.
+      rewrite <- Nat.add_succ_comm in L.
+
+
+      assert (k < length (tm_step (S n + S m))).
+      rewrite tm_size_power2. apply K.
+      apply nth_error_nth' with (d :=false) in H2.
+      assert (S k < length (tm_step (S n + S m))).
+      rewrite tm_size_power2. apply U.
+      apply nth_error_nth' with (d :=false) in H3.
+      
+      rewrite H2 in H3.
+
+    intros J. rewrite H0 in J. rewrite H1 in J. inversion J.
+    induction m. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
+    rewrite Bool.eqb_true_iff
+
+
+Lemma tm_step_next_range2_neighbor : forall (n 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).
+
+  - intros H1. induction m.
+    + rewrite Nat.add_0_r. rewrite Nat.add_0_r.
+
+nth_error_nth:
+  forall [A : Type] (l : list A) (n : nat) [x : A] (d : A),
+  nth_error l n = Some x -> nth n l d = x
+
+
+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)
+
+
+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).
+
+
+
+
+
+
+
 Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
   S k < 2^n ->
     eqb (nth k (tm_step n) false)