Update

thue-morse.v

@@ -1266,54 +1266,34 @@ Proof.
   generalize P. generalize I. apply Nat.lt_le_trans.
 Qed.
 
-
-Lemma tm_step_double_index : forall (n k: nat),
-  2^n <= k -> k < 2^(S n)
-  -> nth_error (tm_step (S n)) k = nth_error (tm_step (S (S n))) (2*k).
+Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
+  nth_error l k = nth_error (tm_morphism l) (2*k).
 Proof.
-  intros n k. intros H I.
-  destruct n.
-  - simpl in H. simpl in I. rewrite Nat.lt_succ_r in I.
-    assert (J: k = 1). generalize H. generalize I. apply Nat.le_antisymm.
-    rewrite J. reflexivity.
-  - symmetry. rewrite tm_build. rewrite nth_error_app2.
-    rewrite tm_size_power2.
+  intros l.
+  induction l.
+  - intro k.
+    simpl. replace (nth_error [] k) with (None : option bool).
+    rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
+    reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
+    symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
+  - intro k. induction k.
+    + rewrite Nat.mul_0_r. reflexivity.
+    + simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
+      replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
+      reflexivity.
+Qed.
 
-    assert (J: 2 ^ S (S n) <= 2 * k).
-    rewrite Nat.pow_succ_r'. apply Nat.mul_le_mono_l. assumption.
+Theorem tm_step_double_index : forall (n k : nat),
+  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
+Proof.
+  intros n k.
+  destruct k.
+  - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
+    rewrite tm_step_head_1. reflexivity.
+  - replace (tm_step (S n)) with (tm_morphism (tm_step n)).
+    rewrite tm_morphism_double_index. reflexivity. reflexivity.
+Qed.
 
-    assert (K: nth_error (tm_step (S (S n))) (2*k - 2^(S (S n)))
-    <> nth_error (tm_step (S (S (S n)))) (2*k - 2^(S (S n)) + 2^(S (S n)))).
-    apply tm_step_next_range2.
-    apply Nat.add_lt_mono_r with (p := 2^(S (S n))). rewrite Nat.sub_add.
-    replace (2*k) with (k+k). apply Nat.add_lt_mono ; assumption.
-    simpl. rewrite Nat.add_0_r. reflexivity. assumption.
-
-    rewrite Nat.sub_add in K.
-    replace (nth_error (tm_step (S (S (S n)))) (2 * k))
-      with (nth_error (tm_step (S (S n))) (2 * k)) in K.
-
-    rewrite nth_error_map.
-
-
-
-
-
-
-
-
-
-
-
-    destruct (nth_error (tm_step (S (S n))) (2 * k - 2 ^ S (S n)));
-    destruct (nth_error (tm_step (S (S n))) k).
-
-
-
-
-Lemma tm_step_next_range2 :
-  forall (n k : nat),
-  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).