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

510 lines
21 KiB
Coq
Raw Blame History

(** * The Thue-Morse sequence (part 4)
TODO
*)
Require Import thue_morse.
Require Import thue_morse2.
Require Import thue_morse3.
Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Bool.
Require Import Arith.
Require Import Lia.
Import ListNotations.
Theorem tm_step_palindrome_power2_inverse :
forall (m n k : nat) (hd tl : list bool),
tm_step n = hd ++ tl
-> length hd = S (Nat.double k) * 2^m
-> odd m = true
-> tl <> nil
-> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
Proof.
intros m n k hd tl. intros H I J K.
assert (L: 2^m <= length hd). rewrite I. lia.
assert (M: m < n). assert (length (tm_step n) = length (hd ++ tl)).
rewrite H. reflexivity. rewrite tm_size_power2 in H0.
rewrite app_length in H0. (* rewrite I in H0. *)
assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H1.
apply Nat.pow_le_mono_r with (a := 2) in H1.
assert (2^n <= length hd). generalize L. generalize H1. apply Nat.le_trans.
rewrite H0 in H2. rewrite <- Nat.add_0_r in H2.
rewrite <- Nat.add_le_mono_l in H2. destruct tl. contradiction K.
reflexivity. simpl in H2. apply Nat.nle_succ_0 in H2. contradiction.
easy. assumption.
assert (N: length (tm_step n) mod 2^m = 0). rewrite tm_size_power2.
apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite <- Nat.pow_sub_r.
rewrite <- Nat.pow_add_r. rewrite Nat.add_comm. rewrite Nat.sub_add.
reflexivity. apply Nat.lt_le_incl. assumption. easy.
apply Nat.lt_le_incl. assumption.
assert (O: length hd mod 2^m = 0).
apply Nat.div_exact. apply Nat.pow_nonzero. easy. rewrite I.
rewrite Nat.div_mul. rewrite Nat.mul_comm. reflexivity.
apply Nat.pow_nonzero. easy.
assert (P: length tl mod 2 ^ m = 0).
rewrite H in N. rewrite app_length in N.
rewrite <- Nat.add_mod_idemp_l in N. rewrite O in N. assumption.
apply Nat.pow_nonzero. easy.
assert (Q: 2^m <= length tl). apply Nat.div_exact in P. rewrite P.
destruct (length tl / 2^m). rewrite Nat.mul_0_r in P.
apply length_zero_iff_nil in P. rewrite P in K. contradiction K.
reflexivity.
rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_l.
apply Nat.le_succ_l. apply Nat.lt_0_succ.
apply Nat.pow_nonzero. easy.
replace hd
with (firstn (length hd - 2^m) hd ++ skipn (length hd - 2^m) hd) in H.
replace tl with (firstn (2^m) tl ++ skipn (2^m) tl) in H.
rewrite <- app_assoc in H.
replace (
skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl ++ skipn (2 ^ m) tl )
with (
(skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) ++ skipn (2 ^ m) tl )
in H.
assert (length (skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl) = 2^(S m)).
rewrite app_length. rewrite skipn_length. rewrite firstn_length_le.
replace (length hd) with (length hd -2^m + 2^m) at 1.
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. simpl. rewrite Nat.add_0_r.
reflexivity. apply Nat.le_refl. apply Nat.sub_add. assumption.
assumption.
assert (length (firstn (length hd - 2^m) hd) mod 2^(S m) = 0).
rewrite firstn_length_le. replace (2^m) with (2^m * 1).
rewrite I. rewrite Nat.mul_comm. rewrite <- Nat.mul_sub_distr_l.
rewrite Nat.sub_succ. rewrite Nat.sub_0_r. rewrite Nat.double_twice.
rewrite Nat.mul_assoc. replace (2^m * 2) with (2^(S m)).
rewrite Nat.mul_comm. rewrite Nat.mod_mul. reflexivity.
apply Nat.pow_nonzero. easy.
rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. reflexivity.
apply Nat.le_0_l. apply Nat.mul_1_r. apply Nat.le_sub_l.
assert (
skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = tm_step (S m)
\/
skipn (length hd - 2 ^ m) hd ++ firstn (2 ^ m) tl = map negb (tm_step (S m))).
generalize H1. generalize H0. generalize H. apply tm_step_repeating_patterns2.
apply tm_step_palindromic_full in J.
destruct H2; rewrite J in H2.
- assert (skipn (length hd - 2^m) hd = tm_step m).
apply app_eq_length_head in H2. assumption.
rewrite skipn_length.
replace (length hd) with (length hd -2^m + 2^m) at 1.
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite tm_size_power2.
reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3.
assert (firstn (2^m) tl = rev (tm_step m)).
rewrite H3 in H2. apply app_inv_head in H2. rewrite <- H2. reflexivity.
rewrite H4. rewrite rev_involutive. reflexivity.
- assert (skipn (length hd - 2^m) hd = map negb (tm_step m)).
rewrite map_app in H2. apply app_eq_length_head in H2. assumption.
rewrite skipn_length. replace (length hd) with (length hd -2^m + 2^m) at 1.
rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite map_length. rewrite tm_size_power2.
reflexivity. reflexivity. apply Nat.sub_add. assumption. rewrite H3.
assert (firstn (2^m) tl = map negb (rev (tm_step m))).
rewrite H3 in H2. rewrite map_app in H2. apply app_inv_head in H2.
rewrite <- H2. reflexivity.
rewrite H4. rewrite map_rev. rewrite rev_involutive. reflexivity.
- rewrite <- app_assoc. reflexivity.
- rewrite firstn_skipn. reflexivity.
- rewrite firstn_skipn. reflexivity.
Qed.
Theorem tm_step_palindrome_power2_inverse' :
forall (m n k : nat) (hd tl : list bool),
tm_step n = hd ++ tl
-> length hd = S (Nat.double k) * 2^m
-> odd m = true
-> 0 < k
-> skipn (length hd - 2^m) hd = rev (firstn (2^m) tl).
Proof.
intros m n k hd tl. intros H I J L.
assert (K: {tl=nil} + {~ tl=nil}). apply list_eq_dec. apply bool_dec.
destruct K as [K|K]. rewrite K in H. rewrite app_nil_r in H.
rewrite <- H in I. rewrite tm_size_power2 in I.
assert (n <= m \/ m < n). apply Nat.le_gt_cases. destruct H0.
apply Nat.pow_le_mono_r with (a := 2) in H0. rewrite I in H0.
rewrite <- Nat.mul_1_l in H0. rewrite <- Nat.mul_le_mono_pos_r in H0.
rewrite <- Nat.succ_le_mono in H0. apply Nat.le_0_r in H0.
rewrite Nat.double_twice in H0. apply Nat.mul_eq_0_r in H0.
rewrite H0 in L. inversion L. easy.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. easy.
replace n with (n-m+m) in I. rewrite Nat.pow_add_r in I.
rewrite Nat.mul_cancel_r in I.
assert (even (2^(n-m)) = true). apply Nat.sub_gt in H0.
apply Nat.neq_0_lt_0 in H0. destruct (n-m). inversion H0.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l. rewrite I in H1. rewrite Nat.even_succ in H1.
rewrite Nat.double_twice in H1. rewrite Nat.odd_mul in H1.
inversion H1. apply Nat.pow_nonzero. easy. lia.
generalize K. generalize J. generalize I. generalize H.
apply tm_step_palindrome_power2_inverse.
Qed.
(*
Lemma xxx :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
-> a = rev a \/ a = map negb (rev a).
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. rewrite app_length in H0. rewrite app_length in H0.
rewrite app_length in H0. rewrite Nat.add_comm in H0.
destruct a. inversion I. rewrite <- Nat.add_assoc in H0.
rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
assert (exists k j, length a = S (Nat.double k) * 2^j).
apply trailing_zeros; assumption. destruct H0. destruct H0.
assert (x = 0 \/ x = 1). generalize H0. generalize H.
apply tm_step_square_size.
generalize dependent n. generalize dependent hd. generalize dependent a.
generalize dependent tl. generalize dependent x.
induction x0; intros x K tl a J I hd n H.
- destruct K; rewrite H0 in I; destruct a.
inversion J. destruct a. left. reflexivity. inversion I.
inversion I. destruct a. inversion I. destruct a. inversion I.
destruct a.
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e. left. reflexivity.
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
apply tm_step_consecutive_identical' in H. inversion H.
rewrite <- app_assoc. reflexivity.
assert (b = b0). destruct b; destruct b0; destruct b1;
reflexivity || contradiction n0 || contradiction n1; reflexivity.
rewrite H1 in H.
replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
inversion I.
- assert (even (length a) = true).
rewrite Nat.mul_comm in I. rewrite Nat.pow_succ_r in I. rewrite I.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l.
assert (even (length (hd ++ a)) = true).
generalize J. generalize H. apply tm_step_square_pos.
assert (even (length hd) = true).
rewrite app_length in H1. rewrite Nat.even_add in H1.
rewrite H0 in H1. destruct (Nat.even (length hd)). reflexivity.
inversion H1.
(se débarrasser du S x0 en I)
generalize H. generalize n. generalize hd. generalize I. generalize J.
apply IHx0.
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)).
*)
Lemma xxx :
forall (j n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
-> a = rev a.
Proof.
intro j. induction j; intros n hd a tl; intros H I.
- destruct I.
+ destruct a. inversion H0. destruct a. reflexivity. inversion H0.
+ destruct a. inversion H0. destruct a. inversion H0. destruct a.
inversion H0. destruct a.
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e. reflexivity.
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl)
with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H.
apply tm_step_consecutive_identical' in H. inversion H.
rewrite <- app_assoc. reflexivity.
assert (b = b0). destruct b; destruct b0; destruct b1;
reflexivity || contradiction n0 || contradiction n1; reflexivity.
rewrite H1 in H.
replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl)
with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H.
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
inversion H0.
- assert (even (length a) = true).
destruct I; rewrite H0; rewrite Nat.double_S;
rewrite Nat.pow_succ_r.
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l.
assert (0 < length a). destruct I; rewrite H1.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.mul_pos_pos. lia.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (even (length (hd ++ a)) = true). generalize H1. generalize H.
apply tm_step_square_pos.
assert (even (length hd) = true). rewrite app_length in H2.
rewrite Nat.even_add in H2. rewrite H0 in H2.
destruct (even (length hd)). reflexivity. inversion H2.
assert (2 <= n).
assert (length (tm_step n) = length (tm_step n)). reflexivity.
rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4.
rewrite app_length in H4. destruct I; rewrite H5 in H4;
rewrite tm_size_power2 in H4; rewrite Nat.double_S in H4;
symmetry in H4; apply Nat.eq_le_incl in H4.
assert (2^(S (S (Nat.double j))) <= 2^n).
assert (2^(S (S (Nat.double j)))
<= 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd).
rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4.
generalize H6. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H6.
assert (2 <= S (S (Nat.double j))). lia. generalize H6. generalize H7.
apply Nat.le_trans. apply Nat.lt_1_2.
assert (3 * 2^(S (S (Nat.double j))) <= 2^n).
assert (3 * 2^(S (S (Nat.double j)))
<= 3 * 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd).
rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4.
generalize H6. apply Nat.le_trans.
assert (2^(S (S (Nat.double j))) <= 3 * 2^(S (S (Nat.double j)))).
rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_pos_r.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. lia.
assert (2^(S (S (Nat.double j))) <= 2^n).
generalize H6. generalize H7. apply Nat.le_trans.
rewrite <- Nat.pow_le_mono_r_iff in H8.
assert (2 <= S (S (Nat.double j))). lia. generalize H8. generalize H9.
apply Nat.le_trans. apply Nat.lt_1_2.
destruct n. inversion H4. destruct n. inversion H4. inversion H6.
assert(
tm_step (S (S n)) = tm_morphism
(firstn (Nat.div2 (length hd)) (tm_step (S n)) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step (S n))) ++
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))) ++
skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n)))).
generalize H0. generalize H0. generalize H3. generalize H.
apply tm_step_morphism4.
pose (hd' := firstn (Nat.div2 (length hd)) (tm_step (S n))).
pose (a' := firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length hd)) (tm_step (S n)))).
pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n))).
fold hd' in H5. fold a' in H5. fold tl' in H5.
assert (length hd' = Nat.div2 (length hd)). unfold hd'.
rewrite firstn_length_le. reflexivity.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.
assert (length hd = length (tm_morphism hd')).
rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
assert (length a' = Nat.div2 (length a)). unfold a'.
rewrite firstn_length_le. reflexivity. rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (length a = length (tm_morphism a')).
rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite H in H5. rewrite tm_morphism_app in H5.
assert (hd = tm_morphism hd'). generalize H7. generalize H5.
apply app_eq_length_head. rewrite <- H10 in H5.
apply app_inv_head in H5. rewrite tm_morphism_app in H5.
assert (a = tm_morphism a'). generalize H9. generalize H5.
apply app_eq_length_head. rewrite <- H11 in H5.
apply app_inv_head in H5. rewrite tm_morphism_app in H5.
assert (length a = length (tm_morphism (
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n)))))).
rewrite tm_morphism_length. rewrite firstn_length_le.
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_assoc.
rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite app_length. lia. apply Nat.le_refl.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (a = tm_morphism (
firstn (Nat.div2 (length a))
(skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))))).
generalize H12. generalize H5. apply app_eq_length_head.
rewrite <- H13 in H5. apply app_inv_head in H5.
assert (H' := H).
rewrite H10 in H'. rewrite H11 in H'. rewrite H5 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'. rewrite <- tm_morphism_eq in H'.
assert (even (length a') = true). unfold a'.
rewrite firstn_length_le.
destruct I; rewrite H14; rewrite Nat.double_S.
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
rewrite Nat.div2_double.
rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l.
rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
rewrite <- Nat.mul_assoc.
rewrite Nat.div2_double.
rewrite Nat.even_mul. rewrite Nat.even_mul.
reflexivity. apply Nat.le_0_l. apply Nat.le_0_l.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (0 < length a'). unfold a'. rewrite firstn_length_le.
destruct (length a). destruct I. inversion H1. inversion H1.
destruct n0. inversion H0. replace (S (S n0)) with (n0 + 1*2).
rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia.
easy. lia.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (even (length (hd' ++ a')) = true). generalize H15.
generalize H'. apply tm_step_square_pos.
assert (even (length hd') = true). rewrite app_length in H16.
rewrite Nat.even_add in H16. rewrite H14 in H16.
destruct (even (length hd')). reflexivity. inversion H16.
assert (
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 a'))
(skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)) ++
skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n))).
generalize H14. generalize H14. generalize H17. generalize H'.
apply tm_step_morphism4.
Lemma xxx :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> a = rev a
-> 0 < length a
-> length a <= 4
\/ (exists m, length a = 2 ^ m /\
length (hd ++ a) mod 2 ^ pred (Nat.double (Nat.div2 (S m))) = 0)
\/ length a = 3 * 2^(pred (Nat.log2 (length a))).
Proof.
intros n hd a tl. intros H I J.
destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0.
rewrite app_length in H0. rewrite Nat.add_comm in H0.
destruct a. inversion J. rewrite <- Nat.add_assoc in H0.
rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0.
apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction.
assert (exists k j, length a = S (Nat.double k) * 2^j).
apply trailing_zeros; assumption. destruct H0. destruct H0.
assert (x = 0 \/ x = 1). generalize H0. generalize H.
apply tm_step_square_size.
rewrite I in H at 2.
destruct H1; rewrite H1 in H0.
- rewrite Nat.mul_1_l in H0.
assert (length a <= 4 \/ 4 < length a). apply Nat.le_gt_cases.
destruct H2. left. assumption.
assert (2 < x0). destruct x0. rewrite H0 in H2. inversion H2.
inversion H4. destruct x0. rewrite H0 in H2. inversion H2.
inversion H4. inversion H6. destruct x0. rewrite H0 in H2.
inversion H2. inversion H4. inversion H6. inversion H8. inversion H10.
lia.
assert (length (hd ++ a) mod 2^(pred (Nat.double (Nat.div2 (S x0)))) = 0).
generalize H3. generalize H0. generalize H.
apply tm_step_palindrome_power2.
right. left. exists x0. split; assumption.
- right. right. rewrite H0. rewrite Nat.mul_cancel_l.
rewrite Nat.log2_mul_pow2. rewrite Nat.add_1_r.
rewrite Nat.pred_succ. reflexivity. lia. lia. lia.
Qed.
Reference in New Issue View Git Blame Copy Permalink