Update

thue-morse.v

@@ -829,19 +829,65 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma tm_step_consecutive_pow2 :
+
+Search nth_error.
+(*
+nth_error_None:
+  forall [A : Type] (l : list A) (n : nat),
+  nth_error l n = None <-> length l <= n
+
+nth_error_Some:
+  forall [A : Type] (l : list A) (n : nat),
+  nth_error l n <> None <-> n < length l
+ *)
+
+
+Lemma xxx : forall (a b : nat), a < b -> a <= b.
+Proof.
+  intros a b.
+  intros H.
+  induction a. destruct b. reflexivity. induction b.
+Admitted.
+
+Lemma tm_step_consecutive_power2 :
   forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),
   tm_step n = l1 ++ b1 :: b2 :: l2
-    -> 2^k > S (length l1)
-      -> nth_error (tm_step n) ((length l1) + 2^k) = Some b1'
+  -> 2^k >= S (S (length l1)) (* TODO: remplacer par inégalité stricte plus jolie *)
+      -> nth_error (tm_step n) (length l1 + 2^k) = Some b1'
         -> nth_error (tm_step n) (S (length l1) + 2^k) = Some b2'
           -> (eqb b1 b2) = (eqb b1' b2').
 Proof.
   intros n k l1 l2 b1 b2 b1' b2'.
   intros.
+  (* on doit travailler sur tm_step (S k) et remarquer que b1 et b2 sont
+     dans la première moitié *)
+  (* on commence donc déjà par tm_step k pou rmontrer la présence dedans *)
+  assert (2^k < 2^n). {
+      assert (I: nth_error (tm_step n) (length l1 + 2^k) <> None).
+      rewrite H1. easy.
+      rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
+      assert (2^k <= length l1 + 2^k).
+      apply PeanoNat.Nat.le_add_l.
+      generalize I. generalize H3.
+      apply PeanoNat.Nat.le_lt_trans.
+    }
+
+  assert (k < n). {
+    generalize H3. apply PeanoNat.Nat.pow_lt_mono_r_iff. 
+
+
+
+
+  assert (I: exists (l3 : list bool), tm_step k = l1 ++ b1 :: b2 :: l3).
+  { 
+    }
 Admitted.
 
 
+
+
+
+
 Require Import BinPosDef.
 
 
@@ -852,12 +898,11 @@ Fixpoint tm_bin_rev (n: nat) : list bool :=
   | 0 => nil
   | S n' => let t := tm_bin_rev n' in
             let m := Pos.of_nat n' in
-              (xorb (hd true t)
-                (odd (Pos.size_nat
-         match Pos.lxor m (Pos.pred m) with
-         | N0 => BinNums.xH
-         | Npos(p)  => p
-         end))) :: t
+              (xorb (hd true t) (odd (Pos.size_nat
+                match Pos.lxor m (Pos.pred m) with
+                | N0 => BinNums.xH
+                | Npos(p)  => p
+                end))) :: t
   end.
 
 Fixpoint tm_bin (n: nat) : list bool :=
@@ -866,14 +911,15 @@ Fixpoint tm_bin (n: nat) : list bool :=
   | S n' => let t := tm_bin n' in
             let m := Pos.of_nat n' in
             t ++ [ xorb (last t true)
-                (odd (Pos.size_nat
-         match Pos.lxor m (Pos.pred m) with
-         | N0 => BinNums.xH
-         | Npos(p)  => p
-         end)) ]
+                     (odd (Pos.size_nat match Pos.lxor m (Pos.pred m) with
+                                        | N0 => BinNums.xH
+                                        | Npos(p)  => p
+                                        end)) ]
   end.
 
-Compute tm_bin 16 = tm_step 4.
+Theorem tm_morphism_eq_bin : forall (k : nat), tm_step k = tm_bin (2^k).
+Proof.
+Admitted.
 
 
 Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),