coqbooks/src/thue_morse4.v

253 lines
9.9 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 (j n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
-> a = rev a.
Proof.
intro j. induction j; intros n hd a tl; intros H I.
- destruct I.
+ destruct a. inversion H0. destruct a. reflexivity. inversion H0.
+ destruct a. inversion H0. destruct a. inversion H0. destruct a.
inversion H0. destruct a.
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e. reflexivity.
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
apply tm_step_consecutive_identical' in H. inversion H.
rewrite <- app_assoc. reflexivity.
assert (b = b0). destruct b; destruct b0; destruct b1;
reflexivity || contradiction n0 || contradiction n1; reflexivity.
rewrite H1 in H.
replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
inversion H0.
- assert (even (length a) = true).
destruct I; rewrite H0; rewrite Nat.double_S;
rewrite Nat.pow_succ_r.
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
assert (0 < length a). destruct I; rewrite H1.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.mul_pos_pos. lia.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (even (length (hd ++ a)) = true). generalize H1. generalize H.
apply tm_step_square_pos.
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.