(*
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_map_explode : forall (l1 l2 : list bool),
  map negb (l1 ++ l2) = map negb l1 ++ map negb l2.
Proof.
  intros l1 l2.
  induction l1.
  - reflexivity.
  - simpl. rewrite IHl1. reflexivity.
Qed.

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 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 negb_map_explode.
    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.

(* 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 negb_map_explode. rewrite negb_double_map.
    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.


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.
  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.

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

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

  assert (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.

  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.

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

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

  assert (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.

  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.





(*
  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) (k : nat),
  tm_step k = hd ++ tl -> even (length hd) = true
  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
Proof.
  intros hd tl k. intros H I.
  destruct k.
  - 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 k))).
    generalize I. generalize H. apply tm_morphism_app2.
    rewrite J. apply tm_morphism_count_occ.
Qed.








Prouver l'énoncé du concours général
(parmi les n premiers termes avec n pairs, il y en a autant de chaque)

Prouver que si un cube existe il est de taille paire

Prouver que si un cube existe de taille k, il existe aussi un cube
de même taille précédé par un préfixe de taille pair (par décalage éventuel de 1)

Prouver que si un cube existe, de taille paire, précédé par un préfixe pair,
alors (par référence au morphisme, il existait à la génération précédente
un cube de taille moitié précédé par un préfixe pair

--> absurdité : on ne peut diviser indéfiniment par 2 et rester sur du pair













  (* TODO: supprimer head_2 *)

(* vérifier si les deux sont nécessaires *)
Require Import BinPosDef.
Require Import BinPos.

Require Import BinNat.


(* Hamming weight of a positive; argument can not be 0! *)
Fixpoint hamming_weight_positive (x: positive) :=
  match x with
  | xH   => 1
  | xO p => hamming_weight_positive p
  | xI p => 1 + hamming_weight_positive p
  end.

Definition hamming_weight_n (x: N) :=
  match x with
  | N0 => 0
  | Npos x => hamming_weight_positive x
  end.









Lemma hamming_weight_positive_nonzero : forall (x: positive),
  hamming_weight_positive x > 0.
Proof.
  intros x.
  induction x.
  - simpl. apply Arith_prebase.gt_Sn_O_stt.
  - simpl. apply IHx.
  - simpl. apply Arith_prebase.gt_Sn_O_stt.
Qed.



Lemma size_double_bin : forall (x: positive),
  Pos.size_nat (Pos.succ (Pos.pred_double x)) = S (Pos.size_nat x).
Proof.
  intros x.
  rewrite Pos.succ_pred_double.
  reflexivity.
Qed.

Lemma succ_succ_pred_double_succ : forall (x: positive),
  Pos.pred_double (Pos.succ x) = Pos.succ (Pos.succ (Pos.pred_double x)).
Proof.
  intros x.
  rewrite <- Pos.add_1_l.
  rewrite Pos.add_xO_pred_double.
  rewrite <- Pos.add_1_l.
  rewrite <- Pos.add_1_l.
  rewrite Pos.add_assoc.
  reflexivity.
Qed.                                                                                  
Lemma size_double_bin2 : forall (x: positive),
  Pos.size_nat (Pos.pred_double (Pos.succ x)) = S (Pos.size_nat x).
Proof.
  intros x.
  rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
  reflexivity.
Qed.

Lemma size_succ_double_bin : forall (x: positive),
  Pos.size_nat (Pos.succ (Pos.succ (Pos.pred_double x))) = S (Pos.size_nat x).
Proof.
  intros x.
  rewrite <- succ_succ_pred_double_succ. rewrite size_double_bin2.
  reflexivity.
Qed.

Lemma nat_size_pos_size : forall (x: positive),
  N.size_nat (N.pos x) = Pos.size_nat x.
Proof.
  intros x. reflexivity.
Qed.

Lemma hamming_weight_increase : forall (x: positive),
  hamming_weight_positive x~1 = S (hamming_weight_positive x).
Proof.
  intros x. reflexivity.
Qed.


Fixpoint bin2power (x : positive) (k : N) :=
  match x with
  | xH   => (2^k)%N
  | xO y => bin2power y (N.succ k)
  | xI y => (2^k + bin2power y (N.succ k))%N
  end.

Lemma bin2power_same : forall  (x : positive),
  Npos x = bin2power x 0.
Proof.
  intros x. 
  induction x.
  - simpl.



(*
Fixpoint bin2power (x : positive) (k : nat) :=
  match x with
  | xH   => 2^k
  | xO y => bin2power y (S k)
  | xI y => 2^k + bin2power y (S k)
  end.
 *)

Lemma bin2power_double : forall (x : positive) (k : N),
  bin2power x~0 k = bin2power x (N.succ k).
Proof.
  intros x. simpl. reflexivity.
Qed.

Lemma bin2power_double2 : forall (x : positive),
  bin2power x~0 0%N = (2 * bin2power x 0)%N.
Proof.
  intros x.
  destruct x.
  - simpl.


N.testbit_even_succ:
  forall a n : N, (0 <= n)%N -> N.testbit (2 * a) (N.succ n) = N.testbit a n







  simpl. reflexivity.
Qed.

Lemma bin2power_succ : forall (x : positive) (k : N),
  bin2power (x~1) k = ((2^k)%N + (bin2power (x~0) k))%N.
Proof.
  intros x k.
  reflexivity.
Qed.

Lemma bin2power_double2 : forall (x : positive),
  bin2power x 1%N = (2 * bin2power x 0)%N.
Proof.
  intros x.
  induction x.
  - rewrite bin2power_succ. rewrite bin2power_succ. rewrite N.pow_0_r.
    rewrite N.mul_add_distr_l. rewrite N.pow_1_r. rewrite N.mul_1_r.
    rewrite N.add_cancel_l.
    replace (bin2power x~0 0) with (bin2power x 1%N).





    assert ((2 * bin2power (Pos.succ x~0) 0)%N = (2 + 2*binpower (x~0) 0)%N).

    replace (x~0) with ((N.pos (N.shiftl (x) 1) 1)%N).
  



  induction x.
  - simpl. rewrite Nat.add_0_r. apply eq_S. rewrite <- plus_n_Sm.
    apply eq_S.
    destruct x.
    + simpl.




    rewrite Pos.xI_succ_xO.
    rewrite <- bin2power_double.


  rewrite bin2power_double.



  - rewrite bin2power_double.
    assert ( I: bin2power x~1 0 = S (bin2power x~0 0) ).
    { simpl. reflexivity. } rewrite I.
    assert ( J: bin2power x~1 1 = S (S (S (bin2power x~0 1) ))).
    { rewrite <- I.






  simpl. rewrite Nat.add_0_r.






Qed.

Lemma bin2power_same : forall (x: positive),
  bin2power x 0 = Pos.to_nat x.
Proof.
  intros x.
  induction x.
  - simpl. rewrite <- Pos.pred_double_succ.
    rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.

    rewrite <- Pos.xI_succ_xO.
    rewrite <- bin2power_double.

    assert (I: bin2power x 1 = 2 * (bin2power x 0)).
    { induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
      simpl in IHx.


    assert (I: bin2power x 1 = 2 * (bin2power x 0)).
    { induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
      simpl in IHx.


Lemma tm_step_hamming : forall (x: N),
  nth_error (tm_step (N.size_nat x)) (N.to_nat x)
  = Some (odd (hamming_weight_n x)).
Proof.
  intros x.
  destruct x.
  - reflexivity.
  - induction p.
    + rewrite <- Pos.pred_double_succ.

      rewrite nat_size_pos_size.
      rewrite succ_succ_pred_double_succ at 1.
      rewrite size_succ_double_bin.

      unfold hamming_weight_n. rewrite Pos.pred_double_succ.
      rewrite hamming_weight_increase. rewrite Nat.odd_succ.
      rewrite <- Nat.negb_odd.

      rewrite tm_build. rewrite nth_error_app1.






      apply map_nth_error.




      rewrite succ_succ_pred_double_succ.







      simpl. rewrite Pos.succ_pred_double.
      rewrite size_double_bin.


      unfold N.to_nat at 2. unfold Pos.to_nat. simpl.
      
      rewrite Pos.xI_succ_xO.   transforme p~1 en Pos.succ p~0
      Lemma pred_double_succ p : pred_double (succ p) = p~1.
      Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
      Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.




Theorem tm_step_hamming_index : forall (n : N),
  nth_error (tm_step (N.to_nat n)) (N.to_nat n)
     = Some (odd (hamming_weight_n n)).
Proof.
  intros n.
  destruct n.
  - reflexivity.
  - induction p. simpl.




Theorem tm_step_hamming_index : forall (n m : nat) (k j: N),
  (N.to_nat k) < 2^n -> (N.to_nat j) < 2^m ->
    hamming_weight_n k = hamming_weight_n j ->
    nth_error (tm_step n) (N.to_nat k) = nth_error (tm_step m) (N.to_nat j).
Proof.
  intros n m k j. intros H I K.
  induction k.
  - simpl in K. assert (j = N0). induction j. reflexivity.
    rewrite <- N.succ_pos_pred. 
    unfold hamming_weight_n in K.
    assert (L: hamming_weight_positive p > 0).
    apply hamming_weight_positive_nonzero. rewrite <- K in L.
    apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
    rewrite H0. rewrite H0 in I.
    generalize I. generalize H. apply tm_step_stable.
  - induction j. simpl in K. assert (L: hamming_weight_positive p > 0).
    apply hamming_weight_positive_nonzero. rewrite K in L.
    apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
    (* coeur de l'induction *)


    induction p. simpl in K.
    symmetry in K. apply Nat.neq_succ_0 in K. contradiction K.



    Theorem N. succ_0_discr n : succ n <> 0.
  Nat.neq_succ_0: forall n : nat, S n <> 0






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






Lemma tm_step_index_split :
  forall (a b n m : nat),
  (* every natural number k can be written according to the following form *)
  a < 2^n -> (a + 2^n * b) < 2^m
    -> nth_error (tm_step m) (a + 2^n * b)
        = nth_error (tm_step (S m)) (a + 2^S n * b).
Proof.
  intros a b n m. intros H I.







Lemma tm_step_cancel_high_bits :
  forall (k b n m : nat),
  (* every natural number k can be written according to the following form *)
  S k < 2^m -> k = 2^n - 1 + 2^S n * b
    -> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
      <-> odd n = true.
Proof.
  intros k b n m. intros H I.

  assert (L: 2^n - 1 < 2^n). apply Nat.sub_lt. replace (1) with (2^0) at 1.
  apply Nat.pow_le_mono_r. easy.
  apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.

  assert (M: S(2^n - 1) = 2^n). rewrite Nat.sub_1_r. apply Nat.succ_pred.
  apply Nat.pow_nonzero. apply Nat.neq_succ_0.

  assert (N: 2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
  apply Nat.lt_succ_diag_r.

  assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
              <-> odd n = true).
  rewrite tm_step_single_bit_index.
  assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
  apply tm_step_stable. apply L.
  assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
  apply Nat.lt_succ_diag_r.
  generalize H0. generalize L. apply Nat.lt_trans. rewrite <- H0.
  rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
  rewrite <- J. rewrite I.


  destruct b.

  (* case b = 0 *)
  rewrite Nat.mul_0_r. rewrite Nat.add_0_r.
  rewrite J. rewrite Nat.mul_0_r in I. rewrite Nat.add_0_r in I.
  rewrite I in H. rewrite M.

  assert (nth_error (tm_step m) (2^n-1) = nth_error (tm_step n) (2^n-1)).
  generalize L. apply tm_step_stable. apply Nat.lt_succ_l. apply H.
  rewrite H0. rewrite tm_step_repunit_index.

  assert (nth_error (tm_step m) (2^n) = nth_error (tm_step (S n)) (2 ^ n)).
  generalize N. rewrite M in H. generalize H. apply tm_step_stable.
  rewrite H1. rewrite tm_step_single_bit_index.

  split. intros. inversion H2. reflexivity. intros. inversion H2.
  reflexivity.

  (* case b > 0 *)
  assert (S b = Pos.to_nat (Pos.of_nat (S b))).




  destruct n.
  - rewrite Nat.pow_0_r. rewrite Nat.sub_diag. rewrite plus_O_n.
    rewrite Nat.pow_1_r.
    rewrite Nat.pow_0_r in I. simpl in I. rewrite Nat.add_0_r in I.
    induction m.
    + rewrite Nat.pow_0_r in H.
      assert (K := H). rewrite Nat.lt_1_r in K.
      apply Nat.neq_succ_0 in K. contradiction K.
    +





  induction k.
  - rewrite <- I.
    assert (b=0).
    { symmetry in I. rewrite Nat.eq_add_0 in I. destruct I.
      apply Nat.mul_eq_0_r in H1. apply H1. apply Nat.pow_nonzero.
      easy. }
    rewrite H0 in I. rewrite Nat.mul_0_r in I.
    rewrite Nat.add_0_r in I. rewrite <- I.

    replace (2^n) with (S (2^n - 1)). rewrite <- I.

    split.

    intros. rewrite tm_step_head_2 at 2. rewrite tm_step_head_1. simpl.
    replace (m) with (S (m-1)) in H1 at 2.
    rewrite tm_step_head_2 in H1. rewrite tm_step_head_1 in H1. simpl in H1.
    apply H1.
    destruct m. simpl in H. apply Nat.lt_irrefl in H. contradiction H.
    rewrite Nat.sub_1_r. simpl. reflexivity.

    intros. rewrite tm_step_head_2 in H1 at 2.
    rewrite tm_step_head_1 in H1. simpl in H1. inversion H1.
    rewrite <- I.
    apply eq_S in I. rewrite I at 1.
    apply Nat.pred_inj. apply Nat.neq_succ_0. apply Nat.pow_nonzero.
    easy. simpl. rewrite Nat.sub_1_r. reflexivity.

  - apply IHk. apply Nat.lt_succ_l in H. apply H.
    rewrite <- I.




    split. intros. apply H1.








    assert (K: S (2 ^ n - 1 + 2 ^ S n * b) = (2 ^ n + 2 ^ S n * b)).
    + rewrite Nat.sub_1_r. rewrite <- Nat.add_succ_l.
      rewrite Nat.succ_pred_pos. reflexivity.
      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
    + rewrite K. symmetry.
      split. intros. symmetry.
      apply tm_step_add_range2_flip_two.


  (*
  assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
  apply tm_step_repunit.
   *)
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)).
  






Déclagae vers la droite de k zéros pour un Bins :
Pos.iter xO xH 3.   (ici k = 3)
  --> on ajoute 3 zéros à gauche









Require Import BinPosDef.


(* Autre construction de la suite, ici n est le nombre de termes *)
(* la construction se fait à l'envers *)
(*
Fixpoint tm_bin_rev (n: nat) : list bool :=
  match n with
  | 0 => nil
  | S n' => let t := tm_bin_rev n' in
            let m := Pos.of_nat n' in
              (xorb (hd true t) (odd (Pos.size_nat
                match Pos.lxor m (Pos.pred m) with
                | N0 => BinNums.xH
                | Npos(p)  => p
                end))) :: t
  end.
*)

Fixpoint tm_bin (n: nat) : list bool :=
  match n with
  | 0 => nil
  | S n' => let t := tm_bin n' in
            let m := Pos.of_nat n' in
            t ++ [ xorb (last t true)
                     (odd (Pos.size_nat match Pos.lxor m (Pos.pred m) with
                                        | N0 => BinNums.xH
                                        | Npos(p)  => p
                                        end)) ]
  end.

Theorem tm_morphism_eq_bin : forall (k : nat), tm_step k = tm_bin (2^k).
Proof.
Admitted.





Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
  tm_step n = l1 ++ b1 :: b2 :: l2 ->
    (eqb b1 b2) = 
      let ind_b2 := Pos.of_nat (S (length l1)) in (* index of b2 *)
      let ind_b1 := Pos.pred ind_b2 in            (* index of b1 *)
       even (Pos.size_nat
         match Pos.lxor ind_b1 ind_b2 with
         | N0 => BinNums.xH
         | Npos(p)  => p
         end).
Proof.
  intros n l1 l2 b1 b2.
  destruct n.
  - simpl. intros H. induction l1.
    + rewrite app_nil_l in H. discriminate.
    + destruct l1. rewrite app_nil_l in IHl1. discriminate. discriminate.
  - rewrite tm_build.
Admitted.




(*
  intros n l1 l2 b1 b2.
  intros H.
  induction l1.
  - simpl. destruct n. discriminate.
    rewrite app_nil_l in H. assert (I := H).
    rewrite tm_step_head_2 in I. injection I.
    assert (J: tl (tl (tm_morphism (tm_step n))) = l2).
    { replace (tm_morphism (tm_step n)) with (tm_step (S n)).
      rewrite H. reflexivity. reflexivity. }
    (* rewrite J *) intros. rewrite <- H1. rewrite <- H2. reflexivity.
  - replace (S (length (a :: l1))) with (S (S (length l1))).







    destruct b1 in H.
    + destruct b2 in H.
      (* Case 1: b1 = true, b2 = true  (false)   *)
      replace (l2) with (tl (tl (tm_step (S n)))) in H.
      assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
      apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
      (* Case 2: b1 = true, b2 = false  (false)   *)
      replace (l2) with (tl (tl (tm_step (S n)))) in H.
      assert (J : tm_step (S n) = false :: true :: tl (tl (tm_step (S n)))).
      apply tm_step_head_2. rewrite J in H. discriminate H. rewrite H. reflexivity.
    + destruct b2.
      (* Case 3: b1 = false, b2 = true  (TRUE)   *)
      discriminate.






    inversion H.
    discriminate tm_step_head_2.
    rewrite <- tm_step_head_2 in H.
    discriminate H.
    discriminate tm_step_head_2.

  - simpl. simpl. simpl in H.
    destruct n in H. discriminate H.
    replace (l2) with (tl (tl (tm_step (S n)))) in H.
    specialize (H tm_step_head_2).
    rewrite <- tm_step_head_2 in H.



Lemma tm_step_head_2 : forall (n : nat),
    tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
 *)