(* 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. 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. (* 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 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_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. 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))). assumption. Qed. --> 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))). *)