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