baruchel
/
coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
coqbooks/src/thue_morse.v

1414 lines
52 KiB
Coq
Raw Blame History

(** * The Thue-Morse sequence
Some proofs related to the Thue-Morse sequence.
See:
- 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.
(**
This whole notebook contains proofs related to the following two functions.
Nothing else is defined afterwards in the current notebook.
*)
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.
(**
More or less "general" lemmas, which are not directly related to
the previous functions are proved below.
*)
Lemma lt_split_bits : forall n m k j,
0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
Proof.
intros n m k j. intros H I J.
assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
apply Nat.mul_le_mono_r with (p := 2^m) in H0.
rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
rewrite Nat.add_le_mono_r with (p := j) in H0.
assert (2^n - 2^m + j < 2^n).
rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
rewrite Nat.add_lt_mono_r with (p := 2^m).
rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
apply Nat.lt_le_incl. assumption.
generalize H1. generalize H0. apply Nat.le_lt_trans.
apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
Qed.
Lemma count_occ_bool_list : forall (a: list bool),
length a = (count_occ bool_dec a true) + (count_occ bool_dec a false).
Proof.
intro a.
induction a.
- reflexivity.
- destruct a.
+ rewrite count_occ_cons_eq. rewrite count_occ_cons_neq.
simpl. rewrite IHa. reflexivity. easy. reflexivity.
+ rewrite count_occ_cons_neq. rewrite count_occ_cons_eq.
simpl. rewrite Nat.add_succ_r. rewrite IHa. reflexivity. reflexivity. easy.
Qed.
Lemma count_occ_bool_list2 : forall (a: list bool),
count_occ bool_dec a false = count_occ bool_dec a true -> even (length a) = true.
Proof.
intro a. intro H.
rewrite count_occ_bool_list. rewrite H.
replace (count_occ bool_dec a true) with (1 * (count_occ bool_dec a true)).
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
replace (2 * count_occ bool_dec a true) with (0 + 2 * count_occ bool_dec a true).
apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l.
Qed.
Lemma app_eq_length_head : forall x0 x1 y0 y1 : list bool,
x0 ++ x1 = y0 ++ y1 -> length x0 = length y0 -> x0 = y0.
Proof.
intro x0. induction x0. destruct y0. intros. reflexivity.
intros. inversion H0. destruct y0. intros. inversion H0.
intros. simpl in H0. apply Nat.succ_inj in H0.
rewrite <- app_comm_cons in H.
rewrite <- app_comm_cons in H.
destruct a; destruct b. inversion H.
apply IHx0 with (x1 := x1) (y1 := y1) in H2. rewrite H2. reflexivity.
assumption. inversion H. inversion H. inversion H.
apply IHx0 with (x1 := x1) (y1 := y1) in H2. rewrite H2. reflexivity.
assumption.
Qed.
Lemma even_mod4 : forall n : nat,
even n = true -> n mod 4 = 0 \/ n mod 4 = 2.
Proof.
intro n. intro H.
assert (K: 0 = n mod 2).
apply Nat.mod_unique with (q := Nat.div2 n). apply Nat.lt_0_2.
replace (0) with (Nat.b2n (Nat.odd n)) at 2.
apply Nat.div2_odd. rewrite <- Nat.negb_even. rewrite H. reflexivity.
assert (L: n mod (2*2) = n mod 2 + 2 * ((n / 2) mod 2)).
apply Nat.mod_mul_r; easy. rewrite <- K in L.
replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
rewrite L.
destruct (Nat.testbit (n / 2) 0) ; [right | left] ; reflexivity.
reflexivity.
Qed.
Lemma odd_mod4 : forall n : nat,
odd n = true -> n mod 4 = 1 \/ n mod 4 = 3.
Proof.
intro n. intro H.
assert (K: 1 = n mod 2).
apply Nat.mod_unique with (q := Nat.div2 n). apply Nat.lt_1_2.
replace (1) with (Nat.b2n (Nat.odd n)) at 2.
apply Nat.div2_odd. rewrite H. reflexivity.
assert (L: n mod (2*2) = n mod 2 + 2 * ((n / 2) mod 2)).
apply Nat.mod_mul_r; easy. rewrite <- K in L.
replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
rewrite L.
destruct (Nat.testbit (n / 2) 0) ; [right | left] ; reflexivity.
reflexivity.
Qed.
(**
Some lemmas related to the first function (tm_morphism) are proved here.
They have a wider scope than the following ones since they don't focus on
the Thue-Morse sequence by itself.
*)
Lemma tm_morphism_concat : forall (l1 l2 : list bool),
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
Proof.
intros l1 l2.
induction l1.
- reflexivity.
- simpl. rewrite IHl1. reflexivity.
Qed.
Lemma tm_morphism_rev : forall (l : list bool),
rev (tm_morphism l) = tm_morphism (map negb (rev l)).
Proof.
intro l. induction l.
- reflexivity.
- simpl. rewrite map_app.
rewrite IHl. rewrite tm_morphism_concat.
rewrite <- app_assoc. simpl.
rewrite negb_involutive. reflexivity.
Qed.
Lemma tm_build_negb : forall (l : list bool),
tm_morphism (map negb l) = map negb (tm_morphism l).
Proof.
intro l.
induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
Qed.
Lemma tm_morphism_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_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_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_length_half : forall (u : list bool),
Nat.div2 (length (tm_morphism u)) = length u.
Proof.
intro u.
induction u. reflexivity.
simpl. rewrite IHu. reflexivity.
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_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: (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l) = l).
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.
(**
Lemmas and theorems below are related to the second function defined initially.
They focus on the Thue-Morse sequence.
*)
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.
rewrite tm_morphism_rev. rewrite tm_build_negb. 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.
- rewrite <- tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
rewrite tm_step_lemma. rewrite IHn. rewrite tm_build_negb.
rewrite <- IHn. rewrite tm_step_lemma. reflexivity.
Qed.
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
Proof.
intro n.
induction n.
- reflexivity.
- rewrite <- tm_step_lemma. rewrite tm_morphism_length.
rewrite Nat.pow_succ_r. rewrite Nat.mul_cancel_l.
assumption. easy. apply Nat.le_0_l.
Qed.
Lemma tm_step_head_1 : forall (n : nat),
tm_step n = false :: tl (tm_step n).
Proof.
intro n.
induction n.
- reflexivity.
- rewrite <- tm_step_lemma. rewrite IHn. reflexivity.
Qed.
Lemma tm_step_end_1 : forall (n : nat),
rev (tm_step n) = odd n :: tl (rev (tm_step n)).
Proof.
intro n.
induction n.
- reflexivity.
- rewrite <- tm_step_lemma. rewrite tm_morphism_rev.
rewrite IHn. simpl. rewrite <- Nat.negb_even at 1. rewrite Nat.odd_succ.
rewrite negb_involutive. reflexivity.
Qed.
Lemma tm_step_odd_step : forall (n : nat),
rev (tm_step (S (Nat.double n))) = map negb (tm_step (S (Nat.double n))).
Proof.
intro n. induction n.
- reflexivity.
- rewrite <- tm_step_lemma. rewrite tm_morphism_rev.
rewrite Nat.double_S. rewrite tm_build. rewrite rev_app_distr.
rewrite tm_build_negb. rewrite IHn. rewrite <- IHn at 1.
rewrite rev_involutive. 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. apply tm_morphism_double_index.
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.
- apply Nat.le_refl.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (pred (2^n)) = Some (odd n).
Proof.
intro n.
rewrite <- Nat.sub_1_r. rewrite <- tm_size_power2.
rewrite nth_error_nth' with (d := false).
- rewrite <- rev_nth. rewrite tm_step_end_1. simpl. reflexivity.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
- rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
Qed.
Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
tm_step n = hd ++ tl -> even (length hd) = true
-> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
Proof.
intros hd tl n. intros H I.
destruct n.
- assert (J: hd = nil). destruct hd. reflexivity.
simpl in H. inversion H.
symmetry in H2. apply app_eq_nil in H2.
destruct H2. rewrite H0 in I. simpl in I. inversion I.
rewrite J. reflexivity.
- rewrite <- tm_step_lemma in H.
assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
rewrite J. apply tm_morphism_count_occ.
Qed.
Lemma tm_step_consecutive_identical :
forall (n : nat) (hd tl : list bool) (b : bool),
tm_step n = hd ++ (b::b::nil) ++ tl
-> odd (length hd) = true.
Proof.
intros n hd tl b. intro H.
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
apply bool_dec. destruct J.
- rewrite <- Nat.negb_even. rewrite e. reflexivity.
- apply not_false_is_true in n0.
assert (K: count_occ Bool.bool_dec hd true
= count_occ Bool.bool_dec hd false).
generalize n0. generalize H. apply tm_step_count_occ.
assert (L: count_occ Bool.bool_dec (hd ++ [b;b]) true
= count_occ Bool.bool_dec (hd ++ [b;b]) false).
assert (even (length (hd ++ [b;b])) = true).
rewrite app_length. rewrite Nat.even_add_even. assumption.
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
generalize H0. rewrite app_assoc in H. generalize H.
apply tm_step_count_occ.
rewrite count_occ_app in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b; inversion L.
Qed.
Lemma tm_step_consecutive_identical' :
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
-> even (length a) = true.
Proof.
intros n hd a tl b1 b2. intros H.
assert (Nat.odd (length hd) = true).
generalize H. apply tm_step_consecutive_identical.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (Nat.odd (length ((hd ++ [b1;b1])++a)) = true).
generalize H. apply tm_step_consecutive_identical.
rewrite app_length in H1. rewrite Nat.odd_add in H1.
rewrite app_length in H1. rewrite Nat.odd_add in H1. rewrite H0 in H1.
replace (Nat.odd (length a)) with (negb (Nat.even (length a))) in H1.
destruct (even (length a)). reflexivity. inversion H1.
reflexivity.
Qed.
Theorem tm_step_length_even : forall (n : nat),
0 < n -> even (length (tm_step n)) = true.
Proof.
intro n. intro H.
rewrite tm_size_power2. destruct n. inversion H.
rewrite Nat.pow_succ_r'. rewrite Nat.even_mul. reflexivity.
Qed.
Theorem tm_step_not_nil_factor_even : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> even (length a) = true
-> 0 < n.
Proof.
intros n hd a tl. intros H I J.
assert (M: 1 < length (tm_step n)). rewrite H.
rewrite app_length. rewrite app_length.
assert (0 <= length hd). apply le_0_n.
assert (2 <= length a + length tl). rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. destruct a. inversion I.
destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply le_0_n.
apply le_0_n. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l.
rewrite plus_n_Sm. apply Nat.add_le_mono; assumption.
rewrite tm_size_power2 in M.
rewrite Nat.pow_lt_mono_r_iff with (a := 2). simpl. assumption.
apply Nat.lt_1_2.
Qed.
Theorem tm_step_tail_not_nil_prefix_odd : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> odd (length hd) = true
-> even (length a) = true
-> nil <> tl.
Proof.
intros n hd a tl. intros H I J K.
assert (L: 0 < n). generalize K. generalize I. generalize H.
apply tm_step_not_nil_factor_even.
assert (M: even (length (tm_step n)) = true). generalize L.
apply tm_step_length_even.
destruct tl. rewrite app_nil_r in H.
rewrite H in M. rewrite app_length in M.
rewrite Nat.even_add in M. rewrite K in M. rewrite <- Nat.negb_odd in M.
rewrite J in M. inversion M. apply nil_cons.
Qed.
(**
The following lemmas and theorems focus on the stability of the sequence:
while lists in the sequence get longer and longer, the beginning of a
longer list contain the same elements as the previous shorter lists.
*)
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.
rewrite H0. rewrite app_length. rewrite <- H1. simpl.
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
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_0_r. 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. apply Nat.add_0_r.
- 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. apply Nat.add_0_r.
Qed.
(**
The following lemma states that a block of terms in the Thue-Morse
sequence having a size being a power of 2 is repeated, either
as an identical version or with all values together flipped.
*)
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. rewrite <- Nat.add_1_r in H0 at 1.
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
rewrite Nat.add_0_r in H0. assumption.
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.
apply Nat.add_comm. assumption.
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
apply Nat.add_comm. 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.
(**
The following lemmas and theorems are related to flipping the
most significant bit in the numerical value of indices (of terms
in the lists).
*)
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.
(**
The following lemmas and theorems are related to flipping the
least significant bit in the numerical value of indices (of terms
in the lists).
*)
(* 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)).
apply tm_step_single_bit_index.
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.
(**
The following lemmas and theorems are of general interest; they
come here because they use more specific previously defined
lemmas and theorems.
*)
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. rewrite <- Nat.pow_1_r with (a := 2).
replace (S (k*2^1)) with (k*2^1 + 2^0).
apply tm_step_flip_low_bit. apply Nat.lt_0_1.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
apply Nat.add_lt_mono; assumption.
simpl. apply Nat.add_1_r.
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) (pred (S (2*k) * 2^m))
<-> 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.pred_succ.
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.
inversion 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: pred( S (2 * k) * 2 ^ m) < S (2 * k) * 2 ^ m).
apply Nat.lt_pred_l. apply Nat.neq_mul_0.
split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0. assumption.
assert (N: pred (2 * (S (2 * k) * 2 ^ m)) < length (tm_step (S n0))).
rewrite tm_size_power2.
rewrite <- Nat.le_succ_l. rewrite Nat.succ_pred_pos. rewrite Nat.pow_succ_r.
apply Nat.mul_le_mono_l. generalize I. apply Nat.lt_le_incl.
apply Nat.le_0_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption.
assert(T: pred (S (2 * k) * 2 ^ m) < 2 ^ n0).
generalize I. generalize L. apply Nat.lt_trans.
assert (nth_error (tm_step n0) (pred (S (2 * k) * 2 ^ m))
<> nth_error (tm_step (S n0)) (S (2 * (pred(S (2 * k) * 2 ^ m))))).
apply tm_step_succ_double_index. assumption.
replace (S (2 * (pred(S (2 * k) * 2 ^ m)))) with (pred(2 * (S (2*k) * 2^m))) 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) (pred(S (2 * k) * 2 ^ m))).
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) (pred(S (2 * k) * 2 ^ m)));
intro K; simpl in K; inversion 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 (pred (S (2 * k) * 2 ^ m)) (tm_step n0) false);
destruct (nth (pred (2 * (S (2 * k) * 2 ^ m))) (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.add_1_r at 4.
rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l.
rewrite <- Nat.add_1_r at 1.
rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l.
rewrite <- Nat.add_succ_l. rewrite Nat.succ_pred_pos. rewrite <- Nat.add_pred_r.
reflexivity. apply Nat.neq_mul_0. split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0.
assumption. 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_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool),
tm_step n' = w ++ z ++ y
-> length z = 4 -> length w mod 4 = 1
-> exists (x : bool), firstn 2 z = [x;x].
intros n' w z y. intros G0 G1 G2.
assert (U: 4 * (length w / 4) <= length w).
apply Nat.mul_div_le. easy.
assert (W: length w < length (tm_step n')). rewrite G0.
rewrite app_length. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_lt_mono_l.
rewrite app_length. rewrite G1. apply Nat.lt_0_succ.
assert (Q: length z <= length (tm_step n')). rewrite G0.
rewrite app_length. rewrite app_length.
rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
apply Nat.le_add_l. rewrite tm_size_power2 in Q. rewrite G1 in Q.
replace (4) with (2^2) in Q. rewrite <- Nat.pow_le_mono_r_iff in Q.
assert (O: nth_error (tm_step 2) 1 = nth_error (tm_step 2) 2
<-> nth_error (tm_step (2+(n'-2))) (length w / 4 * 2 ^ 2 + 1)
= nth_error (tm_step (2+(n'-2))) (length w / 4 * 2 ^ 2 + 2)).
apply tm_step_repeating_patterns.
simpl. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ.
rewrite Nat.mul_lt_mono_pos_l with (p := 2^2). rewrite <- Nat.pow_add_r.
rewrite Nat.add_comm. rewrite Nat.sub_add.
replace (2^2) with 4.
rewrite tm_size_power2 in W. generalize W. generalize U.
apply Nat.le_lt_trans. reflexivity.
assumption.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite Nat.mul_comm in O. replace (2^2) with 4 in O.
rewrite <- G2 in O at 9. rewrite <- G2 in O at 14.
replace (4 * (length w / 4) + S (length w mod 4))
with (S (length w)) in O. rewrite <- Nat.div_mod_eq in O.
replace (2+(n'-2)) with n' in O. rewrite G0 in O.
rewrite nth_error_app2 in O. rewrite Nat.sub_diag in O.
rewrite nth_error_app1 in O. rewrite nth_error_app2 in O.
rewrite Nat.sub_succ_l in O. rewrite Nat.sub_diag in O.
rewrite nth_error_app1 in O. destruct O.
assert (nth_error z 0 = nth_error z 1). apply H. reflexivity.
rewrite nth_error_nth' with (d := false) in H1.
rewrite nth_error_nth' with (d := false) in H1.
exists (nth 0 z false). inversion H1.
rewrite H3 at 2.
destruct z. inversion G1. destruct z. inversion G1. reflexivity.
rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
rewrite G1. apply Nat.lt_0_succ.
rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
apply Nat.le_refl. apply Nat.le_succ_diag_r.
rewrite G1. apply Nat.lt_0_succ. apply Nat.le_refl.
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
reflexivity. easy. assumption.
rewrite Nat.add_succ_r. rewrite <- Nat.div_mod_eq. reflexivity.
reflexivity. apply Nat.lt_1_2. reflexivity.
Qed.
Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
tm_step n' = w ++ z ++ y
-> length z = 4 -> length w mod 4 = 3
-> exists (x : bool), skipn 2 z = [x;x].
Proof.
intros n hd a tl. intros H I M.
assert ((length (hd ++ (firstn 2 a))) mod 4 = 1).
rewrite app_length. rewrite firstn_length. rewrite I.
rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy.
assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)).
apply tm_build. rewrite H in H1.
assert (length ((skipn 2 a)
++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4).
rewrite app_length. rewrite skipn_length. rewrite I.
rewrite firstn_length. rewrite app_length. rewrite <- H.
rewrite map_length.
assert (4 <= length tl + length (tm_step n)).
assert (Q: length a <= length (tm_step n)). rewrite H.
rewrite app_length. rewrite app_length.
rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
apply Nat.le_add_l. rewrite I in Q.
rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity.
assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l.
generalize H2. generalize H3. apply Nat.le_trans.
replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl))
with ((hd ++ firstn 2 a)
++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H1.
assert (exists (x : bool),
firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
= [x;x]).
generalize H0. generalize H2. generalize H1. apply tm_step_factor4_1mod4.
destruct H3. exists x.
rewrite <- H3. rewrite firstn_app. rewrite skipn_length. rewrite I.
replace (2 - (4 - 2)) with 0. rewrite firstn_O.
rewrite app_nil_r.
destruct a. inversion I. destruct a. inversion I.
destruct a. inversion I. destruct a. inversion I.
destruct a. reflexivity. inversion I.
reflexivity.
rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
apply app_inv_head_iff.
rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
rewrite firstn_skipn.
rewrite <- firstn_skipn with (n := 2) (l := a) at 4.
rewrite <- app_assoc. reflexivity.
Admitted.
Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> length a = 4 -> odd (length hd) = true
-> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
Proof.
intros n hd a tl. intros H I M.
apply odd_mod4 in M.
destruct M as [M | M].
- assert (exists (x : bool), firstn 2 a = [x;x]).
generalize M. generalize I. generalize H. apply tm_step_factor4_1mod4.
destruct H0. exists x. exists nil. exists (skipn 2 a).
rewrite app_nil_l. rewrite <- H0. symmetry. apply firstn_skipn.
- assert (exists (x : bool), skipn 2 a = [x;x]).
generalize M. generalize I. generalize H. apply tm_step_factor4_3mod4.
destruct H0. exists x. exists (firstn 2 a). exists nil.
rewrite app_nil_r. rewrite <- H0. symmetry. apply firstn_skipn.
Qed.
Lemma tm_step_consecutive_identical_length :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl -> 4 < length a
-> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
Proof.
intros n hd a tl. intros H I.
assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
apply Nat.Even_or_Odd. destruct J as [J | J].
(* first case *)
replace (hd++a++tl)
with ((hd ++ (firstn 1 a)) ++ (skipn 1 (firstn 5 a))
++ ((skipn 5 a) ++ tl)) in H.
assert (length (skipn 1 (firstn 5 a)) = 4).
rewrite skipn_length. rewrite firstn_length.
rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
reflexivity. assumption.
assert (odd (length (hd ++ firstn 1 a)) = true).
rewrite app_length. rewrite Nat.odd_add. rewrite <- Nat.negb_even.
apply Nat.Even_EvenT in J. apply Nat.EvenT_even in J. rewrite J.
rewrite firstn_length. rewrite Nat.min_l. reflexivity.
apply Nat.lt_le_incl.
assert (1 < 4). rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
generalize I. generalize H1. apply Nat.lt_trans.
assert (exists (x : bool) (u v : list bool),
skipn 1 (firstn 5 a) = u ++ [x;x] ++ v).
generalize H1. generalize H0. generalize H. apply tm_step_factor4_odd_prefix.
destruct H2. destruct H2. destruct H2.
exists ((firstn 1 a) ++ x0). exists (x1 ++ (skipn 5 a)). exists x.
replace ((firstn 1 a ++ x0) ++ [x; x] ++ x1 ++ skipn 5 a)
with (firstn 1 a ++ (x0 ++ [x;x] ++ x1) ++ skipn 5 a). rewrite <- H2.
rewrite app_assoc. replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
rewrite firstn_skipn. rewrite firstn_skipn. reflexivity.
rewrite firstn_firstn. reflexivity.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
rewrite <- app_assoc. apply app_inv_head_iff.
replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
rewrite app_assoc. rewrite firstn_skipn.
rewrite app_assoc. rewrite firstn_skipn.
reflexivity.
rewrite firstn_firstn. reflexivity.
(* second case *)
replace (hd++a++tl) with (hd ++ (firstn 4 a) ++ ((skipn 4 a) ++ tl)) in H.
assert (length (firstn 4 a) = 4). rewrite firstn_length.
rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
reflexivity. assert (4 <= 5). apply Nat.le_succ_diag_r.
generalize I. generalize H0. apply Nat.le_trans.
apply Nat.Odd_OddT in J. apply Nat.OddT_odd in J.
assert (exists (x : bool) (u v : list bool), firstn 4 a = u ++ [x;x] ++ v).
generalize J. generalize H0. generalize H. apply tm_step_factor4_odd_prefix.
destruct H1. destruct H1. destruct H1.
exists x0. exists (x1++(skipn 4 a)). exists x.
replace (x0 ++ [x;x] ++ x1 ++ (skipn 4 a))
with ((x0++[x;x]++x1) ++ (skipn 4 a)).
rewrite <- H1. rewrite firstn_skipn. reflexivity.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
apply app_inv_head_iff.
rewrite app_assoc. rewrite firstn_skipn. reflexivity.
Qed.
(**
Some more lemmas are added there as convenient tools for further
investigations; they have been added quite late, after many
following results were proved, but they are inserted here in
case some proofs are re-written later.
*)
Lemma tm_step_morphism2 :
forall (n : nat) (hd tl : list bool),
tm_step (S n) = hd ++ tl
-> even (length hd) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
skipn (Nat.div2 (length hd)) (tm_step n)).
Proof.
intros n hd tl. intros H I.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app3.
rewrite H0 in H. rewrite H1 in H. rewrite <- tm_morphism_app in H.
assumption.
Qed.
Lemma tm_step_morphism3 :
forall (n : nat) (hd a tl : list bool),
tm_step (S n) = hd ++ a ++ tl
-> even (length hd) = true
-> even (length a) = true
-> tm_morphism (tm_step n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
skipn (Nat.div2 (length hd + length a)) (tm_step n)).
Proof.
intros n hd a tl. intros H I J. rewrite <- tm_step_lemma in H.
assert (even (length (hd ++ a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. symmetry in H1. generalize H1. apply tm_morphism_app3.
rewrite skipn_firstn_comm in H4.
rewrite H3 in H. rewrite H4 in H. rewrite H2 in H.
rewrite app_length in H.
rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H.
rewrite <- Nat.div2_div in H. rewrite Nat.add_sub_swap in H.
rewrite Nat.sub_diag in H. rewrite Nat.add_0_l in H.
rewrite Nat.div2_div in H at 3. rewrite <- Nat.div_add in H.
rewrite Nat.mul_comm in H.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))) in H.
rewrite <- Nat.div2_odd in H. rewrite <- Nat.div2_div in H.
assumption.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity. easy.
apply Nat.le_refl.
replace (length a) with (Nat.div2 (length a) * 2) at 2.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div. reflexivity.
easy. rewrite Nat.mul_comm.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))).
rewrite Nat.div2_odd. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
Qed.
Lemma tm_step_morphism4 :
forall (n : nat) (hd a b tl : list bool),
tm_step (S n) = hd ++ a ++ b ++ tl
-> even (length hd) = true
-> even (length a) = true
-> even (length b) = true
-> tm_step (S n) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step n) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step n)) ++
firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++
skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)).
Proof.
intros n hd a b tl. intros H I J K.
assert (even (length (hd ++ a)) = true).
rewrite app_length. rewrite Nat.even_add.
rewrite I. rewrite J. reflexivity.
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app2.
assert (b ++ tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a)))
(tm_step n))).
generalize H0. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc in H. symmetry in H1. symmetry in H2.
assert (even (length (hd ++ a ++ b)) = true).
rewrite app_length. rewrite Nat.even_add. rewrite I.
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
reflexivity.
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ b)))
(tm_step n))).
replace (hd ++ a ++ b ++ tl) with ((hd ++ a ++ b) ++ tl) in H.
generalize H3. generalize H. apply tm_morphism_app3.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
generalize I. generalize H. apply tm_morphism_app2.
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize I. generalize H1. apply tm_morphism_app3.
assert (b = tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
generalize K. generalize H2. apply tm_morphism_app2.
rewrite skipn_firstn_comm in H6. rewrite app_length in H6.
replace (Nat.div2 (length hd + length a))
with ((length hd) / 2 + Nat.div2 (length a)) in H6.
rewrite <- Nat.div2_div in H6. rewrite Nat.add_sub_swap in H6.
rewrite Nat.sub_diag in H6. rewrite Nat.add_0_l in H6.
rewrite H5 in H. rewrite H6 in H. rewrite H7 in H. rewrite H4 in H.
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
rewrite <- tm_morphism_app in H. rewrite tm_step_lemma in H.
assumption.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
rewrite Nat.mul_comm.
replace (2 * Nat.div2 (length a))
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))).
rewrite <- Nat.div2_odd. reflexivity.
rewrite <- Nat.negb_even. rewrite J.
rewrite <- Nat.add_0_r. reflexivity.
easy.
Qed.
Reference in New Issue View Git Blame Copy Permalink