From d295196e0063256c2443b9ae063e3e638a791b4b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 15 Dec 2022 10:55:30 +0100 Subject: [PATCH] Update --- thue-morse.v | 70 +++++++++++++++++++--------------------------------- 1 file changed, 25 insertions(+), 45 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 0c9fe97..7ac71d5 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1266,54 +1266,34 @@ Proof. generalize P. generalize I. apply Nat.lt_le_trans. Qed. - -Lemma tm_step_double_index : forall (n k: nat), - 2^n <= k -> k < 2^(S n) - -> nth_error (tm_step (S n)) k = nth_error (tm_step (S (S n))) (2*k). +Lemma tm_morphism_double_index : forall (l : list bool) (k : nat), + nth_error l k = nth_error (tm_morphism l) (2*k). Proof. - intros n k. intros H I. - destruct n. - - simpl in H. simpl in I. rewrite Nat.lt_succ_r in I. - assert (J: k = 1). generalize H. generalize I. apply Nat.le_antisymm. - rewrite J. reflexivity. - - symmetry. rewrite tm_build. rewrite nth_error_app2. - rewrite tm_size_power2. + intros l. + induction l. + - intro k. + simpl. replace (nth_error [] k) with (None : option bool). + rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool). + reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l. + symmetry. apply nth_error_None. simpl. apply Nat.le_0_l. + - intro k. induction k. + + rewrite Nat.mul_0_r. reflexivity. + + simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl. + replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r. + reflexivity. +Qed. - assert (J: 2 ^ S (S n) <= 2 * k). - rewrite Nat.pow_succ_r'. apply Nat.mul_le_mono_l. assumption. +Theorem tm_step_double_index : forall (n k : nat), + nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k). +Proof. + intros n k. + destruct k. + - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl. + rewrite tm_step_head_1. reflexivity. + - replace (tm_step (S n)) with (tm_morphism (tm_step n)). + rewrite tm_morphism_double_index. reflexivity. reflexivity. +Qed. - assert (K: nth_error (tm_step (S (S n))) (2*k - 2^(S (S n))) - <> nth_error (tm_step (S (S (S n)))) (2*k - 2^(S (S n)) + 2^(S (S n)))). - apply tm_step_next_range2. - apply Nat.add_lt_mono_r with (p := 2^(S (S n))). rewrite Nat.sub_add. - replace (2*k) with (k+k). apply Nat.add_lt_mono ; assumption. - simpl. rewrite Nat.add_0_r. reflexivity. assumption. - - rewrite Nat.sub_add in K. - replace (nth_error (tm_step (S (S (S n)))) (2 * k)) - with (nth_error (tm_step (S (S n))) (2 * k)) in K. - - rewrite nth_error_map. - - - - - - - - - - - - destruct (nth_error (tm_step (S (S n))) (2 * k - 2 ^ S (S n))); - destruct (nth_error (tm_step (S (S n))) k). - - - - -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).