Update

2022-12-10 13:24:01 +01:00 · 2022-12-10 13:24:01 +01:00 · 01a30e3733
commit 01a30e3733
parent 8a04d818b7
1 changed files with 140 additions and 4 deletions
--- a/thue-morse.v
+++ b/thue-morse.v
@ -1117,12 +1117,147 @@ Proof.
    + simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
 Qed.

+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.
+Proof.
+  intros n m k j. intros 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. assumption.
+  generalize J. generalize H0. apply Nat.le_lt_trans.
+
+  assert (N1: m < n). apply Nat.pow_lt_mono_r_iff in N0. assumption.
+  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 (N4: 0 < m-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
+  replace (m-j+j) with (m). assumption. 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.
+  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. assumption.
+    apply Nat.lt_le_incl. assumption.
+    apply Nat.lt_le_incl. assumption.
+  - 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. assumption.
+    apply Nat.lt_le_incl. assumption.
+Qed.
+
+Lemma tm_step_repeating_patterns :
+  forall (n m i j : nat),
+  i < m -> j < m
+  -> forall k, k < 2^n -> nth_error (tm_step m) (2^i)
+                        = nth_error (tm_step m) (2^j)
+                      <-> nth_error (tm_step (m+n)) (k * 2^m + (2^i))
+                        = nth_error (tm_step (m+n)) (k * 2^m + (2^j)).
+Proof.
+  intros n m i j. intros H I.
+  induction n.
+  - rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro.
+    rewrite H0. simpl. 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.
+      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.
+    + 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^i - 2^(m + n)) with ((k-2^n)*2^m + 2^i).
+      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.
+      rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
+      rewrite Nat.add_comm. reflexivity. assumption.
+
+      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.
+      assert (k*2^m <= k*2^m + 2^i). apply Nat.le_add_r.
+      generalize H2. generalize J. apply Nat.le_trans.
+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),
@ -1203,6 +1338,7 @@ Proof.
    rewrite Nat.mul_1_l. reflexivity. rewrite Nat.mul_1_l. reflexivity.
    apply N0.

+  TODO