From 2786ad33bd18cca24603b7a18f6d43236c447fb9 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 15 Dec 2022 15:38:08 +0100 Subject: [PATCH] Update --- thue-morse.v | 84 ++++++++++++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 38 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 039b975..c8045d6 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -35,7 +35,7 @@ Qed. Lemma negb_double_map : forall (l : list bool), map negb (map negb l) = l. Proof. - intros l. + intro l. induction l. - reflexivity. - simpl. rewrite IHl. replace (negb (negb a)) with (a). @@ -54,7 +54,7 @@ Qed. Lemma tm_morphism_rev : forall (l : list bool), rev (tm_morphism l) = tm_morphism (map negb (rev l)). Proof. - intros l. induction l. + intro l. induction l. - reflexivity. - simpl. rewrite negb_map_explode. rewrite IHl. rewrite tm_morphism_concat. @@ -62,10 +62,19 @@ Proof. rewrite negb_involutive. reflexivity. Qed. +Lemma tm_morphism_rev' : forall (l : list bool), + rev (tm_morphism l) = map negb (tm_morphism (rev l)). +Proof. + intro l. rewrite tm_morphism_rev. induction l. + - reflexivity. + - simpl. rewrite map_app. rewrite tm_morphism_concat. rewrite IHl. + rewrite tm_morphism_concat. rewrite map_app. reflexivity. +Qed. + Lemma tm_morphism_double_index : forall (l : list bool) (k : nat), nth_error l k = nth_error (tm_morphism l) (2*k). Proof. - intros l. + intro l. induction l. - intro k. simpl. replace (nth_error [] k) with (None : option bool). @@ -82,7 +91,7 @@ Qed. Lemma tm_build_negb : forall (l : list bool), tm_morphism (map negb l) = map negb (tm_morphism l). Proof. - intros l. + intro l. induction l. - reflexivity. - simpl. rewrite IHl. reflexivity. @@ -92,13 +101,23 @@ Qed. Lemma tm_step_lemma : forall n : nat, tm_morphism (tm_step n) = tm_step (S n). Proof. - intros n. reflexivity. + intro n. reflexivity. +Qed. + +Theorem tm_step_negb : forall (n : nat), + map negb (tm_step (S n)) = rev (tm_morphism (rev (tm_step n))). +Proof. + intro n. + rewrite <- tm_step_lemma. symmetry. + replace (tm_step n) with (rev (rev (tm_step n))). + rewrite rev_involutive. rewrite tm_morphism_rev'. reflexivity. + rewrite rev_involutive. reflexivity. Qed. Theorem tm_build : forall (n : nat), tm_step (S n) = tm_step n ++ map negb (tm_step n). Proof. - intros n. + intro n. induction n. - reflexivity. - simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat. @@ -109,7 +128,7 @@ Qed. Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n. Proof. - intros n. + intro n. induction n. - reflexivity. - rewrite tm_build. rewrite app_length. rewrite map_length. @@ -120,7 +139,7 @@ Qed. Lemma tm_step_head_2 : forall (n : nat), tm_step (S n) = false :: true :: tl (tl (tm_step (S n))). Proof. - intros n. + intro n. induction n. - reflexivity. - simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)). @@ -130,7 +149,7 @@ Qed. Lemma tm_step_end_2 : forall (n : nat), rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))). Proof. - intros n. induction n. + intro n. induction n. - reflexivity. - simpl tm_step. rewrite tm_morphism_rev. replace (tm_morphism (tm_step n)) with (tm_step (S n)). @@ -144,7 +163,8 @@ Qed. Lemma tm_step_head_1 : forall (n : nat), tm_step n = false :: tl (tm_step n). Proof. - intros n. destruct n. + intro n. + destruct n. - reflexivity. - rewrite tm_step_head_2. reflexivity. Qed. @@ -152,7 +172,7 @@ Qed. Lemma tm_step_end_1 : forall (n : nat), rev (tm_step n) = odd n :: tl (rev (tm_step n)). Proof. - intros n. + intro n. destruct n. - reflexivity. - rewrite tm_step_end_2. simpl. @@ -174,7 +194,7 @@ Qed. Lemma tm_step_single_bit_index : forall (n : nat), nth_error (tm_step (S n)) (2^n) = Some true. Proof. - intros n. + intro n. rewrite tm_build. rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag. replace (true) with (negb false). apply map_nth_error. @@ -182,39 +202,27 @@ Proof. reflexivity. rewrite tm_size_power2. easy. Qed. + Lemma tm_step_repunit_index : forall (n : nat), nth_error (tm_step n) (2^n - 1) = Some (odd n). Proof. - intros n. + intro n. rewrite nth_error_nth' with (d := false). replace (tm_step n) with (rev (rev (tm_step n))). - rewrite rev_nth. rewrite rev_length. - rewrite tm_size_power2. rewrite <- Nat.sub_succ_l. - rewrite Nat.sub_succ. rewrite Nat.sub_0_r. - rewrite Nat.sub_diag. rewrite tm_step_end_1. - reflexivity. - - rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1. - rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn. - simpl in IHn. rewrite Nat.mul_comm in IHn. - rewrite <- Nat.pow_succ_r in IHn. apply IHn. - apply Nat.le_0_l. apply Nat.lt_0_2. - + rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2. + rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag. + rewrite tm_step_end_1. reflexivity. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. rewrite rev_length. rewrite tm_size_power2. - rewrite Nat.sub_1_r. apply Nat.lt_pred_l. - apply Nat.pow_nonzero. easy. - - rewrite rev_involutive. reflexivity. - rewrite tm_size_power2. - rewrite Nat.sub_1_r. apply Nat.lt_pred_l. - apply Nat.pow_nonzero. easy. + rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. + apply rev_involutive. rewrite tm_size_power2. + rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. Qed. - Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool), l = l1 ++ b :: l2 -> length l1 < length l. Proof. - intros l l1 l2 b. intros H. rewrite H. + intros l l1 l2 b. intro H. rewrite H. rewrite app_length. simpl. apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. Qed. @@ -223,7 +231,7 @@ Lemma tm_step_next_range : forall (n k : nat) (b : bool), nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b. Proof. - intros n k b. intros H. assert (I := H). + intros n k b. intro H. assert (I := H). apply nth_error_split in H. destruct H. destruct H. inversion H. rewrite tm_build. rewrite nth_error_app1. apply I. apply list_app_length_lt in H0. rewrite H1 in H0. apply H0. @@ -232,7 +240,7 @@ Qed. 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. + intros n m k. intro H. induction m. - rewrite Nat.add_comm. reflexivity. - rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H. @@ -269,7 +277,7 @@ 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). Proof. - intros n k. intros H. + intros n k. intro H. rewrite tm_build. rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub. assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)). @@ -289,7 +297,7 @@ Lemma tm_step_next_range2_flip_two : forall (n k m : nat), nth_error (tm_step (S n)) (k + 2^n) = nth_error (tm_step (S n)) (m + 2^n). Proof. - intros n k m. intros H. intros I. + intros n k m. intro H. intro I. (* Part 1: preamble *) assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).