Update

thue-morse.v

@@ -1256,16 +1256,155 @@ Proof.
       generalize H2. generalize J. apply Nat.le_trans.
 Qed.
 
+Lemma tm_step_add_small_power2 :
+  forall (n m j : nat),
+  j < m
+  -> forall k, k < 2^n -> nth_error (tm_step m) 0
+                        = nth_error (tm_step m) (2^j)
+                      <-> nth_error (tm_step (m+n)) (k * 2^m )
+                        = nth_error (tm_step (m+n)) (k * 2^m + (2^j)).
+Proof.
+  intros n m j. intros H.
+  induction n.
+  - rewrite Nat.add_0_r. intro k. intro. simpl in H0.
+    assert (k = 0). generalize H0. apply Nat.lt_1_r.
+    rewrite H1. easy.
+  - rewrite Nat.add_succ_r. intro k. intro.
+    rewrite tm_build.
+    assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases.
+    destruct S.
+
+    assert (k*2^m < 2^(m+n)).
+    destruct k.
+    + simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+    + rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
+      rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
+      assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+    + rewrite nth_error_app1. rewrite nth_error_app1.
+      generalize H1. apply IHn.
+
+      rewrite tm_size_power2.
+      assert (k * 2^m + 2^j < 2^(m+n)).
+      destruct k. simpl. apply Nat.log2_lt_cancel.
+      rewrite Nat.log2_pow2. rewrite Nat.log2_pow2.
+      apply Nat.lt_lt_add_r. assumption. apply Nat.le_0_l. apply Nat.le_0_l.
+      generalize H2. apply lt_split_bits.
+      apply Nat.lt_0_succ. assumption. assumption.
+
+      rewrite tm_size_power2. assumption.
+    + assert (J: 2 ^ (m + n) <= k * 2 ^ m).  
+      rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
+      apply Nat.mul_le_mono_r. assumption.
+
+      rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.
+
+      assert (forall a b, option_map negb a = option_map negb b <-> a = b).
+      intros a b. destruct a. destruct b. destruct b0. destruct b.
+      simpl. split. intro. reflexivity. intro. reflexivity.
+      simpl. split. intro. inversion H2. intro. inversion H2.
+      destruct b. simpl. split. intro. inversion H2. intro. inversion H2.
+      simpl. split. intro. reflexivity. intro. reflexivity.
+      split. intro. inversion H2. intro. inversion H2.
+      destruct b. split. intro. inversion H2. intro. inversion H2.
+      split. intro. reflexivity. intro. reflexivity.
+
+      replace (k * 2 ^ m - 2^(m + n)) with ((k-2^n)*2^m).
+      replace (k * 2 ^ m + 2^j - 2^(m + n)) with ((k-2^n)*2^m + 2^j).
+      rewrite nth_error_map. rewrite nth_error_map.
+
+      rewrite H2. apply IHn.
+      rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
+      rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0.
+      rewrite Nat.mul_add_distr_r in H0. simpl in H0.
+      rewrite Nat.add_0_r in H0. assumption. reflexivity.
+      apply Nat.le_0_l. assumption.
+
+      rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
+      rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
+      rewrite Nat.add_comm. reflexivity. assumption.
+
+      rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
+      replace (n+m) with (m+n). reflexivity.
+      rewrite Nat.add_comm. reflexivity.
+
+      rewrite tm_size_power2.
+      assert (k*2^m <= k*2^m + 2^j). apply Nat.le_add_r.
+      generalize H2. generalize J. apply Nat.le_trans.
+
+      rewrite tm_size_power2. assumption.
+Qed.
+
 
 
 
 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).
+  0 < k -> j < m -> k * 2^m < 2^n
+  -> 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 G H I J.
+  intros n m k j. intros G H I.
+
+  assert ( nth_error (tm_step m) 0
+         = nth_error (tm_step m) (2^j)
+       <-> nth_error (tm_step (m+n)) (k * 2^m)
+         = nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ).
+  apply tm_step_add_small_power2.
+  assumption.
+  assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg.
+  apply Nat.le_0_1. rewrite Nat.le_succ_l.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0.
+  rewrite Nat.mul_comm in H0.
+  generalize I. generalize H0. apply Nat.le_lt_trans.
+
+  replace (nth_error (tm_step (m + n)) (k * 2 ^ m))
+    with (nth_error (tm_step n) (k * 2 ^ m)) in H0.
+  replace (nth_error (tm_step (m + n)) (k * 2 ^ m + 2^j))
+    with (nth_error (tm_step n) (k * 2 ^ m + 2^j)) in H0.
+  replace (nth_error (tm_step m) 0) with (Some false) in H0.
+  replace (nth_error (tm_step m) (2^j)) with (Some true) in H0.
+
+  destruct (nth_error (tm_step n) (k * 2 ^ m)).
+  destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
+  destruct b. destruct b0.
+  destruct H0.
+  assert (Some true = Some true). reflexivity.
+  apply H1 in H2. rewrite <- H2 at 1. easy. easy.
+  destruct b0. easy. destruct H0.
+  assert (Some false = Some false). reflexivity.
+  apply H1 in H2. rewrite H2 at 1. easy. easy.
+  rewrite nth_error_nth' with (d := false). easy.
+  rewrite tm_size_power2. apply lt_split_bits.
+  assumption. assumption. assumption.
+
+
+Lemma lt_split_bits : forall n m k j,
+  0 < k -> j < m -> k * 2^m < 2^n -> k * 2^m +2^j < 2^n.
+
+nth_error_nth':
+  forall [A : Type] (l : list A) [n : nat] (d : A),
+  n < length l -> nth_error l n = Some (nth n l d)
+
+
+
+Theorem tm_step_stable : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
+
+
+
+
+Nat.mul_le_mono_nonneg:
+  forall n m p q : nat,
+  0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q
+
+
+Lemma tm_step_add_small_power2 :
+  forall (n m j : nat),
+  j < m
+  -> forall k, k < 2^n -> nth_error (tm_step m) 0
+                        = nth_error (tm_step m) (2^j)
+                      <-> nth_error (tm_step (m+n)) (k * 2^m )
+                        = nth_error (tm_step (m+n)) (k * 2^m + (2^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).