From 4ba41ee7ef78b945165e70cc311c765533d74765 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 8 Feb 2023 17:18:54 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 151 +++++++++++++++++++++++ src/thue_morse4.v | 298 +++++++++++++++------------------------------- 2 files changed, 244 insertions(+), 205 deletions(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index ade2a53..c9f29de 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -719,6 +719,157 @@ Proof. generalize H2. generalize J. apply Nat.le_trans. Qed. +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. + (** The following lemmas and theorems are related to flipping the most significant bit in the numerical value of indices (of terms diff --git a/src/thue_morse4.v b/src/thue_morse4.v index 98ec39e..9cb2c54 100644 --- a/src/thue_morse4.v +++ b/src/thue_morse4.v @@ -13,223 +13,111 @@ Require Import PeanoNat. Require Import Nat. Require Import Bool. -Require Import Lia. Require Import Arith. +Require Import Lia. 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). +Theorem tm_step_palindrome_power2_inverse : + 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 + -> tl <> nil + -> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl). 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. + intros m n k hd tl. intros H I J K. + assert (L: 2^m <= length hd). rewrite I. lia. + assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)). + rewrite H. reflexivity. rewrite tm_size_power2 in H0. + rewrite app_length in H0. (* rewrite I in H0. *) + assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H1. + apply Nat.pow_le_mono_r with (a := 2) in H1. + assert (2^n <= length hd). generalize L. generalize H1. apply Nat.le_trans. + rewrite H0 in H2. rewrite <- Nat.add_0_r in H2. + rewrite <- Nat.add_le_mono_l in H2. destruct tl. contradiction K. + reflexivity. simpl in H2. apply Nat.nle_succ_0 in H2. contradiction. + easy. assumption. - 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 (N: length (tm_step n) mod 2^m = 0). rewrite tm_size_power2. + apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite <- Nat.pow_sub_r. + rewrite <- Nat.pow_add_r. rewrite Nat.add_comm. rewrite Nat.sub_add. + reflexivity. apply Nat.lt_le_incl. assumption. easy. + apply Nat.lt_le_incl. assumption. - assert (L'': forall l, map negb (map negb l) = l). - intro l. induction l. reflexivity. simpl. rewrite IHl. - rewrite negb_involutive. reflexivity. + assert (O: length hd mod 2^m = 0). + apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite I. + rewrite Nat.div_mul. rewrite Nat.mul_comm. reflexivity. + apply Nat.pow_nonzero. easy. - 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 (P: length tl mod 2 ^ m = 0). + rewrite H in N. rewrite app_length in N. + rewrite <- Nat.add_mod_idemp_l in N. rewrite O in N. assumption. + apply Nat.pow_nonzero. easy. - 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 (Q: 2^m <= length tl). apply Nat.div_exact in P. rewrite P. + destruct (length tl / 2^m). rewrite Nat.mul_0_r in P. + apply length_zero_iff_nil in P. rewrite P in K. contradiction K. + reflexivity. + rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l. + apply Nat.le_succ_l. apply Nat.lt_0_succ. + 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. + replace hd + with (firstn (length hd - 2^m) hd ++ skipn (length hd - 2^m) hd) in H. + replace tl with (firstn (2^m) tl ++ skipn (2^m) tl) in H. + rewrite <- app_assoc in H. + replace ( + skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl ++ skipn (2 ^ m) tl ) + with ( + (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) ++ skipn (2 ^ m) tl ) + in H. + assert (length (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) = 2^(S m)). + rewrite app_length. rewrite skipn_length. rewrite firstn_length_le. + replace (length hd) with (length hd -2^m + 2^m) at 1. + rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. simpl. rewrite Nat.add_0_r. + reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption. + assumption. - 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. + assert (length (firstn (length hd - 2^m) hd) mod 2^(S m) = 0). + rewrite firstn_length_le. replace (2^m) with (2^m * 1). + rewrite I. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_l. + rewrite Nat.sub_succ. rewrite Nat.sub_0_r. rewrite Nat.double_twice. + rewrite Nat.mul_assoc. replace (2^m * 2) with (2^(S m)). + rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity. + apply Nat.pow_nonzero. easy. + rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity. + apply le_0_n. apply Nat.mul_1_r. apply Nat.le_sub_l. - 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 ( + skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m) + \/ + skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = map negb (tm_step (S m))). + generalize H1. generalize H0. generalize H. apply tm_step_repeating_patterns2. - 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. + apply tm_step_palindromic_full in J. + destruct H2; rewrite J in H2. + - assert (skipn (length hd - 2^m) hd = tm_step m). + apply app_eq_length_head in H2. assumption. + rewrite skipn_length. + replace (length hd) with (length hd -2^m + 2^m) at 1. + rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite tm_size_power2. + reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. + assert (firstn (2^m) tl = rev (tm_step m)). + rewrite H3 in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity. + rewrite H4. rewrite rev_involutive. reflexivity. + - assert (skipn (length hd - 2^m) hd = map negb (tm_step m)). + rewrite map_app in H2. apply app_eq_length_head in H2. assumption. + rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1. + rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. + rewrite map_length. rewrite tm_size_power2. + reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3. + assert (firstn (2^m) tl = map negb (rev (tm_step m))). + rewrite H3 in H2. rewrite map_app in H2. apply app_inv_head in H2. + rewrite <- H2. reflexivity. + rewrite H4. rewrite map_rev. rewrite rev_involutive. reflexivity. + - rewrite <- app_assoc. reflexivity. + - rewrite firstn_skipn. reflexivity. + - rewrite firstn_skipn. reflexivity. 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