Update

thue-morse.v

@@ -1117,6 +1117,92 @@ Proof.
     + simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
 Qed.
 
+
+
+(* TODO: écrire deux lemmes, avec
+  - une implication vers la première moitié de la construction suivante
+  - une implication vers la seconde moitié de la construction suivante
+  ENSUITE : voir si on peut itérer sur le facteur multiplicatif k *)
+
+Lemma tm_step_add_small_power :
+  forall (n m k j : nat),
+  0 < k -> k * 2^m < 2^n -> j < m
+  -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j)
+  -> nth_error (tm_step (S n)) ((S k) * 2^m) <> nth_error (tm_step (S n)) ((S k) * 2^m + 2^j).
+Proof.
+  intros n m k j. intros G H I J.
+
+  assert (N0: 2^m < 2^n). assert (2^m <= k * 2^m).
+  replace (k * 2^m) with (1*2^m + (k-1)*2^m).
+  simpl. rewrite Nat.add_0_r. apply Nat.le_add_r.
+  rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_l.
+  rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_1_r. rewrite Nat.add_sub.
+  reflexivity. rewrite Nat.le_succ_l. apply G.
+  generalize H. generalize H0. apply Nat.le_lt_trans.
+
+  assert (N1: m < n). apply Nat.pow_lt_mono_r_iff in N0. apply N0.
+  apply Nat.lt_1_2.
+
+  assert (N2: 0 < m). assert (0 <= j). apply Nat.le_0_l.
+  generalize I. generalize H0. apply Nat.le_lt_trans.
+
+  assert (N3: 0 < n). destruct k. apply Nat.lt_irrefl in G. contradiction G.
+  assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
+  replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
+  apply Nat.le_0_l. reflexivity.
+  assert (2^m <= 2^m + k*2^m). apply Nat.le_add_r.
+  generalize H1. generalize H0. apply Nat.le_trans.
+  assert (2^0 < 2^n). generalize H. generalize H0.
+  apply Nat.le_lt_trans.
+  rewrite <- Nat.pow_lt_mono_r_iff in H1.
+  apply H1. apply Nat.lt_1_2.
+
+  assert (N4: 0 < m-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
+  replace (m-j+j) with (m). apply I. symmetry. apply Nat.sub_add.
+  generalize I. apply Nat.lt_le_incl.
+
+  assert (N5: j < n). generalize N1. generalize I. apply Nat.lt_trans.
+
+  assert (N6: 0 < n-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
+  replace (n-j+j) with (n). apply N5. symmetry. apply Nat.sub_add.
+  generalize N5. apply Nat.lt_le_incl.
+
+  assert (O: k * 2^m + 2^j < 2^n). 
+  replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
+  apply Nat.mul_lt_mono_pos_r.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  rewrite Nat.add_1_r. apply lt_even_even.
+  - destruct (m-j).
+    + apply Nat.lt_irrefl in N4. contradiction N4.
+    + rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_mul.
+      rewrite Nat.even_2. rewrite orb_true_r. reflexivity. apply Nat.le_0_l.
+  - destruct (n-j).
+    + apply Nat.lt_irrefl in N6. contradiction N6.
+    + rewrite Nat.pow_succ_r. rewrite Nat.even_mul.
+      rewrite Nat.even_2. rewrite orb_true_l. reflexivity. apply Nat.le_0_l.
+  - apply Nat.mul_lt_mono_pos_r with (p := 2^j).
+    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+    rewrite <- Nat.pow_add_r.
+    rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
+    rewrite Nat.sub_add. rewrite Nat.sub_add. apply H.
+    apply Nat.lt_le_incl. apply N5.
+    apply Nat.lt_le_incl. apply I.
+  - rewrite Nat.mul_add_distr_r.
+    rewrite <- Nat.mul_assoc.
+    rewrite <- Nat.pow_add_r. rewrite Nat.mul_1_l. rewrite Nat.sub_add.
+    rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. reflexivity.
+    apply Nat.lt_le_incl. apply N5.
+    apply Nat.lt_le_incl. apply I.
+  - assert ((S k)*2^m + 2^j < 2^(S n)).
+    apply Nat.add_lt_mono with (p := 2^m) (q := 2^n) in O.
+
+
+
+
+
+
+
+
 Lemma tm_step_add_small_power :
   forall (n m k j : nat),
   1 < k -> k * 2^m < 2^n -> j < m
@@ -1245,11 +1331,10 @@ Proof.
       * rewrite tm_size_power2. apply H0.
     +
 
-
       rewrite nth_error_app2. rewrite nth_error_app2.
       rewrite tm_size_power2.
-      rewrite nth_error_map.
-      rewrite nth_error_map.
+      rewrite nth_error_nth' with (d := false).
+      rewrite nth_error_nth' with (d := false).