Update

thue-morse.v

@@ -844,12 +844,73 @@ nth_error_Some:
  *)
 
 
-Lemma xxx : forall (a b : nat), a < b -> a <= b.
+(*
+nth_error_split:
+  forall [A : Type] (l : list A) (n : nat) [a : A],
+  nth_error l n = Some a ->
+  exists l1 l2 : list A, l = l1 ++ a :: l2 /\ length l1 = n
+ *)
+
+
+Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
+  l = l1 ++ b :: l2 -> length l1 < length l.
 Proof.
-  intros a b.
-  intros H.
-  induction a. destruct b. reflexivity. induction b.
-Admitted.
+  intros l l1 l2 b. intros H.
+  assert (I: l = (l1 ++ b::nil) ++ l2).
+  { rewrite H. rewrite <- app_assoc. reflexivity. }
+  assert (J: length (l1 ++ b::nil) <= length l).
+  { rewrite I.
+    replace (length ((l1 ++ [b]) ++ l2)) with
+      (length (l1 ++ [b]) + length l2).
+      apply Nat.le_add_r.
+    symmetry. apply app_length. }
+  rewrite last_length in J. assert (L: length l1 < S (length l1)).
+    apply Nat.lt_succ_diag_r. generalize J. generalize L.
+    apply Nat.lt_le_trans.
+Qed.
+
+Lemma list_concat_to_pos : forall (l l1 l2 : list bool) (b : bool),
+  l = l1 ++ b :: l2 -> nth_error l (length l1) = Some b.
+Proof.
+  intros l l1 l2 b. intros H.
+  assert (I: length l1 < length l). generalize H. apply list_app_length_lt.
+  assert (L: nth_error l (length l1) = Some (nth (length l1) l false)).
+  { apply nth_error_nth'. apply I. }
+  replace (nth (length l1) l false) with (nth (length l1) (l1++b::l2) false) in L.
+  rewrite nth_middle in L. apply L. rewrite H. reflexivity.
+Qed.
+
+
+(*
+Lemma nth_error_app : forall (l1 l2 : list bool) (k : nat),
+  nth_error (l1 ++ l2) (k + length l1) = nth_error l2 k.
+Proof.
+
+nth_error_app2:
+  forall [A : Type] (l l' : list A) [n : nat],
+  length l <= n -> nth_error (l ++ l') n = nth_error l' (n - length l)
+ *)
+
+
+Lemma tm_step_next_range :
+  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.
+  replace (length l1 + length (tm_step n) - length (tm_step n)) with (length l1).
+
+
+
+
+
+
 
 Lemma tm_step_consecutive_power2 :
   forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),
@@ -875,7 +936,7 @@ Proof.
   assert (k < n). { generalize H3. apply Nat.pow_lt_mono_r_iff. 
     apply Nat.lt_succ_diag_r. }
 
-
+    (* montrer que l1 ++ b1 :: b2 :: nil appartient à tm_step k *)