From 44ae80ab27835a0c8f36aa4751a662e1470f0e18 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 4 Jan 2023 16:12:03 +0100 Subject: [PATCH] Update --- thue-morse.v => thue_morse.v | 339 +++++++++++++---------------------- 1 file changed, 127 insertions(+), 212 deletions(-) rename thue-morse.v => thue_morse.v (90%) diff --git a/thue-morse.v b/thue_morse.v similarity index 90% rename from thue-morse.v rename to thue_morse.v index 9f6521a..8a3a41d 100644 --- a/thue-morse.v +++ b/thue_morse.v @@ -1,7 +1,8 @@ -(* +(** Some proofs related to the Thue-Morse sequence. - See https://oeis.org/A010060 - https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence + See: + - https://oeis.org/A010060 + - https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence *) Require Import Coq.Lists.List. @@ -12,9 +13,9 @@ Require Import Bool. Import ListNotations. -(* +(** This whole notebook contains proofs related to the following two functions. - Nothing else is defined afterwards. + Nothing else is defined afterwards in the current notebook. *) Fixpoint tm_morphism (l:list bool) : list bool := @@ -30,7 +31,7 @@ Fixpoint tm_step (n: nat) : list bool := end. -(* +(** More or less "general" lemmas, which are not directly related to the previous functions are proved below. *) @@ -96,7 +97,7 @@ Proof. Qed. -(* +(** Some lemmas related to the first function (tm_morphism) are proved here. They have a wider scope than the following ones since they don't focus on the Thue-Morse sequence by itself. @@ -281,7 +282,7 @@ Proof. Qed. -(* +(** Lemmas and theorems below are related to the second function defined initially. They focus on the Thue-Morse sequence. *) @@ -369,22 +370,25 @@ Proof. Qed. Lemma tm_step_repunit_index : forall (n : nat), - nth_error (tm_step n) (2^n - 1) = Some (odd n). + nth_error (tm_step n) (pred (2^n)) = Some (odd n). Proof. intro n. - assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2. - rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy. - + rewrite <- Nat.sub_1_r. rewrite <- tm_size_power2. 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_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag. - rewrite tm_step_end_1. reflexivity. + rewrite <- rev_nth. rewrite tm_step_end_1. simpl. + reflexivity. + rewrite tm_size_power2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - rewrite rev_length. assumption. apply rev_involutive. assumption. + rewrite Nat.sub_1_r. apply Nat.lt_pred_l. + rewrite tm_size_power2. apply Nat.pow_nonzero. easy. Qed. +(** + The following lemmas and theorems focus on the stability of the sequence: + while lists in the sequence get longer and longer, the beginning of a + longer list contain the same elements as the previous shorter lists. +*) 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. @@ -432,6 +436,94 @@ Proof. reflexivity. Qed. +(** + The following lemma states that a block of terms in the Thue-Morse + sequence having a size being a power of 2 is repeated, either + as an identical version or with all values together flipped. +*) + +Lemma tm_step_repeating_patterns : + forall (n m i j : nat), + i < 2^m -> j < 2^m + -> forall k, k < 2^n -> nth_error (tm_step m) i + = nth_error (tm_step m) j + <-> nth_error (tm_step (m+n)) (k * 2^m + i) + = nth_error (tm_step (m+n)) (k * 2^m + j). +Proof. + intros n m i j. intros H I. + induction n. + - rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro. + rewrite H0. simpl. easy. + - rewrite Nat.add_succ_r. intro k. intro. + rewrite tm_build. + assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases. + destruct S. + + assert (k*2^m < 2^(m+n)). + destruct k. + + simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + + rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1. + rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm. + assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + + assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))). + intro l. intro M. rewrite tm_size_power2. + destruct k. simpl. assert (2^m <= 2^(m+n)). + apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r. + generalize H3. generalize M. apply Nat.lt_le_trans. + apply lt_split_bits. apply Nat.lt_0_succ. assumption. + assumption. + + rewrite nth_error_app1. rewrite nth_error_app1. + generalize H1. apply IHn. + apply L. assumption. apply L. assumption. + + + assert (J: 2 ^ (m + n) <= k * 2 ^ m). + rewrite Nat.pow_add_r. rewrite Nat.mul_comm. + apply Nat.mul_le_mono_r. assumption. + + rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2. + + assert (forall a b, option_map negb a = option_map negb b <-> a = b). + intros a b. destruct a. destruct b. destruct b0; destruct b; simpl. + split; intro; reflexivity. split; intro; inversion H2. + split; intro; inversion H2. split; intro; reflexivity. + split; intro; inversion H2. + destruct b. split; intro; inversion H2. split; intro; reflexivity. + + replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i). + replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j). + rewrite nth_error_map. rewrite nth_error_map. + + rewrite H2. apply IHn. + rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add. + rewrite Nat.pow_succ_r in H0. rewrite <- Nat.add_1_r in H0 at 1. + rewrite Nat.mul_add_distr_r in H0. simpl in H0. + rewrite Nat.add_0_r in H0. assumption. + apply Nat.le_0_l. assumption. + + rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity. + rewrite Nat.add_comm. reflexivity. assumption. + + rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity. + rewrite Nat.add_comm. reflexivity. assumption. + + rewrite tm_size_power2. + assert (k*2^m <= k*2^m + j). apply Nat.le_add_r. + generalize H2. generalize J. apply Nat.le_trans. + + rewrite tm_size_power2. + assert (k*2^m <= k*2^m + i). apply Nat.le_add_r. + generalize H2. generalize J. apply Nat.le_trans. +Qed. + +(** + The following lemmas and theorems are related to flipping the + most significant bit in the numerical value of indices (of terms + in the lists). +*) + 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). @@ -583,81 +675,12 @@ Proof. apply H1. apply H2. Qed. -Lemma tm_step_repeating_patterns : - forall (n m i j : nat), - i < 2^m -> j < 2^m - -> forall k, k < 2^n -> nth_error (tm_step m) i - = nth_error (tm_step m) j - <-> nth_error (tm_step (m+n)) (k * 2^m + i) - = nth_error (tm_step (m+n)) (k * 2^m + j). -Proof. - intros n m i j. intros H I. - induction n. - - rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro. - rewrite H0. simpl. easy. - - rewrite Nat.add_succ_r. intro k. intro. - rewrite tm_build. - assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases. - destruct S. +(** + The following lemmas and theorems are related to flipping the + least significant bit in the numerical value of indices (of terms + in the lists). +*) - assert (k*2^m < 2^(m+n)). - destruct k. - + simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - + rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1. - rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm. - assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - + assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))). - intro l. intro M. rewrite tm_size_power2. - destruct k. simpl. assert (2^m <= 2^(m+n)). - apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r. - generalize H3. generalize M. apply Nat.lt_le_trans. - apply lt_split_bits. apply Nat.lt_0_succ. assumption. - assumption. - - rewrite nth_error_app1. rewrite nth_error_app1. - generalize H1. apply IHn. - apply L. assumption. apply L. assumption. - - + assert (J: 2 ^ (m + n) <= k * 2 ^ m). - rewrite Nat.pow_add_r. rewrite Nat.mul_comm. - apply Nat.mul_le_mono_r. assumption. - - rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2. - - assert (forall a b, option_map negb a = option_map negb b <-> a = b). - intros a b. destruct a. destruct b. destruct b0; destruct b; simpl. - split; intro; reflexivity. split; intro; inversion H2. - split; intro; inversion H2. split; intro; reflexivity. - split; intro; inversion H2. - destruct b. split; intro; inversion H2. split; intro; reflexivity. - - replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i). - replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j). - rewrite nth_error_map. rewrite nth_error_map. - - rewrite H2. apply IHn. - rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add. - rewrite Nat.pow_succ_r in H0. rewrite <- Nat.add_1_r in H0 at 1. - rewrite Nat.mul_add_distr_r in H0. simpl in H0. - rewrite Nat.add_0_r in H0. assumption. - apply Nat.le_0_l. assumption. - - rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. - rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity. - rewrite Nat.add_comm. reflexivity. assumption. - - rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. - rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity. - rewrite Nat.add_comm. reflexivity. assumption. - - rewrite tm_size_power2. - assert (k*2^m <= k*2^m + j). apply Nat.le_add_r. - generalize H2. generalize J. apply Nat.le_trans. - - rewrite tm_size_power2. - assert (k*2^m <= k*2^m + i). apply Nat.le_add_r. - generalize H2. generalize J. apply Nat.le_trans. -Qed. (* Note: a first version included the 0 < k hypothesis but in the very unorthodox case where k=0 it happens to be true anyway, and the hypothesis @@ -739,6 +762,13 @@ Proof. generalize P. generalize I. apply Nat.lt_le_trans. Qed. + +(** + The following lemmas and theorems are of general interest; they + come here because they use more specific previously defined + lemmas and theorems. +*) + Theorem tm_step_succ_double_index : forall (n k : nat), k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)). Proof. @@ -862,125 +892,13 @@ Proof. apply Nat.mul_comm. apply Nat.mul_comm. Qed. -(* TODO: remove -Lemma tm_step_pred : forall (n k m : nat), - S (2*k) * 2^m < 2^n -> - nth_error (tm_step n) (S (2*k) * 2^m) - = nth_error (tm_step n) (S (2*k) * 2^m - 1) - <-> odd m = true. -Proof. - intros n k m. - generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. - destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r. - intro H. apply Nat.neq_succ_0 in H. contradiction H. - rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r. - rewrite <- tm_step_double_index. intro H. split. intro I. - symmetry in I. apply tm_step_succ_double_index in I. contradiction I. - apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H. - rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2. - intro I. inversion I. - - intro n0. intro I. - destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I. - rewrite Nat.mul_eq_0 in I. destruct I. - apply Nat.neq_succ_0 in H. contradiction H. - apply Nat.pow_nonzero in H. contradiction H. easy. - rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc. - replace (S (2*k) * 2) with (2* (S (2*k))). - rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index. - - rewrite Nat.pow_succ_r' in I. - rewrite Nat.pow_succ_r' in I. - rewrite Nat.mul_assoc in I. - replace (S (2*k) * 2) with (2* (S (2*k))) in I. - rewrite <- Nat.mul_assoc in I. - rewrite <- Nat.mul_lt_mono_pos_l in I. - assert (J := I). apply IHm in J. - - assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - - assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m). - replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2. - apply Nat.lt_succ_diag_r. - rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn. - reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos. - apply Nat.lt_0_succ. assumption. - - assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))). - rewrite tm_size_power2. - rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r. - rewrite Nat.sub_add. rewrite Nat.pow_succ_r'. - rewrite <- Nat.mul_le_mono_pos_l. - apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2. - apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2. - apply Nat.mul_pos_pos. apply Nat.lt_0_succ. - assumption. - - assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0). - generalize I. generalize L. apply Nat.lt_trans. - - assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1) - <> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))). - apply tm_step_succ_double_index. assumption. - - replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H. - rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m). - - split. intro K. rewrite <- K in H. - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)). - destruct J. replace (Some b) with (Some b0) in H. contradiction H. - reflexivity. symmetry. apply H1. reflexivity. - destruct J. replace (Some b) with (None : option bool) in H. - contradiction H. reflexivity. symmetry. apply H1. reflexivity. - destruct J. replace (None : option bool) with (Some b) in H. - contradiction H. reflexivity. symmetry. apply H1. reflexivity. - contradiction H. reflexivity. - - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)); - intro K; simpl in K; inversion K. - - rewrite nth_error_nth' with (d := false) in J. - rewrite nth_error_nth' with (d := false) in J. - rewrite nth_error_nth' with (d := false) in H. - rewrite nth_error_nth' with (d := false) in H. - rewrite nth_error_nth' with (d := false). - rewrite nth_error_nth' with (d := false). - destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false); - destruct (nth (S (2 * k) * 2 ^ m - 1) (tm_step n0) false); - destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (tm_step (S n0)) false). - simpl; split; reflexivity. - destruct J. rewrite H0 in H. contradiction H. reflexivity. - reflexivity. - simpl; split; reflexivity. contradiction H. reflexivity. - contradiction H. reflexivity. - simpl; split; reflexivity. - destruct J. rewrite H0 in H. contradiction H. reflexivity. - reflexivity. - simpl; split; reflexivity. - - assumption. rewrite tm_size_power2. assumption. assumption. - rewrite tm_size_power2. assumption. - rewrite tm_size_power2. assumption. - rewrite tm_size_power2. assumption. - - rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r. - rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity. - rewrite <- Nat.mul_1_r at 1. - apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2. - apply Nat.le_succ_l. apply Nat.mul_pos_pos. - apply Nat.lt_0_succ. assumption. apply Nat.lt_0_2. - - apply Nat.mul_comm. apply Nat.mul_comm. -Qed. - *) - -(* - From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022 - TODO Search "count_occ" - *) +(** + The following lemmas and theorems are related to the sequence being + cubefree. Only the final theorem is of general interest; all other + lemmas are defined for the very specific purpose of being used in the + final proof. +*) Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat), tm_step n = hd ++ tl -> even (length hd) = true -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false. @@ -1447,6 +1365,3 @@ Proof. Qed. - - -