(** * 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