From b51cd1781adcee931317b97225822fccc2850780 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 28 Dec 2022 19:26:44 +0100 Subject: [PATCH] Update --- thue-morse.v | 118 --------------------------------------------------- 1 file changed, 118 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index d82db4a..5fec985 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -762,124 +762,6 @@ Qed. - replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1). - rewrite <- Nat.add_cancel_r with (p := 1). - rewrite Nat.sub_add. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_shuffle0. - rewrite <- Nat.add_assoc. - - - rewrite Nat.sub_succ. - rewrite <- Nat.add_cancel_r with (p := 1). - rewrite Nat.sub_add. rewrite <- Nat.add_assoc. - rewrite - - replace (S (2 * (S (2 * k) * 2 ^ m))) with (2 * (S (2 * k) * 2 ^ m) + 1). - rewrite <- Nat.add_cancel_r with (p := 1). - rewrite Nat.sub_add. - - - - - - - - - - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)); - destruct (nth_error (tm_step (S n0)) (2 * (S (2 * k) * 2 ^ m) - 1)). - destruct (b); destruct (b0); destruct (b1). - split. reflexivity. reflexivity. - destruct J. rewrite H0 in H. contradiction H. reflexivity. - reflexivity. simpl. split; reflexivity. - contradiction H. reflexivity. contradiction H. reflexivity. - simpl. split; reflexivity. - destruct J. rewrite H0 in H. contradiction H. reflexivity. - reflexivity. contradiction H. reflexivity. - destruct (b); destruct (b0). destruct J. rewrite H0. - split. intro J. inversion J. destruct H0. reflexivity. - intro J. simpl in J. symmetry in J. apply diff_false_true in J. - contradiction J. reflexivity. - split. intro K. inversion K. - - - apply Nat.lt_0_2. apply Nat.mul_comm. - - - -Lemma tm_step_repeating_patterns : - forall (n m i j : nat), - i < 2^m -> j < 2^m - -> forall k, k < 2^n -> nth_error (tm_step m) i - = nth_error (tm_step m) j - <-> nth_error (tm_step (m+n)) (k * 2^m + i) - = nth_error (tm_step (m+n)) (k * 2^m + j). - - - - - induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. - rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. - destruct n. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r. - intro H. apply Nat.neq_succ_0 in H. contradiction H. - rewrite <- tm_step_double_index. intro H. split. intro I. - symmetry in I. apply tm_step_succ_double_index in I. contradiction I. - apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H. - rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2. - intro I. apply diff_false_true in I. contradiction I. - - - intro H. - - induction m. - + rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. - rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. - destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H. - rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H. - rewrite <- tm_step_double_index. - split. - intro I. symmetry in I. - apply tm_step_succ_double_index in I. contradiction I. - rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H. - apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H. - rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2. - intro I. apply diff_false_true in I. contradiction I. - + - - - - split. - - induction m. - + rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. - rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. - destruct n. rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H. - rewrite Nat.lt_1_r in H. apply Nat.neq_succ_0 in H. contradiction H. - rewrite <- tm_step_double_index. intro I. symmetry in I. - apply tm_step_succ_double_index in I. contradiction I. - rewrite Nat.pow_0_r in H. rewrite Nat.mul_1_r in H. - apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H. - rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2. - + - - - - - - - -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. -Theorem tm_step_double_index : forall (n k : nat), - nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k). -Theorem tm_step_succ_double_index : forall (n k : nat), - k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)). - - - - - - - -