208 lines
8.2 KiB
Coq
208 lines
8.2 KiB
Coq
(** * 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 Arith.
|
|
Require Import Lia.
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
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.
|
|
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 (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 (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 (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 (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.
|
|
|
|
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.
|
|
|
|
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 Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
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
|
|
-> 0 < k
|
|
-> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
|
|
Proof.
|
|
intros m n k hd tl. intros H I J L.
|
|
|
|
assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
|
|
destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H.
|
|
rewrite <- H in I. rewrite tm_size_power2 in I.
|
|
|
|
assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0.
|
|
apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0.
|
|
rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0.
|
|
rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0.
|
|
rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0.
|
|
rewrite H0 in L. inversion L. easy.
|
|
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy.
|
|
replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I.
|
|
rewrite Nat.mul_cancel_r in I.
|
|
|
|
assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0.
|
|
apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0.
|
|
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
|
|
apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1.
|
|
rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1.
|
|
inversion H1. apply Nat.pow_nonzero. easy. lia.
|
|
|
|
generalize K. generalize J. generalize I. generalize H.
|
|
apply tm_step_palindrome_power2_inverse.
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
Lemma xxx :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ a ++ tl
|
|
-> a = rev a
|
|
-> 0 < length a
|
|
-> length a <= 4
|
|
\/ (exists m, length a = 2 ^ m /\
|
|
length (hd ++ a) mod 2 ^ pred (Nat.double (Nat.div2 (S m))) = 0)
|
|
\/ length a = 3 * 2^(pred (Nat.log2 (length a))).
|
|
Proof.
|
|
intros n hd a tl. intros H I J.
|
|
destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
|
rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
|
|
rewrite app_length in H0. rewrite Nat.add_comm in H0.
|
|
destruct a. inversion J. rewrite <- Nat.add_assoc in H0.
|
|
rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
|
|
apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
|
|
|
|
assert (exists k j, length a = S (Nat.double k) * 2^j).
|
|
apply trailing_zeros; assumption. destruct H0. destruct H0.
|
|
assert (x = 0 \/ x = 1). generalize H0. generalize H.
|
|
apply tm_step_square_size.
|
|
|
|
rewrite I in H at 2.
|
|
|
|
destruct H1; rewrite H1 in H0.
|
|
- rewrite Nat.mul_1_l in H0.
|
|
assert (length a <= 4 \/ 4 < length a). apply Nat.le_gt_cases.
|
|
destruct H2. left. assumption.
|
|
assert (2 < x0). destruct x0. rewrite H0 in H2. inversion H2.
|
|
inversion H4. destruct x0. rewrite H0 in H2. inversion H2.
|
|
inversion H4. inversion H6. destruct x0. rewrite H0 in H2.
|
|
inversion H2. inversion H4. inversion H6. inversion H8. inversion H10.
|
|
lia.
|
|
assert (length (hd ++ a) mod 2^(pred (Nat.double (Nat.div2 (S x0)))) = 0).
|
|
generalize H3. generalize H0. generalize H.
|
|
apply tm_step_palindrome_power2.
|
|
right. left. exists x0. split; assumption.
|
|
- right. right. rewrite H0. rewrite Nat.mul_cancel_l.
|
|
rewrite Nat.log2_mul_pow2. rewrite Nat.add_1_r.
|
|
rewrite Nat.pred_succ. reflexivity. lia. lia. lia.
|
|
Qed.
|