(** * 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 tm_step_square_even_rev : 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. pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)). pose (a'' := firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length hd')) (tm_step n))). pose (tl'' := skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n)). fold hd'' in H18. fold a'' in H18. fold tl'' in H18. 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 H19. 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 H21. rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. reflexivity. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. rewrite H' in H18. rewrite tm_morphism_app in H18. assert (hd' = tm_morphism hd''). generalize H20. generalize H18. apply app_eq_length_head. rewrite <- H23 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (a' = tm_morphism a''). generalize H22. generalize H18. apply app_eq_length_head. rewrite <- H24 in H18. apply app_inv_head in H18. rewrite tm_morphism_app in H18. assert (length a' = length (tm_morphism ( firstn (Nat.div2 (length a')) (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step 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 n)))). generalize H25. generalize H18. apply app_eq_length_head. rewrite <- H26 in H18. apply app_inv_head in H18. assert (H'' := H'). rewrite H23 in H''. rewrite H24 in H''. rewrite H18 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 (0 < length a''). unfold a''. rewrite firstn_length_le. destruct (length a'). inversion H15. destruct n0. inversion H14. 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 (length a = 4 * length a''). rewrite H9. rewrite H24. rewrite tm_morphism_length. rewrite tm_morphism_length. lia. assert ( length a'' = 2 ^ Nat.double j \/ length a'' = 3 * 2 ^ Nat.double j ). destruct I. left. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. right. rewrite <- Nat.mul_cancel_l with (p := 4). rewrite <- H28. rewrite Nat.mul_assoc. replace (4*3) with (3*2*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite <- Nat.double_S. assumption. lia. lia. lia. lia. assert (a'' = rev a''). generalize H29. generalize H''. apply IHj. assert (Z := H11). rewrite H24 in H11. rewrite H30 in H11. rewrite <- tm_morphism_twice_rev in H11. rewrite <- H24 in H11. rewrite <- Z in H11. assumption. Qed. Lemma tm_step_square_odd_rev : forall (j n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)) -> a = map negb (rev a). Proof. intros j n hd a tl. intros H I. assert (even (length a) = true). destruct I; rewrite H0; 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 (0 < 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. destruct a. inversion H1. simpl in H4. rewrite app_length in H4. simpl in H4. rewrite Nat.add_succ_r in H4. destruct n. inversion H4. lia. destruct n. inversion H4. 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 H0. generalize H0. generalize H3. generalize H. apply tm_step_morphism4. pose (hd' := firstn (Nat.div2 (length hd)) (tm_step n)). pose (a' := firstn (Nat.div2 (length a)) (skipn (Nat.div2 (length hd)) (tm_step n))). pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step 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 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 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 (length a = 2 * length a'). rewrite tm_morphism_length in H9. assumption. assert (length a' = 2^(Nat.double j) \/ length a' = 3 * 2^(Nat.double j)). destruct I; [left | right]; rewrite <- Nat.mul_cancel_l with (p := 2). rewrite <- tm_morphism_length. rewrite <- H11. rewrite <- Nat.pow_succ_r. assumption. lia. lia. rewrite <- tm_morphism_length. rewrite <- H11. rewrite Nat.mul_assoc. replace (2*3) with (3*2). rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r. assumption. lia. lia. easy. assert (Z := H11). assert (a' = rev a'). generalize H15. generalize H'. apply tm_step_square_even_rev. rewrite H16 in H11. rewrite <- tm_morphism_rev2 in H11. rewrite <- Z in H11. assumption. Qed. Theorem tm_step_square_rev : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). Proof. intros n hd a tl. intros H I. assert (exists k j, length a = S (Nat.double k) * 2^j). apply trailing_zeros; assumption. destruct H0. destruct H0. assert (0 < n). assert (length (tm_step n) = length (tm_step n)). reflexivity. rewrite H in H1 at 2. rewrite app_length in H1. rewrite Nat.add_comm in H1. destruct a. inversion I. simpl in H1. rewrite app_length in H1. simpl in H1. rewrite Nat.add_succ_r in H1. destruct n. inversion H1. lia. destruct n. inversion H1. assert (x = 0 \/ x = 1). generalize H0. generalize H. apply tm_step_square_size. assert (Nat.Even x0 \/ Nat.Odd x0). apply Nat.Even_or_Odd. destruct H3. apply Nat.Even_double in H3. rewrite H3 in H0. assert (length a = 2^(Nat.double (Nat.div2 x0)) \/ length a = 3 * 2^(Nat.double (Nat.div2 x0))). destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia. reflexivity. left. split. generalize H4. generalize H. apply tm_step_square_even_rev. exists (Nat.div2 x0). assumption. apply Nat.Odd_double in H3. rewrite H3 in H0. assert (length a = 2^(S (Nat.double (Nat.div2 x0))) \/ length a = 3 * 2^(S (Nat.double (Nat.div2 x0)))). destruct H2; [left|right]; rewrite H2 in H0; rewrite H0. simpl. lia. reflexivity. right. split. generalize H4. generalize H. apply tm_step_square_odd_rev. exists (Nat.div2 x0). assumption. Qed. Lemma tm_step_square_rev_even : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = rev a -> even m = true. Proof. intros m n hd a tl. intros H I J. assert (0 < length a). rewrite I. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). generalize H0. generalize H. apply tm_step_square_rev. destruct H1. destruct H1. destruct H2. destruct H2. rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2. rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia. rewrite I in H2. assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2. rewrite Nat.log2_pow2 in H3. rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3. rewrite H3 in H2. rewrite Nat.add_succ_r in H2. rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2. rewrite Nat.mul_cancel_r in H2. inversion H2. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. destruct H1. rewrite J in H1 at 1. destruct a. inversion H0. simpl in H1. rewrite map_app in H1. apply app_inj_tail in H1. destruct H1. destruct b. inversion H3. inversion H3. Qed. Lemma tm_step_square_rev_odd : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = map negb (rev a) -> odd m = true. Proof. intros m n hd a tl. intros H I J. assert (0 < length a). rewrite I. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert ( (a = rev a /\ exists j, length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)) \/ (a = map negb (rev a) /\ exists j, length a = 2^(S (Nat.double j)) \/ length a = 3 * 2^(S (Nat.double j)))). generalize H0. generalize H. apply tm_step_square_rev. destruct H1. destruct H1. rewrite J in H1 at 1. destruct a. inversion H0. simpl in H1. rewrite map_app in H1. apply app_inj_tail in H1. destruct H1. destruct b. inversion H3. inversion H3. destruct H1. destruct H2. destruct H2. rewrite I in H2. apply Nat.pow_inj_r in H2. rewrite H2. rewrite Nat.odd_succ. rewrite Nat.double_twice. rewrite Nat.even_mul. reflexivity. lia. rewrite I in H2. assert (Nat.log2 (2^m) = Nat.log2 (2^m)). reflexivity. rewrite H2 in H3 at 2. rewrite Nat.log2_pow2 in H3. rewrite Nat.log2_mul_pow2 in H3. replace (Nat.log2 3) with 1 in H3. rewrite H3 in H2. rewrite Nat.add_succ_r in H2. rewrite Nat.add_0_r in H2. rewrite Nat.pow_succ_r in H2. rewrite Nat.mul_cancel_r in H2. inversion H2. apply Nat.pow_nonzero. easy. lia. reflexivity. lia. lia. lia. Qed. Lemma xxx : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> length a = 2^m -> a = rev a -> length (hd ++ a) mod (2^(S m)) = 0. Proof. intros m n hd a tl. intros H I J. assert (0 < length a). rewrite I. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. assert (even m = true). generalize J. generalize I. generalize H. apply tm_step_square_rev_even. (* TODO: voir s'il faut remplacer la dernière implication par une équivalence *) Abort. Theorem tm_step_palindrome_power2' : forall (m n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl -> length a = 2^m -> 2 < m -> length (hd ++ a) mod 2^ (Nat.double (Nat.div2 (S m))) = 2^ (pred (Nat.double (Nat.div2 (S m)))). Proof. intros m n hd a tl. intros H I J. assert (K: length (hd ++ a) mod 2^ (pred (Nat.double (Nat.div2 (S m)))) = 0). generalize J. generalize I. generalize H. apply tm_step_palindrome_power2. rewrite <- Nat.div_exact in K. assert (L: Nat.Even (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m)))) \/ Nat.Odd (length (hd ++ a) / 2 ^ pred (Nat.double (Nat.div2 (S m))))). apply Nat.Even_or_Odd. destruct L. - assert (length (hd ++ a) mod 2 ^ Nat.double (Nat.div2 (S m)) = 0). rewrite K. apply Nat.Even_double in H0. symmetry in H0. rewrite Nat.double_twice in H0. rewrite <- H0. rewrite Nat.mul_assoc. rewrite Nat.mul_shuffle0. rewrite Nat.mul_comm. rewrite Nat.mul_assoc. rewrite <- Nat.pow_succ_r. rewrite Nat.succ_pred_pos. rewrite Nat.mul_comm. apply Nat.mod_mul. apply Nat.pow_nonzero. easy. assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd. destruct H1. apply Nat.Even_double in H1. rewrite <- H1. apply Nat.lt_0_succ. apply Nat.Odd_double in H1. apply Nat.succ_inj in H1. rewrite <- H1. apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J. assumption. apply Nat.le_0_l. (* on cherche une contradiction à partir de H1 *) assert (Nat.Even (S m) \/ Nat.Odd (S m)). apply Nat.Even_or_Odd. destruct H2. + assert (E := H2). apply Nat.Even_double in H2. rewrite <- H2 in H1. Abort. (* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *) (* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème ET existence d'un palindrome 2 * - *) Lemma tm_step_palindromic_length_8_bis : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ (rev a) ++ tl -> length a = 4 -> ( length (hd ++ a) mod 4 = 0 /\ exists b, a = [b; negb b; negb b; b] ) \/ ( length (hd ++ a) mod 4 = 2 /\ (exists b, a = [b; negb b; b; negb b]) /\ nth_error hd (length hd - 3) <> nth_error tl 2 ). Proof. intros n hd a tl. intros H I. (* proof that length hd++a is even *) assert (P: even (length (hd ++ a)) = true). assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0. generalize H. apply tm_step_palindromic_even_center. assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2). generalize P. apply even_mod4. (* proof that length hd is even *) assert (Q: even (length hd) = true). rewrite app_length in P. rewrite Nat.even_add_even in P. assumption. rewrite I. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity. (* construction de a *) destruct a. inversion I. destruct a. inversion I. destruct a. inversion I. destruct a. inversion I. destruct a. simpl in H. (* proof that b1 <> b2 *) assert ({b1=b2} + {~ b1=b2}). apply bool_dec. destruct H0. replace (hd ++ b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl) with ((hd ++ b :: b0 :: nil) ++ [b1] ++ [b2] ++ [b2] ++ b1 :: b0 :: b :: tl) in H. rewrite e in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. (* proof that n > 2 *) assert (2 < n). assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl) <= length hd + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)). apply Nat.add_le_mono. apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J. rewrite tm_size_power2 in J. destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1. destruct n. inversion J. inversion H1. apply Nat.nle_succ_0 in H3. contradiction H3. destruct n. inversion J. inversion H1. inversion H3. inversion H5. inversion H7. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. (* proof that hd <> nil *) destruct hd. assert (Z: 4 < 2^n). replace 4 with (2^2). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assert (Some b2 = nth_error (tm_step n) 3). rewrite H. reflexivity. replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H1. simpl in H1. assert (Some b2 = nth_error (tm_step n) 4). rewrite H. reflexivity. replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H2. simpl in H2. rewrite H1 in H2. inversion H2. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assert (3 < 4). rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. generalize Z. generalize H2. apply Nat.lt_trans. (* proof that tl <> nil *) destruct tl. assert (Z: 4 < 2^n). replace 4 with (2^2). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assert (Y: tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev. destruct Y; rewrite H in H1 at 2; rewrite rev_app_distr in H1. assert (Some b2 = nth_error (tm_step n) 3). rewrite H1. reflexivity. replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2. simpl in H2. assert (Some b2 = nth_error (tm_step n) 4). rewrite H1. reflexivity. replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3. simpl in H3. rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assert (3 < 4). rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. generalize Z. generalize H3. apply Nat.lt_trans. assert (Some (negb b2) = nth_error (tm_step n) 3). rewrite H1. rewrite nth_error_map. reflexivity. replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2. simpl in H2. assert (Some (negb b2) = nth_error (tm_step n) 4). rewrite H1. rewrite nth_error_map. reflexivity. replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3. simpl in H3. rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. assert (3 < 4). rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. generalize Z. generalize H3. apply Nat.lt_trans. (* FIRST PART OF THE PROOF: case b0 = b1 *) (* première hypothèse b0 = b1 mais alors on construit vers la gauche jusqu'à (lest hd) et l'on a dans l'ordre jusqu'au centre : b1 | (negb b1) b1 | b1 (negb b1 || et les quatre premiers termes vont impliquer que le centre soit en 4n+2 *) assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1. rewrite e in H. (* on a alors b = negb b1 (car dans le même bloc pair on a 01 ou 10 *) assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e0 in H. replace ((b3 :: hd) ++ b1 :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) with ((b3 :: hd) ++ [b1] ++ [b1] ++ [b1] ++ b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. (* à ce stade on a F T | T F || F T T F trois cas : (??? T) | F T T F || F T T F | ??? impossible à gauche (T F) | F T T F || F T T F | (F T) cube (T F) | F T T F || F T T F | (T F) OK, diff + impossible à droite *) rewrite app_removelast_last with (l := b3::hd) (d := false) in H. rewrite <- app_assoc in H. assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}). apply bool_dec. destruct H1. rewrite e0 in H. assert (b2 = b). destruct b2; destruct b1; destruct b. reflexivity. contradiction n0. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. assert (R: b1 = negb b). destruct b; destruct b1; reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity). (* un cas à étudier (??? T) | F T T F || F T T F | ??? impossible à gauche *) destruct M. left. split. assumption. rewrite e. rewrite R. rewrite H1. exists b. reflexivity. (* suite *) rewrite app_removelast_last with (l := b3::hd) (d := false) in Q. rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q. rewrite app_removelast_last with (l := b3::hd) (d := false) in H2. destruct Q. assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H3. assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H4. replace ( removelast (b3 :: hd) ++ [b1] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b4 :: tl ) with ( removelast (b3 :: hd) ++ [b1;b;b1;b1] ++ (b :: b :: b1 :: b1 :: b :: b4 :: tl )) in H. generalize H. apply tm_step_factor4_1mod4. reflexivity. destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1. contradiction n1. reflexivity. rewrite app_length in H2. rewrite app_length in H2. rewrite <- Nat.add_assoc in H2. rewrite <- Nat.add_mod_idemp_l in H2. rewrite H3 in H2. inversion H2. easy. easy. easy. (* Deux cas (T F) | F T T F || F T T F | (F T) cube (T F) | F T T F || F T T F | (T F) impossible à droite *) assert ({b4=b1} + {~ b4=b1}). apply bool_dec. destruct H1. rewrite e0 in H. (* un sous-cas : (T F) | F T T F || F T T F | (T F) impossible à droite *) assert (b2 = b). destruct b2; destruct b1; destruct b. reflexivity. contradiction n0. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. assert (R: b1 = negb b). destruct b; destruct b1; reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity). destruct M. left. split. assumption. (* ici on postule le modulo = 2 *) rewrite e. rewrite R. rewrite H1. exists b. reflexivity. rewrite e in H2. assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3). rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2. reflexivity. easy. replace( removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b1 :: tl ) with ( (((b3 :: hd) ++ [b; b1; b1; b]) ++ [b]) ++ [b1; b1;b;b1] ++ tl) in H. rewrite H1 in H3. assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H3. assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H4. generalize H. apply tm_step_factor4_3mod4. destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1. contradiction n1. reflexivity. symmetry. rewrite app_assoc. rewrite <- app_removelast_last. rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy. (* un sous-cas (T F) | F T T F || F T T F | (F T) cube *) assert (b4 = b). destruct b4; destruct b1; destruct b; reflexivity || contradiction n3 || contradiction n1; reflexivity. rewrite H1 in H. assert (b2 = b). destruct b2; destruct b1; destruct b. reflexivity. contradiction n0. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H. assert (last (b3::hd) false = b). destruct (last (b3::hd) false); destruct b1; destruct b; reflexivity || contradiction n2 || contradiction n1; reflexivity. (* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *) destruct hd. inversion Q. destruct tl. assert (0 < n). apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. apply tm_step_length_even in H4. rewrite H in H4. rewrite app_assoc in H4. rewrite <- app_removelast_last in H4. rewrite app_length in H4. rewrite Nat.even_add in H4. rewrite Q in H4. inversion H4. easy. rewrite H3 in H. rewrite app_removelast_last with (l := removelast (b3::b5::hd)) (d := false) in H. rewrite <- app_assoc in H. (* assigner last (removelast (b3 :: b5 :: hd)) false = b1 b6 = b1 *) assert ({last (removelast (b3 :: b5 :: hd)) false=b} + {~ last (removelast (b3 :: b5 :: hd)) false=b}). apply bool_dec. destruct H4. rewrite e0 in H. replace ( removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl) with ( removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b] ++ [b] ++ b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. assert (last (removelast (b3 :: b5 :: hd)) false = b1). destruct (last (removelast (b3 :: b5 :: hd)) false); destruct b1; destruct b. reflexivity. reflexivity. contradiction n4. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. contradiction n4. reflexivity. reflexivity. reflexivity. rewrite H4 in H. assert ({b6=b} + {~ b6=b}). apply bool_dec. destruct H5. rewrite e0 in H. replace ( removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b :: tl) with ( (removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: nil) ++ [b] ++ [b] ++ [b] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity. assert (b6 = b1). destruct (b6); destruct b1; destruct b; reflexivity || contradiction n5 || contradiction n1; reflexivity. rewrite H5 in H. (* contradiction *) replace ( removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b1 :: tl) with (removelast (removelast (b3 :: b5 :: hd)) ++ [b1;b;b;b1] ++ [b1;b;b;b1] ++ [b1;b;b;b1] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_succ. reflexivity. easy. easy. assert (H' := H). (* SECOND PART PF THE PROOF: case b0 <> b1 *) (* sinon, sur la base de T F T F || F T F T quatre cas : (F T) | T F T F || F T F T | (F T) diff + impossible à droite (F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ? empiriquement : n'apparaît jamais remonter encore d'un cran et prouver la différence à ce stade, TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ? FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ? revoir l'énoncé en fonction (T F) | T F T F || F T F T | (F T) cube (T F) | T F T F || F T F T | (T F) diff + impossible à gauche *) assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e in H. (* assert (b2 = b0). destruct (b2); destruct b1; destruct b0. reflexivity. contradiction n0. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H. *) rewrite app_removelast_last with (l := b3::hd) (d := false) in H. rewrite <- app_assoc in H. assert ({last (b3::hd) false=b0} + {~ last (b3::hd) false=b0}). apply bool_dec. destruct H1. rewrite e0 in H. (* problème à gauche *) destruct M. (* problème avec n1 !!! *) assert (T1: b0 = b1). replace (removelast (b3 :: hd) ++ [b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl) with (((removelast (b3 :: hd) ++ [b0]) ++ [b1; b0; b1; b2; b2]) ++ [b1; b0; b1; b4] ++ tl) in H. assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]). assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1). replace ((b3 :: hd) ++ [b; b0; b1; b2; b2]) with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]). rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity. generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity. generalize H3. generalize H. rewrite e. rewrite <- e0 at 1. rewrite <- app_removelast_last. apply tm_step_factor4_1mod4. easy. inversion T2. inversion H2. reflexivity. rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. rewrite T1 in n1. contradiction n1. reflexivity. (* ici on postule le modulo = 2 *) rewrite app_removelast_last with (l := b3::hd) (d := false) in Q. rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q. destruct Q. assert (exists x, firstn 2 [b0;b1;b0;b1] = [x;x]). generalize H2. assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3. replace ( removelast (b3 :: hd) ++ [b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl ) with ( removelast (b3 :: hd) ++ [b0;b1;b0;b1] ++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H. generalize H. apply tm_step_factor4_1mod4. reflexivity. destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1. contradiction n1. reflexivity. assert (exists x, skipn 2 [b0;b1;b0;b1] = [x;x]). generalize H2. assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3. replace ( removelast (b3 :: hd) ++ [b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl ) with ( removelast (b3 :: hd) ++ [b0;b1;b0;b1] ++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H. generalize H. apply tm_step_factor4_3mod4. reflexivity. destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1. contradiction n1. reflexivity. easy. (* nouveau cas : last (b3 :: hd) false <> b0 (F T) | T F T F || F T F T | (F T) diff + impossible à droite (F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ? *) (* régler d'abord la question du modulo au centre *) destruct M. assert (T1: b0 = b1). replace (removelast (b3 :: hd) ++ [last (b3::hd) false] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl) with (((removelast (b3 :: hd) ++ [last (b3::hd) false]) ++ [b1; b0; b1; b2; b2]) ++ [b1; b0; b1; b4] ++ tl) in H. assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]). assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1). replace ((b3 :: hd) ++ [b; b0; b1; b2; b2]) with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]). rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity. generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity. generalize H3. generalize H. rewrite e. rewrite <- app_removelast_last. apply tm_step_factor4_1mod4. easy. inversion T2. inversion H2. reflexivity. rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. rewrite T1 in n1. contradiction n1. reflexivity. (* on suppose maintenant le modulo = 2 *) assert (last (b3::hd) false = b1). destruct (last (b3::hd) false); destruct b1; destruct b0; reflexivity || contradiction n2 || contradiction n1; reflexivity. assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H. assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]). replace (removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b0 :: tl) with (((b3 :: hd) ++ [b1;b0;b1;b2;b2]) ++ [b1;b0;b1;b0] ++ tl) in H. assert (length ((b3::hd) ++ [b1; b0; b1; b2; b2]) mod 4 = 3). rewrite e in H1. replace ([b1;b0;b1;b2;b2]) with ([b1;b0;b1;b2] ++ [b2]). rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1. reflexivity. easy. reflexivity. assert (length [b1;b0;b1;b0] = 4). reflexivity. generalize H3. generalize H4. generalize H. apply tm_step_factor4_3mod4. symmetry. rewrite app_assoc. rewrite <- app_removelast_last. rewrite <- app_assoc. reflexivity. easy. destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1. contradiction n1. reflexivity. assert (b4 = b1). destruct b4; destruct b1; destruct b0; reflexivity || contradiction n3 || contradiction n1; reflexivity. rewrite H3 in H. rewrite H2 in H. assert (b2 = b0). destruct b2; destruct b1; destruct b0. reflexivity. contradiction n0. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H4 in H. (* dernier cas (difficile (F T) | T F T F || F T F T | (T F) 4n+2 a/rev a/a possible ? remarquer le schéma a ++ (rev a) ++ a apparaît jusqu'à six termes à gauche et à droite empiriquement : n'apparaît jamais avec un 7ème palindromique ajouté remonter encore d'un cran et prouver la différence à ce stade, TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ? FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ? FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???) TFT TFT FF TFT TFT (si on part sur 2 mod 8) (idem en partant de la droite pour 6 mod 8) Le lemme repeating_patterns se base sur les huit premiers termes de TM : [False, True, True, False, True, False, False, True] --> il y a une contradiction à chaque fois *) (* on prouve 3 < n *) assert (R: 2^3 < length (tm_step n)). rewrite H. rewrite app_length. rewrite <- Nat.add_0_l at 1. apply Nat.add_le_lt_mono. apply Nat.le_0_l. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. rewrite tm_size_power2 in R. rewrite <- Nat.pow_lt_mono_r_iff in R. (* on étend hd *) destruct hd. inversion Q. rewrite app_removelast_last with (l := removelast (b3::b5::hd)) (d := false) in H. assert ({last (removelast (b3 :: b5 :: hd)) false = b1} + {~ last (removelast (b3 :: b5 :: hd)) false = b1}). apply bool_dec. destruct H5. rewrite e0 in H. rewrite <- app_assoc in H. replace (b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) with ([b1] ++ b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. reflexivity. (* on étend tl*) destruct tl. assert (tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev. destruct H5; rewrite H in H5 at 2; rewrite rev_app_distr in H5; simpl in H5; assert (odd 0 = true). assert (nth_error (tm_step n) (S (2*0) * 2^0) = nth_error (tm_step n) (pred (S (2*0) * 2^0))). rewrite H5. reflexivity. generalize H6. apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6. assert (nth_error (tm_step n) (S (2*0) * 2^0) = nth_error (tm_step n) (pred (S (2*0) * 2^0))). rewrite H5. reflexivity. generalize H6. apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6. assert ({b6=b1} + {~ b6=b1}). apply bool_dec. destruct H5. rewrite e0 in H. replace ( (removelast (removelast (b3 :: b5 :: hd)) ++ [last (removelast (b3 :: b5 :: hd)) false]) ++ [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b1 :: tl) with ( (removelast (removelast (b3 :: b5 :: hd)) ++ [last (removelast (b3 :: b5 :: hd)) false] ++ [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: nil) ++ [b1] ++ [b1] ++ [b1] ++ tl) in H. apply tm_step_cubefree in H. contradiction H. reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. (* on assigne les valeurs correctes aux deux extrémités *) assert (b6 = b0). destruct b6; destruct b1; destruct b0; reflexivity || contradiction n5 || contradiction n1; reflexivity. rewrite H5 in H. assert (last (removelast (b3 :: b5 :: hd)) false = b0). destruct (last (removelast (b3 :: b5 :: hd)) false); destruct b1; destruct b0; reflexivity || contradiction n4 || contradiction n1; reflexivity. rewrite H6 in H. (* on étend hd *) destruct hd. simpl in H. assert (odd 3 = true). reflexivity. rewrite <- tm_step_pred with (n := n) (k := 0) in H7. rewrite H in H7. simpl in H7. inversion H7. rewrite H9 in n1. contradiction n1. reflexivity. simpl. replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff. assumption. apply Nat.lt_1_2. reflexivity. rewrite app_removelast_last with (l := removelast (removelast (b3::b5::b7::hd))) (d := false) in H. pose (b8 := last (removelast (removelast (b3 :: b5 :: b7 :: hd))) false). fold b8 in H. rewrite <- app_assoc in H. rewrite <- app_assoc in H. pose (hd' := removelast (removelast (removelast (b3 :: b5 :: b7 :: hd)))). fold hd' in H. (* on étend tl *) destruct tl. assert (tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev. destruct H7; rewrite H in H7 at 2; rewrite rev_app_distr in H7; simpl in H5. assert (odd 3 = true). reflexivity. rewrite <- tm_step_pred with (n := n) (k := 0) in H8. rewrite H7 in H8. simpl in H8. inversion H8. rewrite H10 in n1. contradiction n1. reflexivity. simpl. replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff. assumption. apply Nat.lt_1_2. reflexivity. assert (odd 3 = true). reflexivity. rewrite <- tm_step_pred with (n := n) (k := 0) in H8. rewrite H7 in H8. simpl in H8. inversion H8. destruct b0; destruct b1. contradiction n1. reflexivity. inversion H10. inversion H10. contradiction n1. reflexivity. simpl. replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff. assumption. apply Nat.lt_1_2. reflexivity. (* termes à prouver *) (* lemmes initiaux *) assert (Y: forall (k : bool) (x : list bool), length (removelast (k::x)) = length x). intros k x. rewrite removelast_firstn_len. replace (length (k::x)) with (S (length x)). rewrite Nat.pred_succ. rewrite firstn_length. simpl. apply Nat.min_l. apply Nat.le_succ_diag_r. reflexivity. assert (Y': forall (k1 k2 : bool) (x : list bool), length (removelast (removelast (k1::k2::x))) = length x). intros k1 k2 x. rewrite removelast_firstn_len. rewrite Y. replace (length (k2::x)) with (S (length x)). rewrite Nat.pred_succ. rewrite firstn_length. rewrite Y. apply Nat.min_l. apply Nat.le_succ_diag_r. reflexivity. assert (Y'': forall (k1 k2 k3 : bool) (x : list bool), length (removelast (removelast (removelast (k1::k2::k3::x)))) = length x). intros k1 k2 k3 x. rewrite removelast_firstn_len. rewrite removelast_firstn_len. rewrite Y. replace (length (k2::k3::x)) with (S (length (k3::x))). rewrite Nat.pred_succ. rewrite firstn_length. rewrite firstn_length. rewrite Y. rewrite Nat.min_l. rewrite Nat.min_l. reflexivity. apply Nat.le_succ_diag_r. rewrite Nat.min_l. replace (length (k3 :: x)) with (S (length x)). rewrite Nat.pred_succ. apply Nat.le_succ_diag_r. reflexivity. replace (length (k2 :: k3::x)) with (S (length (k3::x))). apply Nat.le_succ_diag_r. reflexivity. reflexivity. (* preuves *) assert (U: nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3) = Some b8). unfold b8. rewrite app_removelast_last with (l := b3::b5::b7::hd) (d := false) at 1. rewrite app_removelast_last with (l := (removelast (b3::b5::b7::hd))) (d := false) at 1. rewrite app_removelast_last with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1. rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2. rewrite Y''. rewrite <- Nat.sub_add_distr. replace (length (b3::b5::b7::hd)) with (3 + length hd). rewrite Nat.sub_diag. reflexivity. reflexivity. rewrite Y''. replace (length (b3::b5::b7::hd)) with (length hd + 3). rewrite Nat.add_sub. apply Nat.le_refl. rewrite Nat.add_comm. reflexivity. assert (0 < length (removelast (removelast (b3 :: b5 :: b7 :: hd)))). rewrite Y'. simpl. apply Nat.lt_0_succ. assert ({removelast (removelast (b3 :: b5 :: b7 :: hd))=nil} + {~ removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}). apply list_eq_dec. apply bool_dec. destruct H8. rewrite e0 in H7. inversion H7. assumption. assert (0 < length (removelast (b3 :: b5 :: b7 :: hd))). rewrite Y. simpl. apply Nat.lt_0_succ. assert ({removelast (b3 :: b5 :: b7 :: hd)=nil} + {~ removelast (b3 :: b5 :: b7 :: hd)=nil}). apply list_eq_dec. apply bool_dec. destruct H8. rewrite e0 in H7. inversion H7. assumption. easy. assert (T: 8 <= length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])). destruct hd. inversion Q. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono. apply Nat.le_0_l. apply Nat.le_refl. (* analyse finale *) assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H. (* premier sous-cas : b8 = b9, contradiction lié à repeating_patterns *) (* lemme initial *) assert (forall n : nat, n mod 4 = 2 -> n mod 8 = 2 \/ n mod 8 = 6). intro m. intro A. assert (m mod (4*2) = m mod 4 + 4 * ((m / 4) mod 2)). apply Nat.mod_mul_r; easy. rewrite A in H7. rewrite <- Nat.bit0_mod in H7. replace (4*2) with 8 in H7. rewrite H7. destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity. reflexivity. pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])). fold lh in H1. fold lh in T. assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H8. rewrite e1 in H. (* si centre = 8n + 2, alors les cinq premiers sont absurdes *) (* si centre = 8n + 6, alors les cinq derniers sont absurdes *) apply H7 in H1. destruct H1. (* on commence par supposer le centre en 8n+2 : hypothèse H1 *) assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy. rewrite H1 in H8. rewrite <- Nat.succ_pred_pos with (n := lh/8) in H8. assert (lh - 8 = 8 * Nat.pred (lh / 8) + 2). rewrite <- Nat.add_cancel_r with (p := 8). rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r. assumption. assumption. assert (nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 3) = nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 4)). rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. rewrite H. rewrite Nat.mul_comm. apply eq_S in H9. symmetry in H9. rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9. rewrite H9. apply eq_S in H9. rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9. rewrite H9. unfold lh. unfold hd'. rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''. rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. reflexivity. apply Nat.le_refl. unfold lh in T. rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm. rewrite app_length in T. assumption. reflexivity. rewrite Y''. rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. apply Nat.le_succ_diag_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity. rewrite Y''. rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. apply Nat.le_refl. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q. simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity. apply Nat.lt_le_incl. assumption. rewrite <- tm_step_repeating_patterns in H10. inversion H10. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. rewrite Nat.mul_lt_mono_pos_l with (p := 8). rewrite Nat.add_lt_mono_r with (p := 2). rewrite <- H9. rewrite Nat.add_lt_mono_r with (p := 8). rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. rewrite <- Nat.add_assoc. replace (2+8) with 10. replace 8 with (2^3) at 1. rewrite <- Nat.pow_add_r. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl. rewrite <- tm_size_power2. rewrite H'. unfold lh. rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc. rewrite <- Nat.add_lt_mono_l. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. apply Nat.le_refl. apply Nat.lt_le_incl. assumption. reflexivity. reflexivity. assumption. apply Nat.lt_0_succ. apply Nat.div_le_mono with (c := 8) in T. rewrite Nat.div_same in T. rewrite Nat.le_succ_l in T. assumption. easy. easy. (* on change de modulo ; on travaille sur 8k+6 maintenant *) (* si centre = 8n + 6, alors les cinq derniers sont absurdes *) assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy. rewrite H1 in H8. rewrite <- Nat.pred_succ with (n := lh/8) in H8. rewrite Nat.mul_pred_r in H8. assert (lh + 8 = 8 * S (lh / 8) + 6). rewrite <- Nat.add_cancel_r with (p := 8) in H8. rewrite <- Nat.add_sub_swap in H8. rewrite Nat.sub_add in H8. assumption. rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.mul_le_mono_l with (p := 8) in H9. rewrite Nat.mul_1_r in H9. assumption. apply Nat.le_0_l. assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. apply Nat.mul_le_mono_l with (p := 8) in H9. rewrite Nat.mul_1_r in H9. assumption. assert (nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 3) = nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 4)). rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9. symmetry in H9. rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9. apply Nat.succ_inj in H9. apply Nat.succ_inj in H9. rewrite Nat.mul_comm in H9. rewrite H9. rewrite Nat.add_succ_r in H9. symmetry in H9. rewrite Nat.add_succ_r in H9. apply Nat.succ_inj in H9. rewrite <- H9. rewrite H. unfold lh. unfold hd'. rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''. rewrite app_length. replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. symmetry. rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity. apply Nat.le_refl. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. apply Nat.le_refl. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. reflexivity. rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. apply Nat.lt_le_incl. assumption. rewrite <- tm_step_repeating_patterns in H10. inversion H10. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. rewrite Nat.mul_lt_mono_pos_l with (p := 8). rewrite Nat.add_lt_mono_r with (p := 6). rewrite <- H9. replace (8) with (2^3) at 2. rewrite <- Nat.pow_add_r. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. rewrite Nat.add_0_l. rewrite <- tm_size_power2. rewrite H'. unfold lh. rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc. rewrite <- Nat.add_assoc. rewrite <- Nat.add_lt_mono_l. simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r. rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r. apply Nat.lt_0_succ. apply Nat.le_refl. apply Nat.lt_le_incl. assumption. reflexivity. apply Nat.lt_0_succ. (* on arrive à la suite du cas b8 = b9 avec cette fois b9 = b1 et non plus b9 = b0 *) assert (b9 = b1). destruct b9; destruct b1; destruct b0. reflexivity. reflexivity. contradiction n6. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. contradiction n6. reflexivity. reflexivity. reflexivity. rewrite H8 in H. (* le premier nouveau sous cas est lh mod 4 = 2 en H1 FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ? c'est un carré ??? c'est un palindrome fait avec un carré de palindrome ? morphisme de FFTTFFTT sans doute impossible (testé) *) unfold hd' in H. destruct hd. inversion P. rewrite app_removelast_last with (l := (removelast (removelast (removelast (b3::b5::b7::b10::hd))))) (d := false) in H. pose (b11 := last (removelast (removelast (removelast (b3 :: b5 :: b7 :: b10 :: hd)))) false). fold b11 in H. rewrite <- app_assoc in H. pose (hd'' := removelast (removelast (removelast (removelast (b3 :: b5 :: b7 :: b10 :: hd))))). fold hd'' in H. (* proof that b11 <> b1 *) assert ({b11=b1} + {~ b11=b1}). apply bool_dec. destruct H9. rewrite e1 in H. assert (even (length hd'') = false). replace ( hd'' ++ [b1] ++ [b1] ++ [b0] ++ [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: tl) with (hd'' ++ [b1;b1;b0] ++ [b1;b1;b0] ++ b1::b0::b0::b1::b0::b1::b1::b0::b1::tl) in H. assert (odd (length [b1;b1;b0]) = true). reflexivity. generalize H9. generalize H. apply tm_step_odd_prefix_square. reflexivity. unfold hd'' in H9. rewrite removelast_firstn_len in H9. rewrite Y'' in H9. rewrite firstn_length_le in H9. simpl in H9. replace (b3::b5::b7::b10::hd) with ([b3;b5;b7;b10] ++ hd) in Q. rewrite app_length in Q. rewrite Nat.even_add in Q. rewrite H9 in Q. inversion Q. reflexivity. rewrite Y''. apply Nat.le_pred_l. (* proof ath b11 = b0 *) assert (b11 = b0). destruct b11; destruct b1; destruct b0. reflexivity. contradiction n7. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n7. reflexivity. reflexivity. rewrite H9 in H. (* on élargit tl (adding b12 in front of tl) *) destruct tl. assert (tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev. destruct H10; rewrite H in H10 at 2; rewrite rev_app_distr in H10; assert (odd 1 = true). reflexivity. rewrite <- tm_step_pred with (n := n) (k := 0) in H11. rewrite H10 in H11. simpl in H11. inversion H11. rewrite H13 in n1. contradiction n1. reflexivity. simpl. replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff. apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption. apply Nat.lt_1_2. reflexivity. reflexivity. rewrite <- tm_step_pred with (n := n) (k := 0) in H11. rewrite H10 in H11. simpl in H11. inversion H11. destruct b0; destruct b1. contradiction n1. reflexivity. inversion H13. inversion H13. contradiction n1. reflexivity. simpl. replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff. apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption. apply Nat.lt_1_2. reflexivity. (* now we have added b12 in front of tl *) (* proof that b12 <> b1 *) assert ({b12=b1} + {~ b12=b1}). apply bool_dec. destruct H10. rewrite e1 in H. assert (even (length (hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])) = false). replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b1 :: tl) with ((hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1]) ++ [ b0;b1;b1] ++ [b0;b1;b1] ++ tl) in H. assert (odd (length [b0;b1;b1]) = true). reflexivity. generalize H10. generalize H. apply tm_step_odd_prefix_square. rewrite <- app_assoc. reflexivity. unfold hd'' in H10. rewrite removelast_firstn_len in H10. rewrite Y'' in H10. rewrite app_length in H10. rewrite firstn_length_le in H10. simpl in H10. rewrite Nat.even_add in H10. simpl in Q. rewrite Q in H10. inversion H10. rewrite Y''. apply Nat.le_pred_l. (* now we know that b12 <> b1 *) (* proof that b12 = b0 *) assert (b12 = b0). destruct b12; destruct b1; destruct b0. reflexivity. contradiction n8. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n8. reflexivity. reflexivity. rewrite H10 in H. (* simplify notations *) replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b0 :: tl) with (hd'' ++ [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0] ++ tl) in H. pose (s := [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0]). fold s in H. assert (even (length hd'') = true). unfold hd''. rewrite removelast_firstn_len. rewrite Y''. replace (pred (length (b10::hd))) with (length hd). rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity. rewrite Y''. apply Nat.le_succ_diag_r. reflexivity. (* destructuring n *) destruct n. inversion H0. rewrite <- tm_step_lemma in H. (* inverting tm_morphism in tm_step n *) assert (hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))). generalize H11. generalize H. apply tm_morphism_app2. assert (s ++ tl = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))). generalize H11. generalize H. apply tm_morphism_app3. symmetry in H13. assert (even (length s) = true). unfold s. reflexivity. assert (s = tm_morphism (firstn (Nat.div2 (length s)) (skipn (Nat.div2 (length hd'')) (tm_step n)))). generalize H14. generalize H13. apply tm_morphism_app2. assert (tl = tm_morphism (skipn (Nat.div2 (length s)) (skipn (Nat.div2 (length hd'')) (tm_step n)))). generalize H14. generalize H13. apply tm_morphism_app3. rewrite H12 in H. rewrite H15 in H. rewrite H16 in H. rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H. pose (h0 := firstn (Nat.div2 (length hd'')) (tm_step n)). pose (s0 := firstn (Nat.div2 (length s)) (skipn (Nat.div2 (length hd'')) (tm_step n))). pose (t0 := skipn (Nat.div2 (length s)) (skipn (Nat.div2 (length hd'')) (tm_step n))). fold h0 in H. fold s0 in H. fold t0 in H. (* fin de la preuve pour cette partie : morphisme impossible *) assert (s0 = [b0;b0;b1;b1;b0;b0;b1;b1]). fold s0 in H15. unfold s in H15. destruct s0. inversion H15. destruct s0. inversion H15. destruct s0. inversion H15. destruct s0. inversion H15. destruct s0; inversion H15. destruct s0. inversion H15. destruct s0. inversion H15. destruct s0. inversion H15. destruct s0; inversion H15. inversion H15. reflexivity. rewrite H17 in H. (* à ce stade H est contradictoire *) assert (even (length h0) = false). replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0) with (h0 ++ [b0] ++ [b0] ++ ([b1; b1; b0; b0; b1; b1] ++ t0)) in H. assert (odd (length [b0]) = true). reflexivity. generalize H18. generalize H. apply tm_step_odd_prefix_square. reflexivity. replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0) with (h0 ++ [b0;b0;b1;b1] ++ [b0;b0;b1;b1] ++ t0) in H. assert (even (length h0) = true). assert (even (length (h0 ++ [b0;b0;b1;b1])) = true). assert (0 < length [b0;b0;b1;b1]). simpl. apply Nat.lt_0_succ. generalize H19. generalize H. apply tm_step_square_pos. rewrite app_length in H19. rewrite Nat.even_add in H19. rewrite H18 in H19. inversion H19. rewrite H18 in H19. inversion H19. reflexivity. reflexivity. rewrite <- length_zero_iff_nil. rewrite Y''. easy. (* fin de la preuve, on a b8 <> b9 *) right. split. assumption. split. rewrite H4. rewrite e. assert (b0 = negb b1). destruct b0; destruct b1. contradiction n1. reflexivity. reflexivity. reflexivity. contradiction n1. reflexivity. rewrite H7. exists b1. reflexivity. rewrite U. simpl. injection. inversion H7. rewrite H9 in n6. contradiction n6. reflexivity. rewrite removelast_firstn_len. rewrite removelast_firstn_len. simpl. rewrite <- length_zero_iff_nil. easy. rewrite <- length_zero_iff_nil. rewrite removelast_firstn_len. easy. apply Nat.lt_1_2. easy. (* désormais on a b <> b1 ; il suffit de montrer que b = b0 pour arriver à un bloc de 2 contenant deux termes identiques *) assert (b = b0). destruct b; destruct b1; destruct b0. reflexivity. contradiction n2. reflexivity. reflexivity. contradiction n1. reflexivity. contradiction n1. reflexivity. reflexivity. contradiction n2. reflexivity. reflexivity. rewrite H1 in H. replace ( (b3 :: hd) ++ b0 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl) with ( (b3 :: hd) ++ [b0] ++ [b0] ++ b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl) in H. assert (even (length (b3 :: hd)) = false). assert (odd (length [b0]) = true). reflexivity. generalize H2. generalize H. apply tm_step_odd_prefix_square. rewrite H2 in Q. inversion Q. reflexivity. (* fin de la destructuration de a, désormais trop grand cf. hypothèse I *) simpl in I. apply eq_add_S in I. apply eq_add_S in I. apply eq_add_S in I. apply eq_add_S in I. symmetry in I. apply O_S in I. contradiction I. Qed.