From 00fd7e39f1f64859aef788609e67abf916c574da Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 26 Nov 2022 14:00:51 +0100 Subject: [PATCH] Update --- thue-morse.v | 157 +++++++++++++++------------------------------------ 1 file changed, 45 insertions(+), 112 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index cf6f0c3..3b018c9 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1012,145 +1012,78 @@ Proof. easy. Qed. -Lemma tm_step_next_range2_neighbor : forall (n k : nat), - S k < 2^n -> - nth_error (tm_step n) k = nth_error (tm_step n) (S k) +Lemma tm_step_add_range2_flip_two : forall (n m j k : nat), + k < 2^n -> m < 2^n -> + nth_error (tm_step n) k = nth_error (tm_step n) m <-> - nth_error (tm_step (S n)) (k + 2^n) - = nth_error (tm_step (S n)) (S k + 2^n). + nth_error (tm_step (S n+j)) (k + 2^(n+j)) + = nth_error (tm_step (S n+j)) (m + 2^(n+j)). Proof. - intros n k. intros H. - (* Part 1: preamble *) - assert (I := H). apply Nat.lt_succ_l in I. - assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)). - generalize I. apply tm_step_next_range2. - assert (nth_error (tm_step n) (S k) <> nth_error (tm_step (S n)) (S k + 2^n)). - generalize H. apply tm_step_next_range2. - assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r. - rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H. - assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J. - - (* Part 2 *) - assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)). - generalize I. rewrite <- tm_size_power2. apply nth_error_nth'. - assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)). - generalize H. rewrite <- tm_size_power2. apply nth_error_nth'. - assert (nth_error (tm_step (S n)) (k + 2 ^ n) = - Some (nth (k + 2^n) (tm_step (S n)) false)). - generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2. - apply nth_error_nth'. - assert (nth_error (tm_step (S n)) (S k + 2 ^ n) = - Some (nth (S k + 2^n) (tm_step (S n)) false)). - generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2. - apply nth_error_nth'. - rewrite H2. rewrite H3. rewrite H4. rewrite H5. - - (* Part 3 *) - destruct (nth k (tm_step n) false). - destruct (nth (S k) (tm_step n) false). - destruct (nth (k + 2 ^ n) (tm_step (S n)) false). - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - easy. - rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity. - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity. - easy. - destruct (nth (k + 2 ^ n) (tm_step (S n)) false). - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity. - easy. - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - easy. - rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity. - destruct (nth (S k) (tm_step n) false). - destruct (nth (k + 2 ^ n) (tm_step (S n)) false). - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity. - easy. - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - easy. - rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity. - destruct (nth (k + 2 ^ n) (tm_step (S n)) false). - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - easy. - rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity. - destruct (nth (S k + 2 ^ n) (tm_step (S n)) false). - rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity. - easy. -Qed. - - -Lemma tm_step_add_range2_neighbor : forall (n m k : nat), - S k < 2^n -> - nth_error (tm_step n) k = nth_error (tm_step n) (S k) - <-> - nth_error (tm_step (S n+m)) (k + 2^(n+m)) - = nth_error (tm_step (S n+m)) (S k + 2^(n+m)). -Proof. - intros n m k. intros H. - assert (I := H). apply Nat.lt_succ_l in I. - assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r. - rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H. - assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J. + intros n m j k. intros H I. + assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r. + generalize H. apply Nat.add_lt_mono_r. + assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r. + generalize I. apply Nat.add_lt_mono_r. split. - - induction m. + - induction j. + intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r. - apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l. - apply K. - rewrite <- tm_step_next_range2_neighbor. - apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l. - apply K. - rewrite <- tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l. - rewrite <- tm_step_next_range2_neighbor. apply L. - apply H. rewrite <- Nat.add_succ_l. apply K. - rewrite <- Nat.add_succ_l. apply K. + rewrite <- tm_step_next_range2_flip_two. apply L. apply H. apply I. + intros L. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. - assert (S k < 2^(S n + m)). - assert (2^n < 2^(S n + m)). - assert (n < S n + m). assert (n < S n). apply Nat.lt_succ_diag_r. + assert (2^n < 2^(S n + j)). + assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r. generalize H0. apply Nat.lt_lt_add_r. generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. + assert (k < 2^(S n + j)). generalize H0. generalize H. apply Nat.lt_trans. - assert (H1 := H0). apply Nat.lt_succ_l in H1. + assert (m < 2^(S n + j)). + generalize H0. generalize I. apply Nat.lt_trans. - rewrite <- tm_step_next_range2_neighbor. + rewrite <- tm_step_next_range2_flip_two. - assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k). - generalize H1. generalize I. apply tm_step_stable. - assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)). - generalize H0. generalize H. apply tm_step_stable. - rewrite <- H2. rewrite <- H3. apply L. + assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k). + generalize H1. generalize H. apply tm_step_stable. + assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m). + generalize H2. generalize I. apply tm_step_stable. + rewrite <- H3. rewrite <- H4. apply L. - apply H0. - - induction m. + apply H1. apply H2. + - induction j. + intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L. - apply tm_step_next_range2_neighbor. apply H. apply L. + apply tm_step_next_range2_flip_two. apply H. apply I. apply L. + intros L. rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L. - assert (S k < 2^(S n + m)). - assert (2^n < 2^(S n + m)). - assert (n < S n + m). assert (n < S n). apply Nat.lt_succ_diag_r. + assert (2^n < 2^(S n + j)). + assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r. generalize H0. apply Nat.lt_lt_add_r. generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. + assert (k < 2^(S n + j)). generalize H0. generalize H. apply Nat.lt_trans. - assert (H1 := H0). apply Nat.lt_succ_l in H1. + assert (m < 2^(S n + j)). + generalize H0. generalize I. apply Nat.lt_trans. - rewrite <- tm_step_next_range2_neighbor in L. + rewrite <- tm_step_next_range2_flip_two in L. - assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k). - generalize H1. generalize I. apply tm_step_stable. - assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)). - generalize H0. generalize H. apply tm_step_stable. - rewrite <- H2 in L. rewrite <- H3 in L. apply L. + assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k). + generalize H1. generalize H. apply tm_step_stable. + assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m). + generalize H2. generalize I. apply tm_step_stable. + rewrite <- H3 in L. rewrite <- H4 in L. apply L. - apply H0. + apply H1. apply H2. Qed. + + + + + + + Lemma tm_step_cancel_high_bits : forall (k b n m : nat), (* every natral number k can be written according to the following form *)