From ba5ba7b2da987d08da34970dfb75b8106631177b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 17:33:35 +0100 Subject: [PATCH] Update --- thue-morse.v | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index ff505f7..00f0e60 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -872,7 +872,7 @@ Proof. apply list_app_length_lt in H0. rewrite H1 in H0. apply H0. Qed. -Lemma tm_add_range : forall (n m k : nat), +Lemma tm_step_add_range : forall (n m k : nat), k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k. Proof. intros n m k. intros H. @@ -892,14 +892,14 @@ Proof. intros n m k. intros. assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n). apply Nat.max_spec. destruct I. - - destruct H1. replace (m) with (n + (m-n)). apply tm_add_range. apply H. + - destruct H1. replace (m) with (n + (m-n)). apply tm_step_add_range. apply H. apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1. apply Nat.add_sub_assoc. rewrite Nat.add_comm. assert (n <= n). apply le_n. symmetry. replace (m) with (m + (n-n)) at 1. generalize H3. apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm. reflexivity. - - destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_add_range. + - destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range. apply H0. replace (n) with (m + n - m) at 2. generalize H1. apply Nat.add_sub_assoc. rewrite Nat.add_comm. assert (m <= m). apply le_n. symmetry. @@ -939,13 +939,13 @@ Proof. rewrite tm_size_power2. apply Nat.le_add_l. Qed. -Lemma tm_step_next_range2_neighbor : forall (n m k : nat), +Lemma tm_step_next_range2_neighbor : forall (n 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 (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false). Proof. - intros n m k. intros H. rewrite <- tm_size_power2 in H. + intros n k. intros H. rewrite <- tm_size_power2 in H. assert (I := H). apply Nat.lt_succ_l in I. assert (J : nth_error (tm_step n) k = Some (nth k (tm_step n) false)). generalize I. apply nth_error_nth'. @@ -970,9 +970,12 @@ Proof. rewrite L. rewrite M. reflexivity. Qed. - - - +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). +Proof.