611 lines
25 KiB
Coq
611 lines
25 KiB
Coq
Require Import thue_morse.
|
|
|
|
Require Import Coq.Lists.List.
|
|
Require Import PeanoNat.
|
|
Require Import Nat.
|
|
Require Import Bool.
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
(**
|
|
The following lemma, while not of truly general use, is
|
|
used in several proofs and has therefore its own dedicated
|
|
section here.
|
|
*)
|
|
|
|
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 (I: even (length hd) = false).
|
|
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
|
|
apply bool_dec. destruct J. assumption. 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.
|
|
rewrite app_assoc in H.
|
|
assert (L: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
|
|
= count_occ Bool.bool_dec (hd ++ [b1;b1]) false).
|
|
assert (even (length (hd ++ [b1;b1])) = true).
|
|
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
|
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
generalize H0. 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 b1. simpl in L. inversion L. simpl in L. inversion L.
|
|
|
|
assert (J: {even (length (hd ++ [b1;b1] ++ a))
|
|
= false} + { ~ (even (length (hd ++ [b1;b1] ++ a))) = false}).
|
|
apply bool_dec. destruct J.
|
|
|
|
rewrite app_length in e. rewrite app_length in e.
|
|
rewrite Nat.add_assoc in e. rewrite Nat.add_shuffle0 in e.
|
|
rewrite Nat.even_add_even in e. rewrite Nat.even_add in e.
|
|
rewrite I in e. destruct (Nat.even (length a)). reflexivity.
|
|
simpl in e. inversion e. simpl.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
|
|
apply not_false_is_true in n0.
|
|
assert (K: even (length (hd ++ [b1;b1] ++ a ++ [b2;b2])) = true).
|
|
replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
|
|
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]).
|
|
rewrite app_length. rewrite Nat.even_add.
|
|
rewrite n0. reflexivity.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
assert (N: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) true
|
|
= count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) false).
|
|
replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
|
|
with ((hd ++ [b1;b1] ++ a ++ [b2;b2]) ++ tl) in H.
|
|
generalize K. generalize H. apply tm_step_count_occ.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
assert (M: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) true
|
|
= count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) false).
|
|
replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
|
|
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2] ++ tl) in H.
|
|
generalize n0. generalize H. apply tm_step_count_occ.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
|
|
with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]) in N.
|
|
rewrite count_occ_app in N. symmetry in N.
|
|
rewrite count_occ_app in N. rewrite M in N.
|
|
rewrite Nat.add_cancel_l in N.
|
|
destruct b2. simpl in N. inversion N. simpl in N. inversion N.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
Qed.
|
|
|
|
|
|
(**
|
|
The following lemmas and theorems are all related to
|
|
squares of odd length in the Thue-Morse sequence.
|
|
All squared factors of odd length have length 1 or 3.
|
|
*)
|
|
|
|
Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ tl -> length a = 5
|
|
-> a <> [ true; false; true; false; true].
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
|
|
destruct n.
|
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
|
rewrite H in H0 at 2. simpl in H0.
|
|
rewrite app_length in H0. rewrite app_length in H0.
|
|
rewrite I in H0. rewrite Nat.add_shuffle3 in H0.
|
|
apply Nat.succ_inj in H0. inversion H0.
|
|
|
|
assert (even (length (tm_step (S n))) = true).
|
|
rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul.
|
|
apply Nat.le_0_l.
|
|
|
|
assert (J: even (length hd) = negb (even (length tl))).
|
|
rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
|
|
rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0.
|
|
destruct (even (length hd)); destruct (even (length tl)).
|
|
inversion H0. reflexivity. reflexivity. inversion H0.
|
|
|
|
assert (K: {a=[true; false; true; false; true]}
|
|
+ {~ a=[ true; false; true; false; true]}).
|
|
apply list_eq_dec. apply bool_dec. destruct K.
|
|
|
|
assert ({even (length hd) = true} + {even (length hd) <> true}).
|
|
apply bool_dec. destruct H1.
|
|
|
|
(* case length hd is even *)
|
|
rewrite e0 in J. rewrite Nat.negb_even in J.
|
|
destruct tl. inversion J.
|
|
destruct b.
|
|
|
|
assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
|
|
generalize e0. generalize H. apply tm_step_count_occ.
|
|
|
|
assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true
|
|
= count_occ Bool.bool_dec (hd ++ a ++ [true]) false).
|
|
assert (even (length (hd ++ a ++ [true])) = true).
|
|
rewrite app_length. rewrite app_length.
|
|
rewrite Nat.even_add. rewrite Nat.even_add.
|
|
rewrite e0. rewrite e. reflexivity.
|
|
replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H.
|
|
generalize H2. generalize H. apply tm_step_count_occ.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
rewrite count_occ_app in H2. rewrite H1 in H2.
|
|
symmetry in H2.
|
|
rewrite count_occ_app in H2. rewrite Nat.add_cancel_l in H2.
|
|
|
|
rewrite count_occ_app in H2. rewrite count_occ_app in H2.
|
|
rewrite e in H2. simpl in H2. inversion H2.
|
|
|
|
replace (hd ++ a ++ false::tl)
|
|
with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
simpl. apply Nat.lt_0_2.
|
|
|
|
rewrite e. reflexivity.
|
|
|
|
(* case length hd is odd *)
|
|
apply not_true_is_false in n0.
|
|
rewrite app_removelast_last with (l := hd) (d := true) in H.
|
|
rewrite app_removelast_last with (l := hd) (d := true) in n0.
|
|
rewrite app_length in n0. simpl in n0.
|
|
rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0.
|
|
rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0.
|
|
|
|
destruct (last hd true).
|
|
rewrite <- app_assoc in H.
|
|
assert (count_occ Bool.bool_dec (removelast hd) true
|
|
= count_occ Bool.bool_dec (removelast hd) false).
|
|
generalize n0. generalize H. apply tm_step_count_occ.
|
|
replace (removelast hd ++ [true] ++ a ++ tl)
|
|
with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H.
|
|
assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true
|
|
= count_occ Bool.bool_dec (removelast hd ++ [true;true]) false).
|
|
assert (even (length (removelast hd ++ [true;true])) = true).
|
|
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
|
generalize H2. generalize H. apply tm_step_count_occ.
|
|
|
|
rewrite count_occ_app in H2. rewrite count_occ_app in H2.
|
|
rewrite H1 in H2. rewrite Nat.add_cancel_l in H2.
|
|
simpl in H2. inversion H2.
|
|
|
|
rewrite e. rewrite app_assoc_reverse. reflexivity.
|
|
|
|
replace ((removelast hd ++ [false]) ++ a ++ tl)
|
|
with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H.
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
simpl. apply Nat.lt_0_2.
|
|
|
|
rewrite e. rewrite app_assoc_reverse. reflexivity.
|
|
|
|
assert (length hd <> 0). destruct hd. inversion n0.
|
|
simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
|
|
assert (length hd <> 0). destruct hd. inversion n0.
|
|
simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
|
|
|
|
assumption.
|
|
Qed.
|
|
|
|
Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ tl -> length a = 5
|
|
-> a <> [ false; true; false; true; false].
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
assert (K: {a=[false; true; false; true; false]}
|
|
+ {~ a=[false; true; false; true; false]}).
|
|
apply list_eq_dec. apply bool_dec. destruct K.
|
|
assert (tm_step (S n) = hd ++ a ++ tl
|
|
++ (map negb hd) ++ [ true; false; true; false; true ]
|
|
++ (map negb tl)).
|
|
rewrite tm_build. rewrite H.
|
|
rewrite map_app. rewrite map_app.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. rewrite e. reflexivity.
|
|
rewrite app_assoc in H0. rewrite app_assoc in H0.
|
|
rewrite app_assoc in H0. apply tm_step_factor5 in H0.
|
|
contradiction H0. reflexivity.
|
|
reflexivity. assumption.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_step_consecutive_identical_length :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ tl -> length a = 5
|
|
-> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
destruct a. inversion I.
|
|
|
|
assert (a = nil). simpl in I.
|
|
apply Nat.succ_inj in I. apply Nat.succ_inj in I.
|
|
apply Nat.succ_inj in I. apply Nat.succ_inj in I.
|
|
apply Nat.succ_inj in I.
|
|
apply length_zero_iff_nil in I. assumption.
|
|
rewrite H0. rewrite H0 in H. rewrite H0 in I.
|
|
|
|
destruct b; destruct b0; destruct b1; destruct b2; destruct b3.
|
|
|
|
exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity.
|
|
exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity.
|
|
|
|
exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
|
|
exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
|
|
apply tm_step_factor5 in H. contradiction H. reflexivity. reflexivity.
|
|
exists (true::false::true::nil). exists (nil). exists false. simpl. reflexivity.
|
|
exists (true::false::false::nil). exists (nil). exists true. simpl. reflexivity.
|
|
exists (true::nil). exists (true::false::nil). exists false. simpl. reflexivity.
|
|
exists (true::nil). exists (false::true::nil). exists false. simpl. reflexivity.
|
|
exists (true::false::nil). exists (false::nil). exists false. simpl. reflexivity.
|
|
exists (false::nil). exists (true::true::nil). exists true. simpl. reflexivity.
|
|
exists (false::nil). exists (true::false::nil). exists true. simpl. reflexivity.
|
|
exists (false::nil). exists (false::true::nil). exists true. simpl. reflexivity.
|
|
exists (false::nil). exists (false::false::nil). exists true. simpl. reflexivity.
|
|
exists (false::true::false::nil). exists (nil). exists true. simpl. reflexivity.
|
|
apply tm_step_factor5' in H. contradiction H. reflexivity. reflexivity.
|
|
exists (false::true::nil). exists (true::nil). exists false. simpl. reflexivity.
|
|
exists (false::true::nil). exists (false::nil). exists false. simpl. reflexivity.
|
|
exists (false::false::nil). exists (true::nil). exists true. simpl. reflexivity.
|
|
exists (false::false::nil). exists (false::nil). exists true. simpl. reflexivity.
|
|
exists (nil). exists (true::false::true::nil). exists false. simpl. reflexivity.
|
|
exists (nil). exists (true::false::false::nil). exists false. simpl. reflexivity.
|
|
exists (nil). exists (false::true::true::nil). exists false. simpl. reflexivity.
|
|
exists (nil). exists (false::true::false::nil). exists false. simpl. reflexivity.
|
|
exists (nil). exists (false::false::true::nil). exists false. simpl. reflexivity.
|
|
exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
|
|
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.
|
|
rewrite <- firstn_skipn with (l := a) (n := 5).
|
|
assert (length (firstn 5 a) = 5).
|
|
apply firstn_length_le. apply Nat.le_succ_l. apply I.
|
|
rewrite <- firstn_skipn with (l := a) (n := 5) in H.
|
|
rewrite <- app_assoc in H.
|
|
assert (exists (b1 c1 : list bool) (d1 : bool),
|
|
firstn 5 a = b1 ++ [d1; d1] ++ c1).
|
|
generalize H0. generalize H. apply tm_step_consecutive_identical_length.
|
|
destruct H1. destruct H1. destruct H1. rewrite H1.
|
|
exists x. exists (x0 ++ (skipn 5 a)). exists x1.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
Qed.
|
|
|
|
|
|
Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
assert (J: 4 < length a \/ length a <= 4).
|
|
apply Nat.lt_ge_cases. destruct J.
|
|
assert (exists b c d, a = b ++ [d;d] ++ c).
|
|
generalize H0. generalize H. apply tm_step_consecutive_identical_length'.
|
|
destruct H1. destruct H1. destruct H1. rewrite H1 in H.
|
|
|
|
replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
|
|
with ((hd ++ x) ++ [x1;x1] ++ (x0++x) ++ [x1;x1] ++ (x0 ++ tl)) in H.
|
|
apply tm_step_consecutive_identical in H.
|
|
|
|
assert (J: even (length (x0 ++ x)) = false).
|
|
rewrite H1 in I. rewrite app_length in I. rewrite app_length in I.
|
|
rewrite Nat.add_shuffle3 in I. rewrite Nat.add_comm in I.
|
|
rewrite Nat.odd_add_even in I.
|
|
rewrite app_length. rewrite Nat.add_comm. rewrite <- Nat.negb_odd.
|
|
rewrite I. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
|
reflexivity. rewrite H in J. inversion J.
|
|
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. apply app_inv_head_iff. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
reflexivity.
|
|
|
|
apply Nat.le_lteq in H0. destruct H0. assumption.
|
|
rewrite H0 in I. inversion I.
|
|
Qed.
|
|
|
|
|
|
|
|
(**
|
|
New following lemmas and theorems are related to the size
|
|
of squares in the Thue-Morse sequence, namely lengths of
|
|
2^n or 3 * 2^n only.
|
|
*)
|
|
|
|
Lemma tm_step_shift_odd_prefix_even_squares :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ a ++ tl
|
|
-> even (length a) = true
|
|
-> odd (length hd) = true
|
|
-> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
|
|
/\ even (length hd') = true /\ length a = length b.
|
|
Proof.
|
|
intros n hd a tl. intros H I J.
|
|
|
|
assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
|
|
destruct W. rewrite e in J. simpl in J. rewrite Nat.odd_0 in J.
|
|
inversion J.
|
|
|
|
assert (Z: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
|
|
destruct Z.
|
|
exists (removelast hd). exists nil. exists ((last hd true)::nil++tl).
|
|
split. rewrite app_nil_l. rewrite app_nil_l. rewrite app_nil_l.
|
|
replace ((last hd true)::tl) with ([last hd true] ++ tl).
|
|
rewrite app_assoc. rewrite <- app_removelast_last.
|
|
rewrite H. rewrite e. rewrite app_nil_l. rewrite app_nil_l. reflexivity.
|
|
assumption.
|
|
split. rewrite app_removelast_last with (l := hd) (d := last hd true) in J.
|
|
rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
|
|
rewrite J. split. reflexivity. rewrite e. reflexivity. assumption.
|
|
|
|
rewrite app_removelast_last with (l := hd) (d := true) in H.
|
|
rewrite app_removelast_last with (l := a) (d := true) in H.
|
|
rewrite app_assoc_reverse in H.
|
|
rewrite app_removelast_last with (l := hd) (d := true) in J.
|
|
rewrite app_length in J. rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
|
|
rewrite app_removelast_last with (l := a) (d := true) in I.
|
|
rewrite app_length in I. rewrite Nat.add_1_r in I.
|
|
exists (removelast hd).
|
|
rewrite app_assoc_reverse in H. rewrite app_assoc_reverse in H.
|
|
replace (
|
|
removelast hd ++ [last hd true] ++
|
|
removelast a ++ [last a true] ++ removelast a ++ [last a true] ++ tl)
|
|
with (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
|
|
([last a true] ++ tl)) in H.
|
|
assert (K: count_occ Bool.bool_dec (removelast hd) true
|
|
= count_occ Bool.bool_dec (removelast hd) false).
|
|
generalize J. generalize H. apply tm_step_count_occ.
|
|
assert (L: count_occ Bool.bool_dec (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) true
|
|
= count_occ Bool.bool_dec (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) false).
|
|
assert (M: even (length (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a))) = true).
|
|
rewrite app_length. rewrite Nat.even_add_even. apply J.
|
|
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
|
rewrite Nat.even_add_even. rewrite app_length.
|
|
rewrite Nat.add_1_l. assumption.
|
|
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
|
rewrite Nat.add_1_l. assumption.
|
|
generalize M.
|
|
replace (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a) ++
|
|
([last a true] ++ tl))
|
|
with ((
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a) ++ ([last a true] ++ removelast a)) ++
|
|
([last a true] ++ tl)) in H.
|
|
generalize H. apply tm_step_count_occ.
|
|
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
|
|
assert (M: count_occ Bool.bool_dec (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a)) true
|
|
= count_occ Bool.bool_dec (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a)) false).
|
|
assert (N: even (length (
|
|
removelast hd ++
|
|
([last hd true] ++ removelast a))) = true).
|
|
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
|
rewrite app_length. apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
|
rewrite Nat.add_1_l. assumption.
|
|
generalize N.
|
|
rewrite app_assoc in H. generalize H. apply tm_step_count_occ.
|
|
|
|
rewrite count_occ_app in M. symmetry in M. rewrite count_occ_app in M.
|
|
rewrite K in M. rewrite Nat.add_cancel_l in M.
|
|
|
|
rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
|
|
rewrite K in L. rewrite Nat.add_cancel_l in L.
|
|
rewrite count_occ_app in L. symmetry in L. rewrite count_occ_app in L.
|
|
rewrite M in L. rewrite Nat.add_cancel_l in L.
|
|
|
|
assert (O: forall (m: nat), m <> S (S m)).
|
|
induction m. easy. apply not_eq_S. assumption.
|
|
|
|
assert (N: last hd true = last a true).
|
|
destruct (last hd true); destruct (last a true).
|
|
reflexivity.
|
|
rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
|
|
rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
|
|
rewrite L in M. apply O in M. contradiction M.
|
|
rewrite count_occ_app in L. rewrite count_occ_app in L. simpl in L.
|
|
rewrite count_occ_app in M. rewrite count_occ_app in M. simpl in M.
|
|
rewrite <- L in M. symmetry in M. apply O in M. contradiction M.
|
|
reflexivity.
|
|
|
|
rewrite N in H. exists ([last a true] ++ removelast a).
|
|
exists ([last a true] ++ tl). rewrite H.
|
|
|
|
split. reflexivity.
|
|
split. assumption.
|
|
rewrite app_length. rewrite app_removelast_last with (l := a) (d := true).
|
|
rewrite app_length. rewrite last_last. rewrite removelast_app.
|
|
rewrite Nat.add_1_r. rewrite app_nil_r. reflexivity. easy.
|
|
|
|
assumption.
|
|
rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
|
|
assumption. assumption. assumption. assumption.
|
|
Qed.
|
|
|
|
Lemma tm_step_normalize_prefix_even_squares :
|
|
forall (n : nat) (hd a tl : list bool),
|
|
tm_step n = hd ++ a ++ a ++ tl
|
|
-> even (length a) = true
|
|
-> exists (hd' b tl': list bool), tm_step n = hd' ++ b ++ b ++ tl'
|
|
/\ even (length hd') = true /\ length a = length b.
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
assert (odd (length hd) = true \/ odd (length hd) = false).
|
|
destruct (odd (length hd)). left. reflexivity. right. reflexivity.
|
|
destruct H0.
|
|
generalize H0. generalize I. generalize H.
|
|
apply tm_step_shift_odd_prefix_even_squares.
|
|
exists hd. exists a. exists tl.
|
|
split. assumption. split. rewrite <- Nat.negb_odd. rewrite H0.
|
|
reflexivity. reflexivity.
|
|
Qed.
|
|
|
|
|
|
Lemma tm_step_square_half : forall (n : nat) (hd a tl : list bool),
|
|
tm_step (S n) = hd ++ a ++ a ++ tl
|
|
-> even (length a) = true
|
|
-> exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
|
|
/\ length a = Nat.double (length a').
|
|
Proof.
|
|
intros n hd a tl. intros H I.
|
|
assert (
|
|
exists (hd' b tl': list bool), tm_step (S n) = hd' ++ b ++ b ++ tl'
|
|
/\ even (length hd') = true /\ length a = length b).
|
|
generalize I. generalize H. apply tm_step_normalize_prefix_even_squares.
|
|
destruct H0. destruct H0. destruct H0.
|
|
destruct H0. destruct H1. rewrite H2 in I.
|
|
rewrite <- tm_step_lemma in H0.
|
|
assert (x = tm_morphism (firstn (Nat.div2 (length x)) (tm_step n))).
|
|
apply tm_morphism_app2 with (tl := x0 ++ x0 ++ x1). apply H0.
|
|
assumption.
|
|
assert (x0 ++ x0 ++ x1 = tm_morphism (skipn (Nat.div2 (length x)) (tm_step n))).
|
|
apply tm_morphism_app3. apply H0. assumption.
|
|
|
|
assert (Z := H0).
|
|
|
|
assert (H7: length (tm_morphism (tm_step n)) = length (tm_morphism (tm_step n))).
|
|
reflexivity. rewrite Z in H7 at 2. rewrite tm_morphism_length in H7.
|
|
rewrite app_length in H7.
|
|
rewrite app_length in H7.
|
|
rewrite Nat.Even_double with (n := length x) in H7.
|
|
rewrite Nat.Even_double with (n := length x0) in H7.
|
|
rewrite Nat.Even_double with (n := length (x0 ++ x1)) in H7.
|
|
rewrite Nat.double_twice in H7.
|
|
rewrite Nat.double_twice in H7.
|
|
rewrite Nat.double_twice in H7.
|
|
rewrite <- Nat.mul_add_distr_l in H7.
|
|
rewrite <- Nat.mul_add_distr_l in H7.
|
|
rewrite Nat.mul_cancel_l in H7.
|
|
|
|
assert (x0 = tm_morphism (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n)))).
|
|
apply tm_morphism_app2 with (tl := x0 ++ x1). symmetry. assumption.
|
|
assumption.
|
|
|
|
assert (x1 = tm_morphism (skipn (Nat.div2 (length (x0++x0)))
|
|
(skipn (Nat.div2 (length x)) (tm_step n)))).
|
|
apply tm_morphism_app3. symmetry. rewrite app_assoc_reverse. apply H4.
|
|
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
|
|
rewrite H3 in H0. rewrite H5 in H0. rewrite H6 in H0.
|
|
rewrite <- tm_morphism_app in H0.
|
|
rewrite <- tm_morphism_app in H0.
|
|
rewrite <- tm_morphism_app in H0.
|
|
rewrite <- tm_morphism_eq in H0.
|
|
rewrite H0.
|
|
exists (firstn (Nat.div2 (length x)) (tm_step n)).
|
|
exists (firstn (Nat.div2 (length x0)) (skipn (Nat.div2 (length x)) (tm_step n))).
|
|
exists (skipn (Nat.div2 (length (x0 ++ x0))) (skipn (Nat.div2 (length x)) (tm_step n))).
|
|
split. reflexivity.
|
|
rewrite firstn_length_le. rewrite <- Nat.Even_double. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
rewrite skipn_length.
|
|
|
|
rewrite H7. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
|
|
rewrite Nat.add_0_l. rewrite <- Nat.add_0_r at 1.
|
|
rewrite <- Nat.add_le_mono_l.
|
|
apply le_0_n. apply le_n. easy.
|
|
|
|
rewrite <- Nat.Even_double in H7. rewrite <- Nat.Even_double in H7.
|
|
rewrite Nat.add_assoc in H7.
|
|
assert (Nat.even (2 * (length (tm_step n))) = true).
|
|
apply Nat.even_mul. rewrite H7 in H5.
|
|
rewrite Nat.even_add in H5.
|
|
rewrite Nat.even_add in H5.
|
|
rewrite I in H5. rewrite H1 in H5.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT.
|
|
destruct (Nat.even (length (x0 ++ x1))). reflexivity.
|
|
inversion H5.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
|
|
Qed.
|
|
|
|
|
|
|
|
Theorem tm_step_square_size : forall (n k j : nat) (hd a tl : list bool),
|
|
tm_step (S n) = hd ++ a ++ a ++ tl
|
|
-> length a = (S (Nat.double k)) * 2^j
|
|
-> (k = 0 \/ k = 1).
|
|
Proof.
|
|
intros n k j hd a tl.
|
|
generalize hd. generalize a. generalize tl. induction j.
|
|
- intros tl0 a0 hd0. intros H I. simpl in I. rewrite Nat.mul_1_r in I.
|
|
assert (odd (length a0) = true). rewrite I.
|
|
rewrite Nat.odd_succ. rewrite Nat.double_twice.
|
|
apply Nat.even_mul.
|
|
assert (J: length a0 < 4). generalize H0. generalize H.
|
|
apply tm_step_odd_square.
|
|
rewrite I in J.
|
|
destruct k. left. reflexivity.
|
|
destruct k. right. reflexivity.
|
|
apply Nat.succ_lt_mono in J.
|
|
apply Nat.lt_lt_succ_r in J.
|
|
rewrite Nat.double_twice in J. replace (4) with (2*2) in J.
|
|
rewrite <- Nat.mul_lt_mono_pos_l in J.
|
|
apply Nat.succ_lt_mono in J.
|
|
apply Nat.succ_lt_mono in J.
|
|
apply Nat.nlt_0_r in J. contradiction J.
|
|
apply Nat.lt_0_2. reflexivity.
|
|
- intros tl0 a0 hd0. intros H I.
|
|
assert (exists (hd' a' tl' : list bool), tm_step n = hd' ++ a' ++ a' ++ tl'
|
|
/\ length a0 = Nat.double (length a')).
|
|
assert (even (length a0) = true).
|
|
rewrite I. rewrite Nat.pow_succ_r'. rewrite Nat.mul_comm.
|
|
rewrite <- Nat.mul_assoc. apply Nat.even_mul.
|
|
generalize H0. generalize H. apply tm_step_square_half.
|
|
destruct H0. destruct H0. destruct H0. destruct H0.
|
|
rewrite H1 in I. rewrite Nat.pow_succ_r' in I. rewrite Nat.mul_comm in I.
|
|
rewrite <- Nat.mul_assoc in I. rewrite Nat.double_twice in I.
|
|
rewrite Nat.mul_cancel_l in I. rewrite Nat.mul_comm in I.
|
|
generalize I.
|
|
assert (tm_step (S n) = x ++ x0 ++ x0 ++ x1 ++ (map negb (tm_step n))).
|
|
rewrite tm_build. rewrite H0.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
rewrite <- app_assoc. reflexivity.
|
|
generalize H2. apply IHj. easy.
|
|
Qed.
|
|
|
|
|
|
|
|
|