From f0358d7381c0ad50b4160e9e66fb4bdf07e92f47 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 17:25:16 +0100 Subject: [PATCH] Update --- thue-morse.v | 102 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 71 insertions(+), 31 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index f777b86..ff505f7 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -872,37 +872,6 @@ Proof. apply list_app_length_lt in H0. rewrite H1 in H0. apply H0. Qed. -Lemma tm_step_next_range2 : - forall (n : nat) (l1 l2 : list bool) (b : bool), - tm_step n = l1 ++ b :: l2 - -> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b). -Proof. - intros n l1 l2 b. intros H. - assert (nth_error (tm_step n) (length l1) = Some b). - generalize H. apply list_concat_to_pos. - rewrite tm_build. - assert (I: length l1 < 2^n). - rewrite <- tm_size_power2. generalize H. apply list_app_length_lt. - rewrite nth_error_app2. rewrite tm_size_power2. - rewrite Nat.add_sub. apply map_nth_error. apply H0. - rewrite tm_size_power2. apply Nat.le_add_l. -Qed. - -Lemma tm_step_next_range2' : - forall (n k : nat) (b : bool), - nth_error (tm_step n) k = Some b - -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b). -Proof. - intros n k b. intros H. assert (I := H). - apply nth_error_split in H. destruct H. destruct H. inversion H. - rewrite tm_build. - assert (J: k < 2^n). - rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt. - rewrite nth_error_app2. rewrite tm_size_power2. - rewrite Nat.add_sub. apply map_nth_error. apply I. - rewrite tm_size_power2. apply Nat.le_add_l. -Qed. - Lemma tm_add_range : forall (n m k : nat), k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k. Proof. @@ -939,7 +908,78 @@ Proof. reflexivity. Qed. +Lemma tm_step_next_range2 : + forall (n : nat) (l1 l2 : list bool) (b : bool), + tm_step n = l1 ++ b :: l2 + -> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b). +Proof. + intros n l1 l2 b. intros H. + assert (nth_error (tm_step n) (length l1) = Some b). + generalize H. apply list_concat_to_pos. + rewrite tm_build. + assert (I: length l1 < 2^n). + rewrite <- tm_size_power2. generalize H. apply list_app_length_lt. + rewrite nth_error_app2. rewrite tm_size_power2. + rewrite Nat.add_sub. apply map_nth_error. apply H0. + rewrite tm_size_power2. apply Nat.le_add_l. +Qed. +Lemma tm_step_next_range2' : + forall (n k : nat) (b : bool), + nth_error (tm_step n) k = Some b + -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b). +Proof. + intros n k b. intros H. assert (I := H). + apply nth_error_split in H. destruct H. destruct H. inversion H. + rewrite tm_build. + assert (J: k < 2^n). + rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt. + rewrite nth_error_app2. rewrite tm_size_power2. + rewrite Nat.add_sub. apply map_nth_error. apply I. + rewrite tm_size_power2. apply Nat.le_add_l. +Qed. + +Lemma tm_step_next_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 (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. + 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'. + assert (K : nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)). + generalize H. apply nth_error_nth'. + assert (L := J). apply tm_step_next_range2' in L. + assert (M := K). apply tm_step_next_range2' in M. + destruct (nth k (tm_step n) false). + destruct (nth (S k) (tm_step n) false). + apply nth_error_nth with (d :=false) in L. + apply nth_error_nth with (d :=false) in M. + rewrite L. rewrite M. reflexivity. + apply nth_error_nth with (d :=false) in L. + apply nth_error_nth with (d :=false) in M. + rewrite L. rewrite M. reflexivity. + destruct (nth (S k) (tm_step n) false). + apply nth_error_nth with (d :=false) in L. + apply nth_error_nth with (d :=false) in M. + rewrite L. rewrite M. reflexivity. + apply nth_error_nth with (d :=false) in L. + apply nth_error_nth with (d :=false) in M. + rewrite L. rewrite M. reflexivity. +Qed. + + + + + + + + +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)