From d938efe215de4921729ea05318a3bf34ad3487fa Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 14:47:50 +0100 Subject: [PATCH] Update --- thue-morse.v | 453 +-------------------------------------------------- 1 file changed, 1 insertion(+), 452 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index c2b5c0a..1519df9 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1172,6 +1172,7 @@ Proof. apply Nat.lt_le_incl. assumption. Qed. +(* TODO: truc suivant inutile ? *) Lemma tm_step_repeating_patterns : forall (n m i j : nat), i < m -> j < m @@ -1404,458 +1405,6 @@ 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)). - - 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)). rewrite Nat.add_comm. - apply Nat.add_lt_mono with (p := 2^m) (q := 2^n) in O. - rewrite <- Nat.add_assoc in O. rewrite Nat.add_shuffle3 in O. - replace (2^m) with (1 * 2^m) in O at 2. rewrite <- Nat.mul_add_distr_r in O. - rewrite Nat.add_1_r in O. rewrite Nat.pow_succ_r'. - replace (2^n) with (1*2^n) in O. rewrite <- Nat.mul_add_distr_r in O. - rewrite Nat.add_1_r in O. apply O. - rewrite Nat.mul_1_l. reflexivity. rewrite Nat.mul_1_l. reflexivity. - apply N0. - - TODO - - - - - - - -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_nth' with (d := false). - rewrite nth_error_nth' with (d := false). - - - - (* -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 Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply I. - 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 Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply N. - generalize N. apply Nat.lt_le_incl. - - assert (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 N. generalize I. apply Nat.lt_trans. - apply Nat.lt_le_incl. generalize N. generalize I. apply Nat.lt_trans. - - 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. - generalize H4. apply Arith_prebase.le_plus_trans_stt. - 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), - 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 H I. - - (* - assert(J: nth_error (tm_step (S j)) 0 <> nth_error (tm_step (S j)) (2 ^ j)). - rewrite tm_build. rewrite nth_error_app1. rewrite nth_error_app2. - rewrite tm_size_power2. rewrite Nat.sub_diag. - rewrite tm_step_head_1. simpl. easy. - rewrite tm_size_power2. easy. - rewrite tm_size_power2. - rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - replace (nth_error (tm_step (S j)) 0) with (nth_error (tm_step m) 0) in J. - replace (nth_error (tm_step (S j)) (2^j)) with (nth_error (tm_step m) (2^j)) in J. - *) - - - (* à raccourcir avec tm_step build ! *) - assert (J: nth_error (tm_step j) 0 <> nth_error (tm_step (S j)) (2^j)). - replace (2^j) with (0 + 2^j). - apply tm_step_next_range2 with (k := 0). - rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. reflexivity. - assert (K: nth_error (tm_step j) 0 = nth_error (tm_step m) 0). - apply tm_step_stable. - rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - assert (L: nth_error (tm_step (S j)) (2^j) = nth_error (tm_step m) (2^j)). - apply tm_step_stable. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. - apply Nat.lt_succ_diag_r. - apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply I. - rewrite K in J. rewrite L in J. clear K. clear L. - (* fin du à raccourcir *) - - 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. - rewrite nth_error_app1. rewrite nth_error_app1. - apply IHn. apply H0. rewrite tm_size_power2. - - - - rewrite <- tm_size_power2 in H0. - rewrite <- nth_error_None in H0. - - - - - - - - - - - - (* - induction k. rewrite Nat.mul_0_l. rewrite Nat.add_0_l. - - assert(K: nth_error (tm_step n) 0 = nth_error (tm_step m) 0). - replace (nth_error (tm_step n) 0) with (Some false). - rewrite tm_step_head_1. simpl. reflexivity. - rewrite tm_step_head_1. simpl. reflexivity. - assert(L: nth_error (tm_step n) (2^j) = nth_error (tm_step m) (2^j)). - apply tm_step_stable. - *) - - -Lemma tm_step_next_range2 : - forall (n k : nat), - k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n). - -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. - - - - - *) - - - Lemma greedy_power2 : forall (n m : nat),