diff --git a/thue-morse.v b/thue-morse.v index 47a9065..5ea11fb 100644 --- a/thue-morse.v +++ b/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), - + *)