From 210b3b8b7910392b34b0b166fd354b8266556d19 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 8 Feb 2023 12:31:48 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 12 +++ src/thue_morse3.v | 23 +++++ src/thue_morse4.v | 235 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 270 insertions(+) create mode 100644 src/thue_morse4.v diff --git a/src/thue_morse.v b/src/thue_morse.v index 58e58ad..ade2a53 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -625,6 +625,18 @@ Proof. apply Nat.add_sub_assoc. rewrite Nat.sub_diag. apply Nat.add_0_r. Qed. +Lemma tm_step_stable2 : forall (n m : nat), + m <= n -> exists (tl : list bool), tm_step n = (tm_step m) ++ tl. +Proof. + intro n. induction n; intro m; intro H. + - apply Nat.le_0_r in H. rewrite H. exists nil. reflexivity. + - apply Nat.lt_eq_cases in H. destruct H as [ H| H]. + + rewrite Nat.lt_succ_r in H. rewrite tm_build. + apply IHn in H. destruct H. rewrite H. rewrite <- app_assoc. + exists (x ++ map negb (tm_step m ++ x)). reflexivity. + + rewrite H. exists nil. apply app_nil_end. +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 diff --git a/src/thue_morse3.v b/src/thue_morse3.v index b28dc9c..f322b24 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -2709,6 +2709,29 @@ Proof. Qed. +(* +Theorem tm_step_palindrome_power2_reciprocal : + forall (m n k : nat) (hd tl : list bool), + tm_step n = hd ++ tl + -> length hd = S (Nat.double k) * 2^m + -> odd m = true + -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl). +Proof. + intros m n. + assert (A: odd m = true + -> (forall k hd tl, tm_step n = hd ++ tl + ->length hd = S (Nat.double k) * 2^m + -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl)) + -> (forall k hd tl, tm_step (S n) = hd ++ tl + -> length hd = S (Nat.double k) * 2^m + -> skipn ((length hd) - 2^m) hd = rev (firstn (2^m) tl))). + intros H I. + intros k hd tl. intros J K. + + rewrite tm_build in J. + *) + + (* Lemma tm_step_proper_palindrome_center : forall (m n k : nat) (hd a tl : list bool), diff --git a/src/thue_morse4.v b/src/thue_morse4.v new file mode 100644 index 0000000..98ec39e --- /dev/null +++ b/src/thue_morse4.v @@ -0,0 +1,235 @@ +(** * The Thue-Morse sequence (part 4) + + TODO + +*) + +Require Import thue_morse. +Require Import thue_morse2. +Require Import thue_morse3. + +Require Import Coq.Lists.List. +Require Import PeanoNat. +Require Import Nat. +Require Import Bool. + +Require Import Lia. +Require Import Arith. + +Import ListNotations. + + +Lemma tm_step_repeating_patterns2 : + forall (n m : nat) (hd pat tl : list bool), + tm_step n = hd ++ pat ++ tl + -> length pat = 2^m + -> length hd mod (2^m) = 0 + -> pat = tm_step m \/ pat = map negb (tm_step m). +Proof. + intro n. + induction n; intros m hd pat tl; intros H I J. + - left. assert (K: length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in K at 2. rewrite app_length in K. rewrite app_length in K. + destruct hd; destruct tl. + + simpl in H. rewrite app_nil_r in H. rewrite <- H in I. + destruct m. rewrite <- H. reflexivity. + replace (length [false]) with (2^0) in I. apply Nat.pow_inj_r in I. + inversion I. apply Nat.lt_1_2. reflexivity. + + simpl in K. rewrite Nat.add_succ_r in K. inversion K. + symmetry in H1. apply Nat.eq_add_0 in H1. destruct H1. + rewrite H0 in I. symmetry in I. apply Nat.pow_nonzero in I. + contradiction. easy. + + simpl in K. inversion K. + symmetry in H1. apply Nat.eq_add_0 in H1. destruct H1. + rewrite Nat.add_0_r in H1. rewrite H1 in I. + symmetry in I. apply Nat.pow_nonzero in I. + contradiction. easy. + + simpl in K. rewrite Nat.add_succ_r in K. inversion K. + symmetry in H1. apply Nat.eq_add_0 in H1. destruct H1. + inversion H1. + - assert (H' := H). rewrite tm_build in H. + assert (K: length (hd ++ pat) <= 2^n \/ 2^n < length (hd ++ pat)). + apply Nat.le_gt_cases. destruct K as [K | K]. + + assert (tm_step n = hd ++ pat ++ firstn (2^n - length (hd ++ pat)) tl). + replace tl with (firstn (2^n - length (hd ++ pat)) tl + ++ skipn (2^n - length (hd ++ pat)) tl) in H. + rewrite app_assoc in H. rewrite app_assoc in H. + apply app_eq_length_head in H. rewrite app_assoc. assumption. + rewrite app_length. rewrite firstn_length_le. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite tm_size_power2. reflexivity. + apply Nat.le_refl. assumption. + rewrite Nat.add_le_mono_r with (p := length (hd ++ pat)). + rewrite Nat.sub_add. rewrite Nat.add_comm. rewrite <- app_length. + rewrite <- app_assoc. rewrite <- H'. rewrite tm_size_power2. + apply Nat.pow_le_mono_r. easy. apply Nat.le_succ_diag_r. assumption. + apply firstn_skipn. + generalize J. generalize I. generalize H0. apply IHn. + + assert (L: forall l1 l2, map negb l1 = l2 -> l1 = map negb l2). + intro l1. induction l1; intros. rewrite <- H0. reflexivity. + simpl in H0. destruct l2; inversion H0. apply IHl1 in H3. + rewrite H0. rewrite <- H2. simpl. rewrite negb_involutive. + rewrite <- H3. reflexivity. + + assert (L': forall l1 l2, map negb l1 = map negb l2 -> l1 = l2). + intro l1. induction l1; intros. destruct l2. reflexivity. + inversion H0. destruct l2. inversion H0. inversion H0. + apply IHl1 in H3. rewrite H3. + destruct a; destruct b; try reflexivity || inversion H2. + + assert (L'': forall l, map negb (map negb l) = l). + intro l. induction l. reflexivity. simpl. rewrite IHl. + rewrite negb_involutive. reflexivity. + + assert (U: n < m \/ m <= n). apply Nat.lt_ge_cases. destruct U as [U | U]. + assert (V: length hd < 2^n \/ 2^n <= length hd). apply Nat.lt_ge_cases. + destruct V as [V | V]. rewrite <- Nat.div_exact in J. + assert (length hd / 2^ m = 0). apply Nat.div_small. + rewrite Nat.pow_lt_mono_r_iff with (a := 2) in U. + generalize U. generalize V. apply Nat.lt_trans. apply Nat.lt_1_2. + rewrite H0 in J. rewrite Nat.mul_0_r in J. + rewrite length_zero_iff_nil in J. rewrite J in H'. rewrite J in K. + assert (length (tm_step (S n)) = length (pat ++ tl)). + rewrite H'. reflexivity. rewrite tm_size_power2 in H1. + rewrite app_length in H1. rewrite I in H1. + rewrite <- Nat.le_succ_l in U. + rewrite Nat.pow_le_mono_r_iff with (a := 2) in U. + rewrite Nat.lt_eq_cases in U. destruct U. rewrite H1 in H2. + (* contradiction en H2 *) + assert (2^m <= 2^m + length tl). apply Nat.le_add_r. + apply Nat.le_ngt in H3. contradiction. + rewrite <- tm_build in H. rewrite app_nil_l in H'. + rewrite <- app_nil_r in H' at 1. + apply app_eq_length_head in H'. apply Nat.pow_inj_r in H2. + rewrite H2 in H'. left. rewrite H'. reflexivity. + apply Nat.lt_1_2. rewrite I. rewrite tm_size_power2. rewrite H2. + reflexivity. apply Nat.lt_1_2. apply Nat.pow_nonzero. easy. + + rewrite Nat.add_le_mono_r with (p := length pat) in V. + rewrite Nat.pow_lt_mono_r_iff with (a := 2) in U. + rewrite Nat.add_lt_mono_l with (p := 2^n) in U. + rewrite <- I in U. + assert (length (tm_step (S n)) < length (hd ++ pat)). + rewrite app_length. rewrite tm_size_power2. simpl. rewrite Nat.add_0_r. + generalize V. generalize U. apply Nat.lt_le_trans. + rewrite H' in H0. rewrite app_assoc in H0. rewrite app_length in H0. + rewrite <- Nat.add_0_r in H0. rewrite <- Nat.add_lt_mono_l in H0. + apply Nat.nlt_0_r in H0. contradiction. apply Nat.lt_1_2. + + assert ((2^n) mod (2^m) = 0). rewrite <- Nat.div_exact. + rewrite <- Nat.pow_sub_r. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. reflexivity. apply Nat.le_refl. + assumption. easy. assumption. apply Nat.pow_nonzero. easy. + + assert (K': 2^n <= length hd \/ length hd < 2^n). + apply Nat.le_gt_cases. destruct K' as [K'|K']. + rewrite <- firstn_skipn with (n := 2^n) (l := hd) in H. + rewrite <- app_assoc in H. + assert (tm_step n = firstn (2^n) hd). + apply app_eq_length_head + with (x1 := map negb (tm_step n)) + (y1 := skipn (2 ^ n) hd ++ pat ++ tl). assumption. + rewrite firstn_length_le. apply tm_size_power2. assumption. + rewrite H1 in H at 1. apply app_inv_head_iff in H. + + apply L in H. rewrite map_app in H. rewrite map_app in H. + assert (length (map negb pat) = 2^m). rewrite map_length. assumption. + assert (length (map negb (skipn (2^n) hd)) mod (2^m) = 0). + rewrite map_length. rewrite skipn_length. + + replace (length hd - 2^n) with (length hd - 2^n + (2^n mod 2^m)). + rewrite Nat.add_mod_idemp_r. rewrite Nat.sub_add. assumption. + assumption. apply Nat.pow_nonzero. easy. rewrite H0. + apply Nat.add_0_r. + + assert (forall l1 l2, + (map negb l1 = map negb l2 \/ map negb l1 = map negb (map negb l2)) + -> l1 = l2 \/ l1 = map negb l2). + intros. destruct H4. left. apply L'. assumption. apply L' in H4. + right. assumption. apply H4. rewrite L''. rewrite or_comm. + generalize H3. generalize H2. generalize H. apply IHn. + + (* cas impossible *) + rewrite <- Nat.div_exact in J. rewrite J in K'. + rewrite <- Nat.div_exact in H0. rewrite H0 in K'. + rewrite <- Nat.mul_lt_mono_pos_l in K'. + apply Nat.lt_le_pred in K'. + rewrite Nat.mul_le_mono_pos_l with (p := 2^m) in K'. + rewrite <- J in K'. + rewrite <- Nat.sub_1_r in K'. rewrite Nat.mul_sub_distr_l in K'. + rewrite Nat.mul_1_r in K'. + rewrite Nat.add_le_mono_r with (p := length pat) in K'. + rewrite <- app_length in K'. rewrite I in K'. + rewrite Nat.sub_add in K'. rewrite <- H0 in K'. + apply Nat.le_ngt in K'. apply K' in K. contradiction. + rewrite <- H0. apply Nat.pow_le_mono_r. easy. assumption. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + apply Nat.pow_nonzero. easy. + apply Nat.pow_nonzero. easy. +Qed. + + + + + + + + + + +Lemma tm_step_repeating_patterns2 : + forall (n m k : nat), k < 2^n + -> tm_step m = firstn (2^m) (skipn (k * 2^m) (tm_step (m + n))) + \/ tm_step m = map negb (firstn (2^m) (skipn (k * 2^m) (tm_step (m + n)))). +Proof. + intros n m k. intro H. + generalize dependent + + + + forall n m i j : nat, + i < 2 ^ m -> + j < 2 ^ m -> + forall k : nat, + 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) + + + + + + + +Lemma tm_step_mod_palindromic : + forall (n m k : nat) (hd a b tl : list bool), + tm_step n = hd ++ a ++ b ++ tl + -> length (hd ++ a) = (S (Nat.double k)) * (2^(S (Nat.double m))) + -> 0 < m + -> length a = 2^(S (Nat.double m)) + -> length a = length b + -> a = rev b. +Proof. + intros n m k hd a b tl. intros H I J K L. + destruct m. inversion J. + generalize dependent n. generalize dependent hd. + generalize dependent a. generalize dependent b. + generalize dependent tl. + induction k. + + + + 0 < k -> S (Nat.double k) < n -> + firstn (2^(S (Nat.double k))) (tm_step n) + = firstn (2^(S (Nat.double k))) (skipn (2^(S (Nat.double k))) (tm_step n)). +Proof. + + +tm_step_palindromic_full_even: + forall n : nat, even n = true -> tm_step n = rev (tm_step n) + + +5.10.3