Update

thue-morse.v

@@ -1117,8 +1117,143 @@ Proof.
     + simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
 Qed.
 
-Require Import Arith_prebase.
+Lemma tm_step_add_small_power :
+  forall (n m k j : nat),
+  1 < 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).
+Proof.
+  intros n m k j. intros J H I.
 
+  assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
+  rewrite Nat.add_0_r. rewrite Nat.add_comm.
+  replace (m-j+j) with (m). apply I. symmetry. apply Nat.sub_add.
+  generalize I. apply Nat.lt_le_incl.
+
+  induction n.
+  - simpl. destruct k.
+    + (* hypothèse vraie : k = 0 *)
+      simpl. assert (0 < 2^j).
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+      assert (nth_error [false] (2^j) = None).
+      apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
+      rewrite H1. easy.
+    + (* hypothèse fausse : contradiction en H *)
+      assert ((S k) * (2^m) <> 0).
+      rewrite <- Nat.neq_mul_0.
+      split. easy. apply Nat.pow_nonzero. easy.
+      rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
+      rewrite H in H0. contradiction H0. reflexivity.
+  - rewrite tm_build.
+    assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
+    destruct S.
+    +
+      (* m < n *)
+      assert (N: m < n). apply Nat.lt_le_incl in H0.
+      apply Nat.log2_le_mono in H0.
+      rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
+      generalize H0. assert (m < m + Nat.log2 k).
+      apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
+      generalize H1. apply Nat.lt_le_trans.
+      apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
+      apply Nat.le_0_l.
+
+      assert (0 < n-m).
+      rewrite Nat.add_lt_mono_l with (p := m).
+
+  rewrite Nat.add_0_r. rewrite Nat.add_comm.
+  replace (n-m+m) with (n). apply N. symmetry. apply Nat.sub_add.
+  generalize N. apply Nat.lt_le_incl.
+
+      assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
+  rewrite Nat.add_0_r. rewrite Nat.add_comm.
+  replace (n-j+j) with (n). generalize N. generalize I. apply Nat.lt_trans.
+  symmetry. apply Nat.sub_add.
+  assert (j < n). generalize N. generalize I. apply Nat.lt_trans.
+  generalize H2. apply Nat.lt_le_incl.
+
+      rewrite nth_error_app1. rewrite nth_error_app1.
+      apply IHn. apply H0. rewrite tm_size_power2.
+
+      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.
+
+      assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
+      generalize I. generalize H3. apply Nat.le_lt_trans.
+
+      assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
+      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 H5. generalize H4. apply Nat.le_trans.
+
+      assert (2^0 < 2^n). generalize H0. generalize H4.
+      apply Nat.le_lt_trans.
+
+      rewrite <- Nat.pow_lt_mono_r_iff in H5.
+      apply H5. apply Nat.lt_1_2.
+
+      assert (S (k*2^m) < 2^n). apply lt_even_even.
+      rewrite Nat.even_mul.
+
+      assert (Nat.even (2^m) = true). destruct m.
+      * apply Nat.lt_irrefl in H3. contradiction H3.
+      * rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        reflexivity. apply Nat.le_0_l.
+      * destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
+      * destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
+
+        destruct n.
+        apply Nat.lt_irrefl in H2. contradiction H2.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        reflexivity. apply Nat.le_0_l.
+      * apply H0.
+      * rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
+
+        destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
+
+        destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
+        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
+        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 H0.
+
+        apply Nat.lt_le_incl.
+        generalize N. generalize I. apply Nat.lt_trans.
+        apply Nat.lt_le_incl. apply I.
+      * rewrite <- Nat.pow_add_r.
+        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.sub_add.
+        reflexivity.
+        apply Nat.lt_le_incl.
+        generalize N. generalize I. apply Nat.lt_trans.
+        apply Nat.lt_le_incl. apply I.
+      * 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.
+
+
+
+      (*
 Lemma tm_step_add_small_power :
   forall (n m k j : nat),
   1 < k -> k * 2^m < 2^n -> j < m
@@ -1130,30 +1265,6 @@ Proof.
   rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply I.
   generalize I. apply Nat.lt_le_incl.
 
-
-  (*
-        destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
-        rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
-        simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
-   *)
-  (*
-   *)
-
-  (*
-        assert (0 < n-m).
-        rewrite Nat.add_lt_mono_l with (p := m).
-        rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply H4.
-        generalize H4. apply Nat.lt_le_incl.
-   *)
-
-  (*
-  assert (N: 0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
-  rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r.
-  generalize I. generalize I. apply Nat.lt_trans.
-  apply Nat.lt_le_incl. generalize H4. generalize I. apply Nat.lt_trans.
-   *)
-
-
   induction n.
   - simpl. destruct k.
     + (* hypothèse vraie : k = 0 *)
@@ -1251,10 +1362,22 @@ Proof.
         apply Nat.lt_le_incl.
         generalize N. generalize I. apply Nat.lt_trans.
         apply Nat.lt_le_incl. apply I.
-      *
-
+      * rewrite <- Nat.pow_add_r.
+        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.sub_add.
+        reflexivity.
+        apply Nat.lt_le_incl.
+        generalize N. generalize I. apply Nat.lt_trans.
+        apply Nat.lt_le_incl. apply I.
+      * 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.
 
 
 
@@ -1356,7 +1479,7 @@ Theorem tm_step_stable : forall (n m k : nat),
 
 
 
-
+       *)