From f2d876f60be06415672f63bfea023dfbf32c1049 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 18:34:05 +0100 Subject: [PATCH] Update --- thue-morse.v | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 00f0e60..5f69f0b 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -974,16 +974,30 @@ Lemma tm_step_add_range2_neighbor : forall (n m k : nat), S k < 2^n -> eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false) = eqb - (nth (k + 2^n) (tm_step (n+m)) false) (nth (S k + 2^n) (tm_step (n+m)) false). + (nth (k + 2^n) (tm_step (S n+m)) false) (nth (S k + 2^n) (tm_step (S n+m)) false). Proof. - - - - -nth_error_nth': - forall [A : Type] (l : list A) [n : nat] (d : A), - n < length l -> nth_error l n = Some (nth n l d) - + intros n m k. intros H. + induction m. + - rewrite Nat.add_0_r. generalize H. apply tm_step_next_range2_neighbor. + - rewrite Nat.add_succ_r. + assert (I : + eqb (nth (k + 2 ^ n) (tm_step (S n + m)) false) + (nth (S k + 2 ^ n) (tm_step (S n + m)) false) + = +eqb (nth (k + 2 ^ n) (tm_step (S (S n + m))) false) + (nth (S k + 2 ^ n) (tm_step (S (S n + m))) false) + ). + assert (S k < 2^(S n + m)). + induction m. + + rewrite Nat.add_0_r. simpl. generalize H. + apply Nat.lt_lt_add_r. + + assert (2^n < 2^(S n + S m)). + assert (n < S n + S m). rewrite Nat.add_succ_comm. + apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. + generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1. + apply Nat.pow_lt_mono_r. generalize H0. generalize H. + apply Nat.lt_trans. + +