(*
https://oeis.org/A010060
https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
*)  

Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Bool.

Import ListNotations.

Fixpoint tm_morphism (l:list bool) : list bool :=
  match l with
  | nil => []
  | h :: t => h :: (negb h) :: (tm_morphism t)
  end.

Fixpoint tm_step (n: nat) : list bool :=
  match n with
  | 0 => false :: nil
  | S n' => tm_morphism (tm_step n')
  end.

(* ad hoc more or less general lemmas *)
Lemma negb_double_map : forall (l : list bool),
  map negb (map negb l) = l.
Proof.
  intro l.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. replace (negb (negb a)) with (a).
    reflexivity. rewrite negb_involutive. reflexivity.
Qed.

Lemma lt_split_bits : forall n m k j,
  0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
Proof.
  intros n m k j. intros H I J.

  assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
  apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.

  assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.

  assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
  rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
  apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
  apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
  apply Nat.mul_le_mono_r with (p := 2^m) in H0.
  rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
  rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.

  rewrite Nat.add_le_mono_r with (p := j) in H0.
  assert (2^n - 2^m + j < 2^n).
  rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
  rewrite Nat.add_lt_mono_r with (p := 2^m).
  rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
  rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.

  apply Nat.lt_le_incl. assumption.
  generalize H1. generalize H0. apply Nat.le_lt_trans.
  apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
  apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
  rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
Qed.


Lemma count_occ_bool_list : forall (a: list bool),
  length a = (count_occ bool_dec a true) + (count_occ bool_dec a false).
Proof.
  intro a.
  induction a.
  - reflexivity.
  - destruct a.
    + rewrite count_occ_cons_eq. rewrite count_occ_cons_neq.
      simpl. rewrite IHa. reflexivity. easy. reflexivity.
    + rewrite count_occ_cons_neq. rewrite count_occ_cons_eq.
      simpl. rewrite Nat.add_succ_r. rewrite IHa. reflexivity. reflexivity. easy.
Qed.


Lemma count_occ_bool_list2 : forall (a: list bool),
  count_occ bool_dec a false = count_occ bool_dec a true -> even (length a) = true.
Proof.
  intro a. intro H.
  rewrite count_occ_bool_list. rewrite H.
  replace (count_occ bool_dec a true) with (1 * (count_occ bool_dec a true)).
  rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
  replace (2 * count_occ bool_dec a true) with (0 + 2 * count_occ bool_dec a true).
  apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l.
Qed.


Lemma tm_morphism_concat : forall (l1 l2 : list bool),
  tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
  intros l1 l2.
  induction l1.
  - reflexivity.
  - simpl. rewrite IHl1. reflexivity.
Qed.

Lemma tm_morphism_rev : forall (l : list bool),
  rev (tm_morphism l) = tm_morphism (map negb (rev l)).
Proof.
  intro l. induction l.
  - reflexivity.
  - simpl. rewrite map_app.
    rewrite IHl. rewrite tm_morphism_concat.
    rewrite <- app_assoc. simpl.
    rewrite negb_involutive. reflexivity.
Qed.

Lemma tm_morphism_rev' : forall (l : list bool),
  rev (tm_morphism l) = map negb (tm_morphism (rev l)).
Proof.
  intro l. rewrite tm_morphism_rev. induction l.
  - reflexivity.
  - simpl. rewrite map_app. rewrite tm_morphism_concat. rewrite IHl.
    rewrite tm_morphism_concat. rewrite map_app. reflexivity.
Qed.

Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
  nth_error l k = nth_error (tm_morphism l) (2*k).
Proof.
  intro l.
  induction l.
  - intro k.
    simpl. replace (nth_error [] k) with (None : option bool).
    rewrite Nat.add_0_r. replace (nth_error [] (k+k)) with (None : option bool).
    reflexivity. symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
    symmetry. apply nth_error_None. simpl. apply Nat.le_0_l.
  - intro k. induction k.
    + rewrite Nat.mul_0_r. reflexivity.
    + simpl. rewrite Nat.add_0_r. rewrite Nat.add_succ_r. simpl.
      replace (k+k) with (2*k). apply IHl. simpl. rewrite Nat.add_0_r.
      reflexivity.
Qed.

Lemma tm_build_negb : forall (l : list bool),
  tm_morphism (map negb l) = map negb (tm_morphism l).
Proof.
  intro l.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.


Lemma tm_morphism_count_occ : forall (l : list bool),
  count_occ Bool.bool_dec (tm_morphism l) true
    = count_occ Bool.bool_dec (tm_morphism l) false.
Proof.
  intro l. induction l.
  - reflexivity.
  - destruct a.
    + simpl. apply eq_S. assumption.
    + simpl. apply eq_S. assumption.
Qed.

Lemma tm_morphism_app : forall (l1 l2 : list bool),
  tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
  intros l1 l2.
  induction l1.
  - reflexivity.
  - simpl. rewrite IHl1. reflexivity.
Qed.

Lemma tm_morphism_eq : forall (l1 l2 : list bool),
  l1 = l2 <-> tm_morphism l1 = tm_morphism l2.
Proof.
  intros l1 l2. split.
  - intro H. rewrite H. reflexivity.
  - generalize l2. induction l1.
    + intro l. intro H. simpl in H.
      induction l. reflexivity. simpl in H. inversion H.
    + simpl. intro l0. intro H.
      induction l0. simpl in H. inversion H.
      simpl in H. inversion H. apply IHl1 in H3. rewrite H3.
      reflexivity.
Qed.

Lemma tm_morphism_length : forall (l : list bool),
  length (tm_morphism l) = 2 * (length l).
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite Nat.add_0_r. rewrite IHl.
    rewrite Nat.add_succ_r.
    simpl. rewrite Nat.add_0_r. reflexivity.
Qed.

Lemma tm_morphism_app2 : forall (l hd tl : list bool),
  tm_morphism l = hd ++ tl
  -> even (length hd) = true
  -> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
Proof.
  intros l hd tl. intros H I.
  assert (J : l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
  symmetry. apply firstn_skipn.
  rewrite tm_morphism_eq in J.
  rewrite tm_morphism_app in J. rewrite H in J.
  apply app_eq_app in J.

  assert (H2: length (tm_morphism l) = length hd + length tl).
  rewrite H. apply app_length.

  assert (H3: length hd <= length (tm_morphism l)).
  rewrite H2. apply Nat.le_add_r.
  rewrite tm_morphism_length in H3.

  assert (H4: Nat.div2 (length hd) <= length l).
  rewrite Nat.mul_le_mono_pos_l with (p := 2).
  rewrite <- Nat.add_0_r at 1.
  replace (0) with (Nat.b2n (Nat.odd (length hd))) at 2.
  rewrite <- Nat.div2_odd. assumption.
  rewrite <- Nat.negb_even. rewrite I. reflexivity. apply Nat.lt_0_2.

  destruct J. destruct H0; destruct H0.

  assert (L: length hd = length hd). reflexivity.
  rewrite H0 in L at 2. rewrite app_length in L.
  rewrite tm_morphism_length in L.

  apply firstn_length_le in H4. rewrite H4 in L.
  replace (2 * Nat.div2 (length hd))
    with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
  rewrite <- Nat.div2_odd in L.
  rewrite <- Nat.add_0_r in L at 1.
  apply Nat.add_cancel_l in L. symmetry in L.
  apply length_zero_iff_nil in L.
  rewrite L in H0. rewrite <- app_nil_end in H0. assumption.
  rewrite <- Nat.negb_even. rewrite I. simpl.
  rewrite Nat.add_0_r. reflexivity.

  assert (L: length (tm_morphism (firstn (Nat.div2 (length hd)) l))
      = length (tm_morphism (firstn (Nat.div2 (length hd)) l))).
  reflexivity. rewrite H0 in L at 2. rewrite app_length in L.
  rewrite tm_morphism_length in L.

  apply firstn_length_le in H4. rewrite H4 in L.
  replace (2 * Nat.div2 (length hd))
    with (2 * Nat.div2 (length hd) + Nat.b2n (Nat.odd (length hd))) in L.
  rewrite <- Nat.div2_odd in L.
  rewrite <- Nat.add_0_r in L at 1.
  apply Nat.add_cancel_l in L. symmetry in L.
  apply length_zero_iff_nil in L.
  rewrite L in H0. rewrite <- app_nil_end in H0. symmetry. assumption.
  rewrite <- Nat.negb_even. rewrite I. simpl.
  rewrite Nat.add_0_r. reflexivity.
Qed.


Lemma tm_morphism_app3 : forall (l hd tl : list bool),
  tm_morphism l = hd ++ tl
  -> even (length hd) = true
  -> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
Proof.
  intros l hd tl. intros H I.
  assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) l)).
  generalize I. generalize H. apply tm_morphism_app2.
  assert (K: l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
  symmetry. apply firstn_skipn.
  assert (L: tm_morphism l = (tm_morphism (firstn (Nat.div2 (length hd)) l))
                          ++ (tm_morphism (skipn (Nat.div2 (length hd)) l))).
  rewrite K at 1. apply tm_morphism_app.
  rewrite H in L. rewrite <- J in L.
  rewrite app_inv_head_iff in L. assumption.
Qed.

(* Thue-Morse related lemmas and theorems *)
Lemma tm_step_lemma : forall n : nat,
  tm_morphism (tm_step n) = tm_step (S n).
Proof.
  intro n. reflexivity.
Qed.

Theorem tm_step_negb : forall (n : nat),
  map negb (tm_step (S n)) = rev (tm_morphism (rev (tm_step n))).
Proof.
  intro n.
  rewrite <- tm_step_lemma. symmetry.
  replace (tm_step n) with (rev (rev (tm_step n))).
  rewrite rev_involutive. rewrite tm_morphism_rev'. reflexivity.
  rewrite rev_involutive. reflexivity.
Qed.

Theorem tm_build : forall (n : nat),
  tm_step (S n) = tm_step n ++ map negb (tm_step n).
Proof.
  intro n.
  induction n.
  - reflexivity.
  - simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
    simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
    rewrite map_app. rewrite negb_double_map.
    reflexivity.
Qed.

Lemma tm_morphism_size : forall l : list bool,
  length (tm_morphism l) = 2 * (length l).
Proof.
  intro l. induction l.
  - reflexivity.
  - simpl. rewrite Nat.add_0_r. rewrite IHl.
    rewrite Nat.add_succ_r. replace (2) with (1+1). rewrite Nat.mul_add_distr_r.
    rewrite Nat.mul_1_l. reflexivity. reflexivity.
Qed.

Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
Proof.
  intro n.
  induction n.
  - reflexivity.
  - rewrite tm_build. rewrite app_length. rewrite map_length.
    replace (2^S n) with (2^n + 2^n). rewrite IHn. reflexivity.
    simpl. rewrite <- plus_n_O. reflexivity.
Qed.

Lemma tm_step_head_2 : forall (n : nat),
    tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
Proof.
  intro n.
  induction n.
  - reflexivity.
  - simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
    rewrite IHn. reflexivity. reflexivity.
Qed.

Lemma tm_step_end_2 : forall (n : nat),
  rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))).
Proof.
  intro n. induction n.
  - reflexivity.
  - simpl tm_step. rewrite tm_morphism_rev.
    replace (tm_morphism (tm_step n)) with (tm_step (S n)).
    rewrite IHn. simpl tm_morphism. simpl tl.
    rewrite Nat.even_succ.
    rewrite Nat.odd_succ.
    rewrite negb_involutive.
    reflexivity. reflexivity.
Qed.

Lemma tm_step_head_1 : forall (n : nat),
    tm_step n = false :: tl (tm_step n).
Proof.
  intro n. 
  destruct n.
  - reflexivity.
  - rewrite tm_step_head_2. reflexivity.
Qed.

Lemma tm_step_end_1 : forall (n : nat),
  rev (tm_step n) = odd n :: tl (rev (tm_step n)).
Proof.
  intro n.
  destruct n.
  - reflexivity.
  - rewrite tm_step_end_2. simpl.
    rewrite Nat.odd_succ.
    reflexivity.
Qed.

Theorem tm_step_double_index : forall (n k : nat),
  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
Proof.
  intros n k.
  destruct k.
  - rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
    rewrite tm_step_head_1. reflexivity.
  - rewrite <- tm_step_lemma.
    rewrite tm_morphism_double_index. reflexivity.
Qed.

Lemma tm_step_single_bit_index : forall (n : nat),
  nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
  intro n.
  rewrite tm_build.
  rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
  replace (true) with (negb false). apply map_nth_error.
  rewrite tm_step_head_1. reflexivity.
  reflexivity. rewrite tm_size_power2. easy.
Qed.

Lemma tm_step_repunit_index : forall (n : nat),
  nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
  intro n.
  assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2.
  rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.

  rewrite nth_error_nth' with (d := false).
  replace (tm_step n) with (rev (rev (tm_step n))).
  rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2.
  rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag.
  rewrite tm_step_end_1. reflexivity.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
  rewrite rev_length. assumption. apply rev_involutive. assumption.
Qed.

Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
  l = l1 ++ b :: l2 -> length l1 < length l.
Proof.
  intros l l1 l2 b. intro H. rewrite H.
  rewrite app_length. simpl. apply Nat.lt_add_pos_r.
  apply Nat.lt_0_succ.
Qed.

Lemma tm_step_next_range :
  forall (n k : nat) (b : bool),
  nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
Proof.
  intros n k b. intro H. assert (I := H).
  apply nth_error_split in H. destruct H. destruct H. inversion H.
  rewrite tm_build. rewrite nth_error_app1. apply I.
  apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
Qed.

Lemma tm_step_add_range : forall (n m k : nat),
  k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
Proof.
  intros n m k. intro H.
  induction m.
  - rewrite Nat.add_comm. reflexivity.
  - rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
    assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
    generalize H. apply nth_error_nth'.
    rewrite H0 in IHm. symmetry in IHm.
    rewrite H0. symmetry. generalize IHm.
    apply tm_step_next_range.
Qed.

Theorem tm_step_stable : forall (n m k : nat),
  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Proof.
  intros n m k. intros.
  assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
  apply Nat.max_spec. destruct I.
  - destruct H1. replace (m) with (n + (m-n)). apply tm_step_add_range. apply H.
    apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1.
    apply Nat.add_sub_assoc. rewrite Nat.add_comm.
    assert (n <= n). apply le_n. symmetry.
    replace (m) with (m + (n-n)) at 1. generalize H3.
    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
    reflexivity.
  - destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
    apply H0. replace (n) with (m + n - m) at 2. generalize H1.
    apply Nat.add_sub_assoc. rewrite Nat.add_comm.
    assert (m <= m). apply le_n. symmetry.
    replace (n) with (n + (m-m)) at 1. generalize H3.
    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
    reflexivity.
Qed.

Lemma tm_step_next_range2 :
  forall (n k : nat),
  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Proof.
  intros n k. intro H.
  rewrite tm_build.
  rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
  assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
  generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
  rewrite H0.
  assert (nth_error (map negb (tm_step n)) k
    = Some (negb (nth k (tm_step n) false))).
  generalize H0. apply map_nth_error. rewrite H1.
  destruct (nth k (tm_step n) false). easy. easy.
  rewrite tm_size_power2. apply Nat.le_add_l.
Qed.

Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
  k < 2^n -> m < 2^n ->
    nth_error (tm_step n) k = nth_error (tm_step n) m
    <->
    nth_error (tm_step (S n)) (k + 2^n)
      = nth_error (tm_step (S n)) (m + 2^n).
Proof.
  intros n k m. intro H. intro I.
  (* Part 1: preamble *)

  assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
  generalize H. apply tm_step_next_range2.
  assert (nth_error (tm_step n) m <> nth_error (tm_step (S n)) (m + 2^n)).
  generalize I. apply tm_step_next_range2.

  assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
  generalize H. apply Nat.add_lt_mono_r.
  assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
  generalize I. apply Nat.add_lt_mono_r.

  (* Part 2: main proof *)
  assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
  generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
  assert (nth_error (tm_step n) m = Some (nth m (tm_step n) false)).
  generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
  assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
    Some (nth (k + 2^n) (tm_step (S n)) false)).
  generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
  apply nth_error_nth'.
  assert (nth_error (tm_step (S n)) (m + 2 ^ n) =
    Some (nth (m + 2^n) (tm_step (S n)) false)).
  generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
  apply nth_error_nth'.
  rewrite H2. rewrite H3. rewrite H4. rewrite H5.

  (* Part 3: handling 16 different cases *)
  destruct (nth k (tm_step n) false).
  destruct (nth m (tm_step n) false).
  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  easy.
  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
  easy.
  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
  easy.
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  easy.
  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
  destruct (nth m (tm_step n) false).
  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
  easy.
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  easy.
  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  easy.
  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
  easy.
Qed.

Lemma tm_step_add_range2_flip_two : forall (n m j k : nat),
  k < 2^n -> m < 2^n ->
    nth_error (tm_step n) k = nth_error (tm_step n) m
    <->
    nth_error (tm_step (S n+j)) (k + 2^(n+j))
      = nth_error (tm_step (S n+j)) (m + 2^(n+j)).
Proof.
  intros n m j k. intros H I.
  assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
  generalize H. apply Nat.add_lt_mono_r.
  assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
  generalize I. apply Nat.add_lt_mono_r.

  split.
  - induction j.
    + intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
    rewrite <- tm_step_next_range2_flip_two. apply L. apply H. apply I.
    + intros L.

      rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.

      assert (2^n < 2^(S n + j)).
      assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
      generalize H0. apply Nat.lt_lt_add_r.
      generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
      assert (k < 2^(S n + j)).
      generalize H0. generalize H. apply Nat.lt_trans.
      assert (m < 2^(S n + j)).
      generalize H0. generalize I. apply Nat.lt_trans.

      rewrite <- tm_step_next_range2_flip_two.

      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
      generalize H1. generalize H. apply tm_step_stable.
      assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
      generalize H2. generalize I. apply tm_step_stable.
      rewrite <- H3. rewrite <- H4. apply L.

      apply H1. apply H2.
  - induction j.
    + intro L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
      apply tm_step_next_range2_flip_two. apply H. apply I. apply L.
    + intro L.
      rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.

      assert (2^n < 2^(S n + j)).
      assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
      generalize H0. apply Nat.lt_lt_add_r.
      generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
      assert (k < 2^(S n + j)).
      generalize H0. generalize H. apply Nat.lt_trans.
      assert (m < 2^(S n + j)).
      generalize H0. generalize I. apply Nat.lt_trans.

      rewrite <- tm_step_next_range2_flip_two in L.

      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
      generalize H1. generalize H. apply tm_step_stable.
      assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
      generalize H2. generalize I. apply tm_step_stable.
      rewrite <- H3 in L. rewrite <- H4 in L. apply L.

      apply H1. apply H2.
Qed.

Lemma tm_step_repeating_patterns :
  forall (n m i j : nat),
  i < 2^m -> j < 2^m
  -> forall k, 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).
Proof.
  intros n m i j. intros H I.
  induction n.
  - rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro.
    rewrite H0. simpl. easy.
  - rewrite Nat.add_succ_r. intro k. intro.
    rewrite tm_build.
    assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases.
    destruct S.

    assert (k*2^m < 2^(m+n)).
    destruct k.
    + simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
    + rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
      rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
      assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
    + assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))).
      intro l. intro M. rewrite tm_size_power2.
      destruct k. simpl. assert (2^m <= 2^(m+n)). 
      apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
      generalize H3. generalize M. apply Nat.lt_le_trans.
      apply lt_split_bits. apply Nat.lt_0_succ. assumption.
      assumption.

      rewrite nth_error_app1. rewrite nth_error_app1.
      generalize H1. apply IHn.
      apply L. assumption. apply L. assumption.

    + assert (J: 2 ^ (m + n) <= k * 2 ^ m).  
      rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
      apply Nat.mul_le_mono_r. assumption.

      rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.

      assert (forall a b, option_map negb a = option_map negb b <-> a = b).
      intros a b. destruct a. destruct b. destruct b0; destruct b; simpl.
      split; intro; reflexivity. split; intro; inversion H2.
      split; intro; inversion H2. split; intro; reflexivity.
      split; intro; inversion H2.
      destruct b. split; intro; inversion H2. split; intro; reflexivity.

      replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i).
      replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).
      rewrite nth_error_map. rewrite nth_error_map.

      rewrite H2. apply IHn.
      rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
      rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0.
      rewrite Nat.mul_add_distr_r in H0. simpl in H0.
      rewrite Nat.add_0_r in H0. assumption. reflexivity.
      apply Nat.le_0_l. assumption.

      rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
      rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
      rewrite Nat.add_comm. reflexivity. assumption.

      rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
      rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
      rewrite Nat.add_comm. reflexivity. assumption.

      rewrite tm_size_power2.
      assert (k*2^m <= k*2^m + j). apply Nat.le_add_r.
      generalize H2. generalize J. apply Nat.le_trans.

      rewrite tm_size_power2.
      assert (k*2^m <= k*2^m + i). apply Nat.le_add_r.
      generalize H2. generalize J. apply Nat.le_trans.
Qed.

(* Note: a first version included the  0 < k  hypothesis but in the very
   unorthodox case where k=0 it happens to be true anyway, and the hypothesis
   was removed in order to make the theorem more general *)
Theorem tm_step_flip_low_bit :
  forall (n m k j : nat),
  j < m -> k * 2^m < 2^n
  -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
  intros n m k j. intros H I.

  assert (L: nth_error (tm_step m) 0 = Some false).
  rewrite tm_step_head_1. reflexivity.

  assert (M: 2^j < 2^m).
  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.

  assert (N: nth_error (tm_step m) (2^j) = Some true).
  replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
  rewrite tm_step_single_bit_index. reflexivity.
  apply tm_step_stable.
  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
  assumption.

  assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G as [G1|G2].

  (* k = 0 *)
  rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
  rewrite tm_step_head_1 at 1.
  assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
  destruct S as [S1|S2]. rewrite Nat.lt_succ_r in S1.
  apply Nat.pow_le_mono_r with (a := 2) in S1.
  rewrite <- tm_size_power2 in S1. rewrite <- nth_error_None in S1.
  rewrite S1. easy. easy.
  rewrite Nat.le_succ_l in S2. apply Nat.pow_lt_mono_r with (a := 2) in S2.
  rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
  apply Nat.lt_1_2.

  (* k < 0 *)
  assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
  assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.

  assert ( nth_error (tm_step m) 0
         = nth_error (tm_step m) (2^j)
       <-> nth_error (tm_step (m+n)) (k * 2^m + 0)
         = nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ).
  apply tm_step_repeating_patterns.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.

  assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg.
  apply Nat.le_0_1. rewrite Nat.le_succ_l.
  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
  apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0.
  rewrite Nat.mul_comm in H0.
  generalize I. generalize H0. apply Nat.le_lt_trans.
  rewrite Nat.add_0_r in H0.

  replace (nth_error (tm_step (m + n)) (k * 2 ^ m))
    with (nth_error (tm_step n) (k * 2 ^ m)) in H0.
  replace (nth_error (tm_step (m + n)) (k * 2 ^ m + 2^j))
    with (nth_error (tm_step n) (k * 2 ^ m + 2^j)) in H0.
  rewrite L in H0. rewrite N in H0.

  destruct (nth_error (tm_step n) (k * 2 ^ m)).
  destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
  destruct b; destruct b0; destruct H0.
  assert (Some true = Some true). reflexivity.
  apply H1 in H2. rewrite <- H2 at 1. easy. easy. easy.
  assert (Some false = Some false). reflexivity.
  apply H1 in H2. rewrite H2 at 1. easy. easy.
  rewrite nth_error_nth' with (d := false). easy.
  rewrite tm_size_power2. assumption.

  apply tm_step_stable. assumption.
  generalize P. generalize O. apply Nat.lt_le_trans.

  apply tm_step_stable. assumption.
  generalize P. generalize I. apply Nat.lt_le_trans.
Qed.

Theorem tm_step_succ_double_index : forall (n k : nat),
  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
Proof.
  intros n k. intro H. rewrite tm_step_double_index.
  rewrite Nat.mul_comm. replace (2) with (2^1).
  replace (S (k*2^1)) with (k*2^1 + 2^0).
  apply tm_step_flip_low_bit. apply Nat.lt_0_1.
  simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k).
  apply Nat.add_lt_mono; assumption.
  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
  simpl. rewrite Nat.add_1_r. reflexivity. reflexivity.
Qed.


Lemma tm_step_pred : forall (n k m : nat),
    S (2*k) * 2^m < 2^n ->
    nth_error (tm_step n) (S (2*k) * 2^m)
     = nth_error (tm_step n) (S (2*k) * 2^m - 1)
     <-> odd m = true.
Proof.
  intros n k m.

  generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
  destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
  intro H. apply Nat.neq_succ_0 in H. contradiction H.
  rewrite Nat.odd_0. rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
  rewrite <- tm_step_double_index. intro H. split. intro I.
  symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
  apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
  rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
  intro I. apply diff_false_true in I. contradiction I.

  intro n0. intro I.
  destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
  rewrite Nat.mul_eq_0 in I. destruct I.
  apply Nat.neq_succ_0 in H. contradiction H.
  apply Nat.pow_nonzero in H. contradiction H. easy.
  rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc.
  replace (S (2*k) * 2) with (2* (S (2*k))).
  rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.

  rewrite Nat.pow_succ_r' in I.
  rewrite Nat.pow_succ_r' in I.
  rewrite Nat.mul_assoc in I.
  replace (S (2*k) * 2) with (2* (S (2*k))) in I.
  rewrite <- Nat.mul_assoc in I.
  rewrite <- Nat.mul_lt_mono_pos_l in I.
  assert (J := I). apply IHm in J.

  assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.

  assert (L: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
  replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
  apply Nat.lt_succ_diag_r.
  rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn.
  reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos.
  apply Nat.lt_0_succ. assumption.

  assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))).
  rewrite tm_size_power2.
  rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r.
  rewrite Nat.sub_add. rewrite Nat.pow_succ_r'.
  rewrite <- Nat.mul_le_mono_pos_l.
  apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2.
  apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
  apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
  assumption.

  assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0).
  generalize I. generalize L. apply Nat.lt_trans.

  assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
    <> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
  apply tm_step_succ_double_index. assumption.

  replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
  rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).

  split. intro K. rewrite <- K in H.
  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
  destruct J. replace (Some b) with (Some b0) in H. contradiction H.
  reflexivity. symmetry. apply H1. reflexivity.
  destruct J. replace (Some b) with (None : option bool) in H.
  contradiction H. reflexivity. symmetry. apply H1. reflexivity.
  destruct J. replace (None : option bool) with (Some b) in H.
  contradiction H. reflexivity. symmetry. apply H1. reflexivity.
  contradiction H. reflexivity.

  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
  destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
  intro K. simpl in K. apply diff_false_true in K. contradiction K.
  intro K. simpl in K. apply diff_false_true in K. contradiction K.
  intro K. simpl in K. apply diff_false_true in K. contradiction K.
  intro K. simpl in K. apply diff_false_true in K. contradiction K.

  rewrite nth_error_nth' with (d := false) in J.
  rewrite nth_error_nth' with (d := false) in J.
  rewrite nth_error_nth' with (d := false) in H.
  rewrite nth_error_nth' with (d := false) in H.
  rewrite nth_error_nth' with (d := false).
  rewrite nth_error_nth' with (d := false).
  destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false);
  destruct (nth (S (2 * k) * 2 ^ m - 1) (tm_step n0) false);
  destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (tm_step (S n0)) false).
  simpl; split; reflexivity.
  destruct J. rewrite H0 in H. contradiction H. reflexivity.
  reflexivity.
  simpl; split; reflexivity. contradiction H. reflexivity.
  contradiction H. reflexivity.
  simpl; split; reflexivity.
  destruct J. rewrite H0 in H. contradiction H. reflexivity.
  reflexivity.
  simpl; split; reflexivity.

  assumption. rewrite tm_size_power2. assumption. assumption.
  rewrite tm_size_power2. assumption.
  rewrite tm_size_power2. assumption.
  rewrite tm_size_power2. assumption.

  rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
  rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity.
  rewrite <- Nat.mul_1_r at 1.
  apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2.
  apply Nat.le_succ_l. apply Nat.mul_pos_pos.
  apply Nat.lt_0_succ. assumption. apply Nat.lt_0_2.

  apply Nat.mul_comm. apply Nat.mul_comm.
Qed.


(*
  From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022 
   TODO Search "count_occ"
 *)
Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
  tm_step n = hd ++ tl -> even (length hd) = true
  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
Proof.
  intros hd tl n. intros H I.
  destruct n.
  - assert (J: hd = nil). destruct hd. reflexivity.
    simpl in H. inversion H.
    symmetry in H2. apply app_eq_nil in H2.
    destruct H2. rewrite H0 in I. simpl in I. inversion I.
    rewrite J. reflexivity.
  - rewrite <- tm_step_lemma in H.
    assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
    generalize I. generalize H. apply tm_morphism_app2.
    rewrite J. apply tm_morphism_count_occ.
Qed.


Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
Proof.
  intros n a hd tl. intro H.
  assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd.
  assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd.

  destruct H1.
  - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
  - destruct H0.
    assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
    assert (Nat.even (length hd) = true).
    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
    generalize H2. generalize H. apply tm_step_count_occ.

    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I.
    assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false).
    assert (even (length (hd++a++a)) = true).
    rewrite app_length. rewrite Nat.even_add_even.
    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.

    rewrite app_length. replace (length a) with (1*(length a)).
    rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
    rewrite <- Nat.add_0_l. apply Nat.EvenT_Even.
    apply Nat.even_EvenT.
    rewrite Nat.even_add_mul_2. reflexivity.
    apply Nat.mul_1_l.
    generalize H3. generalize I. apply tm_step_count_occ.

    rewrite count_occ_app in H3. symmetry in H3.
    rewrite count_occ_app in H3. rewrite H2 in H3.
    rewrite Nat.add_cancel_l in H3.

    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.

    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
    assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
    assert (even (length (hd++a)) = true).
    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    generalize H2. generalize I. apply tm_step_count_occ.

    assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J.
    assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false).
    assert (even (length (hd++a++a++a)) = true).
    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
    rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length.
    apply Nat.Even_Even_add.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
    generalize H3. generalize J. apply tm_step_count_occ.

    replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3.
    rewrite count_occ_app in H3. symmetry in H3.
    rewrite count_occ_app in H3. rewrite H2 in H3.
    rewrite Nat.add_cancel_l in H3.

    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
    rewrite app_assoc_reverse. reflexivity.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity.
Qed.


Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a -> 0 < n.
Proof.
  intros n a hd tl. intros H I.
  destruct n.
  - assert (3 <= length (a ++ a ++ a)).
    rewrite app_length. rewrite app_length.
    rewrite <- Nat.le_succ_l in I.
    assert (2 <= length a + length a).
    generalize I. generalize I. apply Nat.add_le_mono.
    generalize H0. generalize I. apply Nat.add_le_mono.
    assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
    rewrite H in H1 at 2.
    assert (0 <= length hd). apply Nat.le_0_l.
    assert (0 + 3 <= length hd + length (a ++ a ++ a)).
    generalize H0. generalize H2. apply Nat.add_le_mono.
    simpl in H3. rewrite <- app_length in H3.
    assert (0 <= length tl). apply Nat.le_0_l.
    assert (3 + 0 <= length (hd ++ a ++ a ++ a) + length (tl)).
    generalize H4. generalize H3. apply Nat.add_le_mono.
    rewrite <- app_length in H5. rewrite Nat.add_0_r in H5.
    replace ((hd++a++a++a)++tl) with (hd++a++a++a++tl) in H5.
    rewrite <- H1 in H5. simpl in H5. apply le_S_n in H5.
    apply Nat.nle_succ_0 in H5. contradiction H5.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.
  - apply Nat.lt_0_succ.
Qed.


Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> even (length hd) = even (length tl).
Proof.
  intros n a hd tl. intros H J.
  assert (K : 0 < n). generalize J. generalize H. apply tm_step_cube2.
  destruct n.
  - apply Nat.lt_irrefl in K. contradiction K.
  - assert (Nat.Even (length (tm_step (S n)))).
    rewrite tm_size_power2. rewrite Nat.pow_succ_r'.
    apply Nat.Even_mul_l. apply Nat.EvenT_Even.
    apply Nat.EvenT_2. apply Nat.EvenT_0.
    rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
    rewrite Nat.add_shuffle3 in H0.
    assert (I := H). apply tm_step_cube1 in I.
    apply Nat.even_EvenT in I. apply Nat.EvenT_Even in I.
    assert (Nat.Even (length hd + length (a ++ a ++ tl))).
    generalize I. generalize H0. apply Nat.Even_add_Even_inv_r.
    rewrite app_length in H1. rewrite Nat.add_shuffle3 in H1.
    assert (Nat.Even (length hd + length (a ++ tl))).
    generalize I. generalize H1. apply Nat.Even_add_Even_inv_r.
    rewrite app_length in H2. rewrite Nat.add_shuffle3 in H2.
    assert (Nat.Even (length hd + length tl)).
    generalize I. generalize H2. apply Nat.Even_add_Even_inv_r.

    apply Nat.Even_EvenT in H3. apply Nat.EvenT_even in H3.
    rewrite Nat.even_add in H3.
    destruct (even (length hd)); destruct (even (length tl)).
    reflexivity. simpl in H3. inversion H3.
    simpl in H3. inversion H3. reflexivity.
Qed.


Lemma tm_step_cube4 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false
  -> 0 < length a
  -> hd_error a = hd_error tl.
Proof.
  intros n a hd tl. intros H I J.
  assert (even (length hd) = even (length tl)).
  generalize J. generalize H. apply tm_step_cube3.
  assert (even (length a) = true). generalize H. apply tm_step_cube1.
  rewrite I in H0.
  destruct a.
  - simpl in J. apply Nat.lt_irrefl in J. contradiction J.
  - destruct tl. simpl in H0. inversion H0.
    simpl. replace (b::a) with ((b::nil) ++ a) in H.
    replace (hd ++ ([b] ++ a) ++ ([b] ++ a) ++ ([b] ++ a) ++ (b0::tl))
    with ((hd ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b0::nil)) ++ tl) in H.

    assert (even (length (hd ++ (b::nil))) = true).
    rewrite last_length.
    rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite I. reflexivity.

    assert (count_occ Bool.bool_dec (hd ++ (b::nil)) true
        = count_occ Bool.bool_dec (hd ++ (b::nil)) false).
    generalize H2. generalize H. apply tm_step_count_occ.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)))) = true).
    rewrite app_length. rewrite Nat.even_add. rewrite H2.
    rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
    reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) true
            = count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) false).
    generalize H4. rewrite app_assoc in H. generalize H. apply tm_step_count_occ.

    assert (K := H5).
    rewrite count_occ_app in H5. symmetry in H5. rewrite count_occ_app in H5.
    rewrite H3 in H5. rewrite Nat.add_cancel_l in H5.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil))  ++ (a++ (b::nil)))) = true).
    rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
    rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
    reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) true
    = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) false).
    generalize H6.
    rewrite app_assoc in H. rewrite app_assoc in H.
    replace (((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b])
      with ((hd ++ [b]) ++ (a ++ [b]) ++ a ++ [b]) in H.
    generalize H. apply tm_step_count_occ.

    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.

    assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil))  ++ (a++ (b::nil)) ++ (a++ (b0::nil)))) = true).
    rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
    rewrite app_length. rewrite last_length.
    replace (length (b::a)) with (S (length a)) in H1. rewrite Nat.even_add. rewrite H1.
    rewrite last_length. rewrite H1. reflexivity. reflexivity.

    assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) true
    = count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) false).
    generalize H8.

    rewrite app_assoc in H. rewrite app_assoc in H. rewrite app_assoc in H.
    replace ((((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) ++ a ++ [b0])
    with ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) in H.
    generalize H. apply tm_step_count_occ.

    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.

    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H3 in H9. rewrite Nat.add_cancel_l in H9.
    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
    rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
    rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.

    destruct b; destruct b0.
    reflexivity.
    rewrite count_occ_app in H9. rewrite count_occ_app in H9.
    rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
    rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
    rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
    rewrite count_occ_app in H5. rewrite count_occ_app in H5.
    rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
    rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
    rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
    rewrite H5 in H9.
    rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
    rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
    rewrite Nat.add_cancel_l in H9. inversion H9.
    reflexivity. easy. easy. reflexivity.
    rewrite count_occ_app in H9. rewrite count_occ_app in H9.
    rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
    rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
    rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
    rewrite count_occ_app in H5. rewrite count_occ_app in H5.
    rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
    rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
    rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
    rewrite <- H5 in H9.
    rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
    rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
    rewrite Nat.add_cancel_l in H9. inversion H9.
    easy. reflexivity. reflexivity. easy.
    reflexivity.

    rewrite app_assoc_reverse. apply app_inv_head_iff.
    rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    rewrite app_assoc_reverse. rewrite app_assoc_reverse.
    apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse.
    apply app_inv_head_iff. apply app_inv_head_iff.
    rewrite app_assoc_reverse.
    reflexivity.

    reflexivity.
Qed.


Lemma tm_step_cube5 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
                         /\ length a = length b
                         /\ even (length hd2) = true.
Proof.
  intros n a hd tl. intros H I.
  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
  apply Nat.Even_or_Odd.
  destruct J.
  - exists hd. exists a. exists tl.
    split. assumption. split. reflexivity.
    apply Nat.Even_EvenT in H0.
    apply Nat.EvenT_even in H0. assumption.
  - apply Nat.Odd_OddT in H0.
    apply Nat.OddT_odd in H0.
    rewrite <- Nat.negb_even in H0. rewrite negb_true_iff in H0.
    destruct a.
    + simpl in I. apply Nat.lt_irrefl in I. contradiction I.
    + assert (Nat.even (length hd) = Nat.even (length tl)).
      generalize I. generalize H. apply tm_step_cube3.
      rewrite H0 in H1.
      destruct tl.
      * simpl in H1. inversion H1.
      * assert (hd_error (b::a) = hd_error (b0::tl)).
        generalize I. generalize H0. generalize H. apply tm_step_cube4.
        simpl in H2. inversion H2. rewrite <- H4 in H.
        exists (hd ++ (b::nil)). exists (a ++ (b::nil)). exists tl.
        split. rewrite H.
        rewrite app_assoc_reverse. apply app_inv_head_iff.
        replace (b::a) with ([b] ++ a).
        rewrite app_assoc_reverse. apply app_inv_head_iff.
        rewrite app_assoc_reverse. rewrite app_assoc_reverse.
        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
        rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
        rewrite app_assoc_reverse. reflexivity.
        reflexivity.
        split. rewrite last_length. reflexivity.
        rewrite last_length.
        rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite H0.
        reflexivity.
Qed.


Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool),
  tm_step n = hd ++ a ++ a ++ a ++ tl
  -> 0 < length a
  -> exists (hd2 b tl2 : list bool), tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2
     /\ 0 < length b.
Proof.
  intros n a hd tl. intros H I.
  assert(J: exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
                         /\ length a = length b
                         /\ even (length hd2) = true).
  generalize I. generalize H. apply tm_step_cube5.
  destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2].
  destruct J2 as [J3 J4]. destruct J4 as [J5 J6].
  assert (J: even (length b) = true). generalize J3. apply tm_step_cube1.
  
  assert (K: 0 < n). generalize I. generalize H. apply tm_step_cube2.
  destruct n.
  - apply Nat.lt_irrefl in K. contradiction K.
  - rewrite <- tm_step_lemma in J3.
    assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))).
    generalize J6. generalize J3. apply tm_morphism_app2.
    assert (M: b ++ b ++ b ++ tl2 = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))).
    generalize J6. generalize J3. apply tm_morphism_app3.
    assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))).
    generalize J. symmetry in M. generalize M. apply tm_morphism_app2.
    assert (even (length (b++b++b)) = true).
    rewrite app_length. rewrite app_length.
    rewrite Nat.even_add_even. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT.
    rewrite Nat.even_add_even. assumption.
    apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
    assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) (skipn (Nat.div2 (length hd2)) (tm_step n)))).
    generalize H0. symmetry in M. generalize M.
    replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3.
    rewrite app_assoc_reverse. apply app_inv_head_iff.
    rewrite app_assoc_reverse. reflexivity.
    assert (hd2 ++ b ++ b ++ b ++ tl2
      = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n)))
      ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
      ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))))).
   rewrite <- L. rewrite <- N. rewrite <- O. reflexivity.
   rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
   rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
   rewrite <- J3 in H1.

   rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1.
   exists (firstn (Nat.div2 (length hd2)) (tm_step n)).
   exists (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))).
   exists (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))).
   split. assumption.

   assert (2 <= length b).
   destruct b. simpl in J5. rewrite J5 in I. apply Nat.lt_irrefl in I. contradiction I.
   destruct b0. simpl in J. inversion J.
   simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
   assert (length (b++b++b++tl2) = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
   rewrite M. apply tm_morphism_size.

   assert (2 <= length (b++b++b++tl2)).
   rewrite app_length. rewrite <- Nat.add_0_r at 1.
   apply Nat.add_le_mono. assumption. apply Nat.le_0_l.
   rewrite H3 in H4. rewrite <- Nat.mul_1_r in H4 at 1.
   rewrite <- Nat.mul_le_mono_pos_l in H4.
    
   rewrite firstn_length. rewrite <- Nat.le_succ_l.
   assert (1 <= Nat.div2 (length b)).
   rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r.
   replace (2 * Nat.div2 (length b)) with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))).
   rewrite <- Nat.div2_odd. assumption.
   rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
   apply Nat.lt_0_2.
   generalize H4. generalize H5. apply Nat.min_glb.
   apply Nat.lt_0_2.
Qed.


Lemma tm_step_cube7 : forall (n : nat),
     (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
     /\ 0 < length a)
  -> exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2
     /\ 0 < length b.
Proof.
  intros n. intro H.
  induction n.
  - destruct H. destruct H. destruct H. destruct H.
    exists x. exists x0. exists x1. split; assumption.
  - destruct H. destruct H. destruct H. destruct H.
    assert (J: exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2).
    generalize H0. generalize H. apply tm_step_cube6. rewrite Nat.pred_succ in J.
    apply IHn. apply J.
Qed.


Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
  tm_step n = hd ++ a ++ a ++ b ++ tl -> 0 < length a -> a <> b.
Proof.
  intros n hd a b tl. intros H I.

  assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.

  destruct J. rewrite <- e in H.

  assert (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
     /\ 0 < length a).
  exists hd. exists a. exists tl. split; assumption.

  assert (exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2
     /\ 0 < length b).
  generalize H0. apply tm_step_cube7.
  destruct H1. destruct H1. destruct H1. destruct H1.

  assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2.
  apply Nat.lt_irrefl in H3. contradiction H3.
  assumption.
Qed.