Update

thue-morse.v

@@ -993,128 +993,41 @@ Proof.
       assert (n < S n + S m). rewrite Nat.add_succ_comm.
       apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
       generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
-      apply Nat.pow_lt_mono_r. generalize H0. generalize H.
+      apply Nat.pow_lt_mono_r. generalize H0. generalize H. apply Nat.lt_trans.
-      apply Nat.lt_trans.
     + rewrite <- I. rewrite <- IHm.
 
       assert (U: S k < 2^(S n+m)).
       assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
-    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 (J: k < 2^n). apply Nat.lt_succ_l. apply H.
-
-      assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
-      generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
-      assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)).
-      generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
-
-      (*  assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false).  *)
-      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
-      generalize K. generalize J. apply tm_step_stable.
-
-      rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
-      rewrite H4.
-
-      assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
-      generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
-      assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
-
-      generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
-      
-      assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
-
-      generalize U. generalize H. apply tm_step_stable.
-      rewrite H3 in H6. rewrite H5 in H6.
-      inversion H6. rewrite H8.
-      reflexivity.
-Qed.
-
-
-Lemma tm_step_add_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+m)) (tm_step (S n+m)) false) (nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
-Proof.
-  intros n m k. intros H. induction m.
-  - rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply tm_step_next_range2_neighbor.
-    apply H.
-  - rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
-
-    assert (I : eqb (nth k (tm_step (S n + m)) false)
-                    (nth (S k) (tm_step (S n + m)) false)
-              = eqb (nth (k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)
-                    (nth (S k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)).
-    apply tm_step_next_range2_neighbor. induction m.
-    + rewrite Nat.add_0_r. simpl. generalize H.
-      apply Nat.lt_lt_add_r.
-    + assert (2^n < 2^(S n + S m)).
-      assert (n < S n + S m). rewrite Nat.add_succ_comm.
-      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
-      generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
-      apply Nat.pow_lt_mono_r. generalize H0. generalize H.
-      apply Nat.lt_trans.
-    + rewrite <- I. rewrite <- IHm.
-      assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
-      assert (K: k < 2^(S n+m)).
       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 J. apply Nat.lt_trans.
+      generalize L. generalize H. apply Nat.lt_trans.
+      assert (K := U). apply Nat.lt_succ_l in K.
+
+      assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
 
       assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
       generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
       assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)).
       generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
-
-      (*  assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false).  *)
       assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
       generalize K. generalize J. apply tm_step_stable.
-
+      rewrite <- H2 in H1. rewrite H0 in H1. inversion H1. rewrite H4.
-      rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
-      rewrite H4.
 
       assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
       generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
       assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
-
+      generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
-      assert (2^n < 2^(S n + m)).
-      assert (n < S n + m). rewrite Nat.add_succ_comm.
-      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
-      generalize H5.
-      apply Nat.pow_lt_mono_r.
-      apply Nat.lt_1_2.
-      assert (S k < 2^(S n + m)). generalize H5. generalize H.
-      apply Nat.lt_trans.
-
-      generalize H6. rewrite <- tm_size_power2. apply nth_error_nth'.
-
-      
       assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
-      assert (2^n < 2^(S n + m)).
+      generalize U. generalize H. apply tm_step_stable.
-      assert (n < S n + m). rewrite Nat.add_succ_comm.
+      rewrite H3 in H6. rewrite H5 in H6. inversion H6. rewrite H8. reflexivity.
-      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
-      generalize H6.
-      apply Nat.pow_lt_mono_r.
-      apply Nat.lt_1_2.
-      assert (S k < 2^(S n + m)). generalize H6. generalize H.
-      apply Nat.lt_trans.
-
-      generalize H7. generalize H. apply tm_step_stable.
-      rewrite H3 in H6. rewrite H5 in H6.
-      inversion H6. rewrite H8.
-      reflexivity.
 Qed.
 
 
 
 
+
 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)