2023-01-17 11:12:20 -05:00
|
|
|
(** * The Thue-Morse sequence (part 3)
|
|
|
|
|
|
|
|
TODO
|
2023-01-21 09:14:07 -05:00
|
|
|
|
2023-01-26 04:08:29 -05:00
|
|
|
Theorem tm_step_rev : forall (n : nat),
|
|
|
|
Theorem tm_step_palindromic_full : forall (n : nat),
|
|
|
|
Theorem tm_step_palindromic_full_even : forall (n : nat),
|
|
|
|
Theorem tm_step_palindromic_length_12 :
|
2023-01-18 03:45:21 -05:00
|
|
|
*)
|
2023-01-17 11:12:20 -05:00
|
|
|
|
|
|
|
Require Import thue_morse.
|
|
|
|
Require Import thue_morse2.
|
|
|
|
|
|
|
|
Require Import Coq.Lists.List.
|
|
|
|
Require Import PeanoNat.
|
|
|
|
Require Import Nat.
|
|
|
|
Require Import Bool.
|
|
|
|
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
|
2023-01-21 09:14:07 -05:00
|
|
|
Theorem tm_step_rev : forall (n : nat),
|
|
|
|
tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n)).
|
|
|
|
Proof.
|
|
|
|
assert (Z: forall l, map (fun x : bool => negb (negb x)) l = l).
|
|
|
|
intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
|
|
|
|
rewrite IHl. reflexivity.
|
|
|
|
|
|
|
|
intro n. induction n. left. reflexivity.
|
|
|
|
rewrite tm_build. destruct IHn ; [right | left];
|
|
|
|
rewrite rev_app_distr; rewrite H at 1;
|
|
|
|
rewrite H at 2; rewrite <- map_rev.
|
|
|
|
rewrite map_app. rewrite map_map. rewrite Z. reflexivity.
|
|
|
|
rewrite map_map. rewrite Z. reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-01-17 11:12:20 -05:00
|
|
|
Lemma tm_step_palindromic_odd : forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ tl
|
|
|
|
-> a = rev a
|
|
|
|
-> odd (length a) = true
|
2023-01-17 15:07:54 -05:00
|
|
|
-> length a < 4.
|
2023-01-17 11:12:20 -05:00
|
|
|
Proof.
|
2023-01-17 15:07:54 -05:00
|
|
|
(* end of the lemma *)
|
|
|
|
assert (LEMMA: forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ tl
|
|
|
|
-> a = rev a
|
|
|
|
-> odd (length a) = true
|
|
|
|
-> length a <> 5).
|
2023-01-17 11:12:20 -05:00
|
|
|
intros n hd a tl. intros H I J.
|
|
|
|
destruct a. easy. destruct a. easy.
|
|
|
|
destruct a. easy. destruct a. easy.
|
|
|
|
destruct a. easy.
|
|
|
|
|
|
|
|
destruct a. (* case of length 5 *)
|
|
|
|
assert (exists (u v : list bool) (d: bool),
|
|
|
|
b::b0::b1::b2::b3::nil = u ++ [d;d] ++ v).
|
|
|
|
assert (4 < length (b::b0::b1::b2::b3::nil)). 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. generalize H0. generalize H.
|
|
|
|
apply tm_step_consecutive_identical_length.
|
|
|
|
|
|
|
|
destruct H0. destruct H0. destruct H0.
|
|
|
|
|
|
|
|
assert (K: {b=b0} + {~ b=b0}). apply bool_dec.
|
|
|
|
assert (L: {b0=b1} + {~ b0=b1}). apply bool_dec.
|
|
|
|
assert (M: {b1=b2} + {~ b1=b2}). apply bool_dec.
|
|
|
|
assert (N: {b2=b3} + {~ b2=b3}). apply bool_dec.
|
|
|
|
|
|
|
|
destruct K. rewrite e in H. rewrite e in I.
|
|
|
|
destruct N. rewrite e0 in H.
|
|
|
|
replace ([b0;b0;b1;b3;b3] ++ tl) with ([b0;b0] ++ [b1] ++ [b3;b3] ++ tl) in H.
|
|
|
|
apply tm_step_consecutive_identical' in H. inversion H. reflexivity.
|
|
|
|
inversion I. rewrite H3 in n0. contradiction n0.
|
|
|
|
|
|
|
|
destruct L. rewrite e in H. rewrite e in I.
|
|
|
|
destruct M. rewrite <- e0 in H.
|
|
|
|
replace (hd ++ [b; b1; b1; b1; b3] ++ tl)
|
|
|
|
with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b1] ++ ([b3] ++ tl)) in H.
|
|
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_succ. rewrite <- app_assoc. simpl. reflexivity.
|
2023-01-18 03:45:21 -05:00
|
|
|
|
2023-01-17 11:12:20 -05:00
|
|
|
inversion I. rewrite H3 in n1. contradiction n1.
|
|
|
|
|
|
|
|
destruct M. rewrite <- e in I. inversion I.
|
|
|
|
rewrite H3 in n1. contradiction n1.
|
|
|
|
destruct N. rewrite e in I. inversion I.
|
|
|
|
rewrite H2 in n0. rewrite H3 in n0. contradiction n0.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H2 in n0. rewrite H3 in n0. contradiction n0.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H3 in n1. rewrite H4 in n1. contradiction n1.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H4 in n2. rewrite H5 in n2. contradiction n2.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
destruct x. inversion H0.
|
|
|
|
rewrite H5 in n3. rewrite H6 in n3. contradiction n3.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
assert (length [b;b0;b1;b2;b3] = length [b;b0;b1;b2;b3]).
|
|
|
|
reflexivity. rewrite H0 in H1 at 2. simpl in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply Nat.succ_inj in H1.
|
|
|
|
rewrite app_length in H1. simpl in H1.
|
|
|
|
rewrite Nat.add_succ_r in H1. rewrite Nat.add_succ_r in H1.
|
|
|
|
apply Nat.succ_inj in H1. apply O_S in H1. contradiction H1.
|
|
|
|
|
|
|
|
simpl. apply not_eq_S. apply not_eq_S. apply not_eq_S.
|
|
|
|
apply not_eq_S. apply not_eq_S. apply Nat.neq_succ_0.
|
2023-01-17 15:07:54 -05:00
|
|
|
(* end of the lemma *)
|
2023-01-17 11:12:20 -05:00
|
|
|
|
|
|
|
intros n hd a tl. intros H I J.
|
|
|
|
|
|
|
|
assert (length a <= 5 \/ 5 < length a). apply Nat.le_gt_cases.
|
|
|
|
destruct H0.
|
|
|
|
apply Nat.lt_eq_cases in H0. destruct H0.
|
|
|
|
rewrite Nat.lt_succ_r in H0.
|
|
|
|
apply Nat.lt_eq_cases in H0. destruct H0. assumption.
|
|
|
|
rewrite H0 in J. inversion J.
|
|
|
|
assert (length a <> 5). generalize J. generalize I. generalize H.
|
2023-01-17 15:07:54 -05:00
|
|
|
apply LEMMA. rewrite H0 in H1. contradiction H1.
|
2023-01-17 11:12:20 -05:00
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
(* main part of the proof:
|
|
|
|
each odd palindromic factor greater than 5
|
|
|
|
contains a palindromic subfactor of length 5 *)
|
2023-01-17 12:59:33 -05:00
|
|
|
pose (t := length a - 5). assert (Nat.even t = true).
|
|
|
|
unfold t. rewrite Nat.even_sub. rewrite <- Nat.negb_odd.
|
|
|
|
rewrite J. reflexivity. generalize H0.
|
|
|
|
apply Nat.lt_le_incl.
|
|
|
|
|
|
|
|
pose (u := firstn (Nat.div2 t) a).
|
|
|
|
pose (v := firstn 5 (skipn (Nat.div2 t) a)).
|
|
|
|
pose (w := skipn (Nat.div2 t + 5) a).
|
|
|
|
|
|
|
|
assert (a = u ++ v ++ w).
|
|
|
|
unfold u. unfold v. unfold w.
|
|
|
|
rewrite firstn_skipn_comm.
|
|
|
|
replace (Nat.div2 t) with (min (Nat.div2 t) (Nat.div2 t + 5)) at 1.
|
|
|
|
rewrite <- firstn_firstn. rewrite app_assoc. rewrite firstn_skipn.
|
|
|
|
rewrite firstn_skipn. reflexivity.
|
|
|
|
apply Nat.min_l. rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_le_mono_l. apply le_0_n.
|
|
|
|
|
|
|
|
assert (Nat.Even (length a - 5)).
|
|
|
|
apply Nat.EvenT_Even. apply Nat.even_EvenT. rewrite Nat.even_sub.
|
|
|
|
rewrite <- Nat.negb_odd. rewrite J. reflexivity.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
|
|
|
|
assert (length v = 5). unfold v. apply firstn_length_le.
|
|
|
|
rewrite skipn_length. unfold t.
|
|
|
|
rewrite Nat.mul_le_mono_pos_l with (p := 2).
|
|
|
|
rewrite Nat.mul_sub_distr_l.
|
|
|
|
replace (2 * Nat.div2 (length a - 5))
|
|
|
|
with (Nat.double (Nat.div2 (length a - 5))).
|
|
|
|
rewrite <- Nat.Even_double.
|
|
|
|
|
|
|
|
replace (2 * length a) with ((length a + 5) + (length a - 5)).
|
|
|
|
rewrite Nat.add_sub. replace (2*5) with (5+5).
|
|
|
|
apply Nat.add_le_mono_r. apply Nat.lt_le_incl. assumption.
|
|
|
|
reflexivity. rewrite <- Nat.add_assoc.
|
|
|
|
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
|
|
|
|
rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
|
|
assumption. assumption.
|
|
|
|
apply Nat.double_twice. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
assert (length u = length w). unfold u. unfold w.
|
|
|
|
rewrite firstn_length. rewrite skipn_length. rewrite Nat.min_l.
|
|
|
|
unfold t. rewrite <- Nat.mul_cancel_l with (p := 2).
|
|
|
|
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
|
|
|
|
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_add_distr_l.
|
|
|
|
rewrite <- Nat.double_twice. rewrite <- Nat.double_twice.
|
|
|
|
rewrite <- Nat.Even_double. rewrite Nat.double_twice.
|
|
|
|
rewrite <- Nat.add_sub_swap. rewrite <- Nat.add_sub_assoc.
|
|
|
|
replace (2 * length a) with ((length a - 5) + (length a + 5)).
|
|
|
|
simpl. rewrite Nat.add_sub. reflexivity.
|
|
|
|
rewrite Nat.add_comm. rewrite <- Nat.add_assoc.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
|
|
|
|
rewrite Nat.add_0_r. reflexivity. apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
|
|
assumption. simpl. apply le_n_S. apply le_n_S. apply le_n_S. apply le_n_S.
|
|
|
|
apply le_n_S. apply le_0_n. apply Nat.lt_le_incl. assumption.
|
|
|
|
assumption. assumption. easy.
|
|
|
|
unfold t.
|
|
|
|
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
|
|
|
|
rewrite <- Nat.Even_double. simpl. rewrite Nat.add_0_r.
|
|
|
|
rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono.
|
|
|
|
apply Nat.le_sub_l. apply le_0_n. assumption. apply Nat.lt_0_2.
|
|
|
|
|
|
|
|
assert (v = rev v). rewrite H2 in I.
|
2023-01-18 03:45:21 -05:00
|
|
|
rewrite rev_app_distr in I. rewrite rev_app_distr in I.
|
2023-01-17 12:59:33 -05:00
|
|
|
rewrite <- app_assoc in I.
|
|
|
|
|
|
|
|
assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
|
2023-01-19 01:17:53 -05:00
|
|
|
generalize I. apply app_eq_length_head.
|
|
|
|
rewrite H6 in I. rewrite rev_involutive in I.
|
2023-01-17 12:59:33 -05:00
|
|
|
apply app_inv_head in I. apply app_inv_tail in I. assumption.
|
|
|
|
|
|
|
|
assert (length v <> 5).
|
|
|
|
assert (odd (length v) = true). rewrite H4. reflexivity.
|
|
|
|
generalize H7. generalize H6. generalize H. rewrite H2.
|
|
|
|
rewrite <- app_assoc. rewrite <- app_assoc. rewrite app_assoc.
|
2023-01-17 15:07:54 -05:00
|
|
|
apply LEMMA. rewrite H4 in H7. contradiction H7.
|
2023-01-17 12:59:33 -05:00
|
|
|
reflexivity.
|
|
|
|
Qed.
|
2023-01-18 03:45:21 -05:00
|
|
|
|
2023-01-28 05:54:52 -05:00
|
|
|
Theorem tm_step_palindromic_even_center :
|
2023-01-18 03:45:21 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 0 < length a
|
|
|
|
-> even (length (hd ++ a)) = true.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
assert (J: a = removelast a ++ [ last a false ]).
|
|
|
|
apply app_removelast_last.
|
|
|
|
assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct K. rewrite e in I. inversion I. assumption.
|
|
|
|
rewrite J in H. rewrite rev_app_distr in H.
|
|
|
|
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
|
|
rewrite app_assoc in H.
|
|
|
|
replace
|
|
|
|
([last a false] ++ rev [last a false] ++ rev (removelast a) ++ tl)
|
|
|
|
with ([last a false; last a false] ++ (rev (removelast a) ++ tl)) in H.
|
|
|
|
apply tm_step_consecutive_identical in H. rewrite J.
|
|
|
|
rewrite app_assoc. rewrite app_length. rewrite Nat.even_add.
|
|
|
|
rewrite <- Nat.negb_odd. rewrite H. reflexivity.
|
|
|
|
reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
2023-01-18 06:24:21 -05:00
|
|
|
Lemma tm_step_palindromic_even_center' :
|
|
|
|
forall (n k m: nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 0 < length a
|
|
|
|
-> length (hd ++ a) = S (2 * k) * 2^m
|
|
|
|
-> odd m = true.
|
|
|
|
Proof.
|
|
|
|
intros n k m hd a tl. intros H I J.
|
|
|
|
assert (Z := H).
|
|
|
|
assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec.
|
|
|
|
destruct K. rewrite e in I. inversion I.
|
|
|
|
assert (L: a = removelast a ++ [ last a false ]).
|
|
|
|
apply app_removelast_last. assumption.
|
|
|
|
rewrite L in H. rewrite rev_app_distr in H.
|
|
|
|
assert (nth_error (tm_step n) (length (hd++a))
|
|
|
|
= nth_error (tm_step n) (pred (length (hd++a)))).
|
|
|
|
rewrite H.
|
|
|
|
rewrite app_assoc. rewrite nth_error_app2.
|
|
|
|
symmetry. rewrite <- app_assoc. rewrite <- app_assoc.
|
|
|
|
rewrite app_assoc. rewrite nth_error_app2.
|
|
|
|
rewrite <- app_removelast_last. rewrite Nat.sub_diag.
|
|
|
|
replace (hd++a) with ((hd ++ removelast a) ++ [last a false]).
|
|
|
|
rewrite app_length. rewrite Nat.add_1_r. rewrite <- pred_Sn.
|
|
|
|
rewrite Nat.sub_diag. reflexivity. rewrite L at 3.
|
|
|
|
rewrite <- app_assoc. reflexivity. assumption.
|
|
|
|
|
|
|
|
rewrite L at 2. rewrite app_assoc.
|
|
|
|
replace (length ((hd ++ removelast a) ++ [last a false]))
|
|
|
|
with (length (hd ++ removelast a) + length [last a false]).
|
|
|
|
rewrite Nat.add_1_r. rewrite <- pred_Sn. apply Nat.le_refl.
|
|
|
|
|
|
|
|
symmetry. rewrite app_length. reflexivity.
|
|
|
|
rewrite <- app_removelast_last. apply Nat.le_refl.
|
|
|
|
assumption.
|
|
|
|
|
|
|
|
generalize H0. rewrite J. apply tm_step_pred.
|
|
|
|
|
|
|
|
rewrite <- J. rewrite <- tm_size_power2. rewrite Z.
|
|
|
|
rewrite app_length. rewrite app_length.
|
|
|
|
apply Nat.add_lt_mono_l. rewrite app_length.
|
|
|
|
rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_lt_mono_l. rewrite app_length. rewrite rev_length.
|
|
|
|
assert (0 <= length tl). apply le_0_n. rewrite <- Nat.add_0_r at 1.
|
|
|
|
apply Nat.add_lt_le_mono; assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-01-19 02:48:12 -05:00
|
|
|
Theorem tm_step_palindromic_full : forall (n : nat),
|
|
|
|
odd n = true -> tm_step (S n) = (tm_step n) ++ rev (tm_step n).
|
|
|
|
Proof.
|
|
|
|
intro n. intro H.
|
|
|
|
apply Nat.odd_OddT in H. apply Nat.OddT_Odd in H.
|
|
|
|
apply Nat.Odd_double in H. rewrite H. rewrite tm_step_odd_step.
|
|
|
|
rewrite <- tm_build. reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
2023-01-19 02:57:46 -05:00
|
|
|
(* very close to the previous one but we add the case n=0 here *)
|
|
|
|
Theorem tm_step_palindromic_full_even : forall (n : nat),
|
|
|
|
even n = true -> tm_step n = rev (tm_step n).
|
|
|
|
Proof.
|
|
|
|
intro n. intro H. destruct n. reflexivity.
|
|
|
|
rewrite Nat.even_succ in H. apply tm_step_palindromic_full in H.
|
|
|
|
rewrite H. rewrite rev_app_distr. rewrite rev_involutive.
|
|
|
|
reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
2023-01-19 15:56:10 -05:00
|
|
|
|
2023-01-21 09:14:07 -05:00
|
|
|
(**
|
|
|
|
In this notebook I call "proper palindrome" in the Thue-Morse sequence,
|
|
|
|
any palindromic subsequence such that the middle (of the palindromic
|
|
|
|
subsequence) is not also the middle of a wider palindromic subsequence.
|
|
|
|
In ther words, a proper palindrome can not be enlarged by adding more
|
|
|
|
termes on both sides.
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
2023-01-21 15:55:04 -05:00
|
|
|
(* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *)
|
2023-01-22 02:16:44 -05:00
|
|
|
(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème
|
|
|
|
ET existence d'un palindrome 2 * - *)
|
2023-01-21 09:14:07 -05:00
|
|
|
Lemma tm_step_palindromic_length_8 :
|
2023-01-20 03:56:23 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
2023-01-21 09:14:07 -05:00
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> length a = 4
|
2023-01-22 03:13:36 -05:00
|
|
|
-> length (hd ++ a) mod 4 = 0
|
|
|
|
\/ nth_error hd (length hd - 3) <> nth_error tl 2.
|
2023-01-20 03:56:23 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
|
2023-01-21 09:14:07 -05:00
|
|
|
(* 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.
|
|
|
|
|
2023-01-21 12:14:50 -05:00
|
|
|
assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2).
|
|
|
|
generalize P. apply even_mod4.
|
|
|
|
|
2023-01-21 09:14:07 -05:00
|
|
|
(* 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 le_0_n. 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.
|
2023-01-20 03:56:23 -05:00
|
|
|
|
2023-01-21 09:14:07 -05:00
|
|
|
(* 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.
|
|
|
|
|
2023-01-21 13:43:33 -05:00
|
|
|
(* FIRST PART OF THE PROOF: case b0 = b1 *)
|
2023-01-21 09:14:07 -05:00
|
|
|
(* 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.
|
2023-01-20 03:56:23 -05:00
|
|
|
|
2023-01-21 12:14:50 -05:00
|
|
|
(* à 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.
|
|
|
|
(* un cas à étudier
|
|
|
|
(??? T) | F T T F || F T T F | ??? impossible à gauche
|
|
|
|
*)
|
|
|
|
destruct M. left. assumption. (* 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.
|
|
|
|
rewrite app_removelast_last with (l := b3::hd) (d := false) in H1.
|
|
|
|
destruct Q.
|
|
|
|
assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H2.
|
|
|
|
assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H3.
|
|
|
|
replace (
|
|
|
|
removelast (b3 :: hd) ++
|
|
|
|
[b1] ++ b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )
|
|
|
|
with (
|
|
|
|
removelast (b3 :: hd) ++ [b1;b;b1;b1]
|
|
|
|
++ (b2 :: b2 :: b1 :: b1 :: b :: 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.
|
|
|
|
|
|
|
|
rewrite app_length in H1. rewrite app_length in H1.
|
|
|
|
rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
|
|
|
|
rewrite H2 in H1. inversion H1. 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
|
|
|
|
*)
|
2023-01-21 12:54:32 -05:00
|
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
|
|
|
|
rewrite e in H1.
|
|
|
|
assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
|
|
|
|
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1.
|
|
|
|
reflexivity. easy.
|
|
|
|
|
|
|
|
replace(
|
|
|
|
removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
|
|
|
|
b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b1 :: tl )
|
|
|
|
with (
|
|
|
|
(((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) ++ [b1; b1;b;b1] ++ tl) in H.
|
|
|
|
|
|
|
|
assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H2.
|
|
|
|
assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H3.
|
|
|
|
generalize H. apply tm_step_factor4_3mod4.
|
|
|
|
destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 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. reflexivity. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
reflexivity. contradiction n3. reflexivity. 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. reflexivity. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
2023-01-21 13:38:07 -05:00
|
|
|
reflexivity. contradiction n2. reflexivity. reflexivity.
|
|
|
|
|
|
|
|
(* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
|
|
|
|
destruct hd. inversion Q. destruct tl.
|
2023-01-22 04:06:55 -05:00
|
|
|
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.
|
2023-01-21 13:38:07 -05:00
|
|
|
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. reflexivity. contradiction n5. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
contradiction n5. reflexivity. reflexivity. 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.
|
|
|
|
|
2023-01-22 16:36:48 -05:00
|
|
|
assert (H' := H).
|
|
|
|
|
2023-01-21 13:43:33 -05:00
|
|
|
(* SECOND PART PF THE PROOF: case b0 <> b1 *)
|
2023-01-21 13:49:26 -05:00
|
|
|
(* 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.
|
2023-01-21 14:41:23 -05:00
|
|
|
(*
|
2023-01-21 13:49:26 -05:00
|
|
|
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.
|
2023-01-21 14:41:23 -05:00
|
|
|
*)
|
2023-01-21 13:49:26 -05:00
|
|
|
|
2023-01-21 14:41:23 -05:00
|
|
|
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.
|
2023-01-21 13:38:07 -05:00
|
|
|
|
2023-01-21 14:41:23 -05:00
|
|
|
(* problème à gauche *)
|
|
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
2023-01-21 13:38:07 -05:00
|
|
|
|
2023-01-21 14:41:23 -05:00
|
|
|
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 ?
|
|
|
|
*)
|
2023-01-21 14:48:33 -05:00
|
|
|
(* régler d'abord la question du modulo au centre *)
|
|
|
|
destruct M. left. assumption. (* ici on postule le modulo = 2 *)
|
|
|
|
|
2023-01-21 15:11:47 -05:00
|
|
|
assert (last (b3::hd) false = b1).
|
|
|
|
destruct (last (b3::hd) false); destruct b1; destruct b0.
|
|
|
|
reflexivity. reflexivity. contradiction n2. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
contradiction n2. reflexivity. reflexivity. 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]).
|
2023-01-21 14:48:33 -05:00
|
|
|
replace (removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
|
|
|
|
b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b0 :: tl)
|
2023-01-21 15:11:47 -05:00
|
|
|
with (((b3 :: hd) ++ [b1;b0;b1;b2;b2])
|
2023-01-21 14:48:33 -05:00
|
|
|
++ [b1;b0;b1;b0] ++ tl) in H.
|
2023-01-21 15:11:47 -05:00
|
|
|
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.
|
2023-01-21 12:54:32 -05:00
|
|
|
|
2023-01-21 15:11:47 -05:00
|
|
|
assert (b4 = b1). destruct b4; destruct b1; destruct b0.
|
|
|
|
reflexivity. reflexivity. contradiction n3. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
contradiction n3. reflexivity. reflexivity. reflexivity.
|
|
|
|
rewrite H3 in H. rewrite H2 in H.
|
2023-01-21 12:54:32 -05:00
|
|
|
|
2023-01-21 15:55:04 -05:00
|
|
|
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.
|
2023-01-21 12:54:32 -05:00
|
|
|
|
2023-01-21 15:55:04 -05:00
|
|
|
(* 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 ?
|
2023-01-22 02:16:44 -05:00
|
|
|
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
|
2023-01-22 04:06:55 -05:00
|
|
|
*)
|
2023-01-21 12:14:50 -05:00
|
|
|
|
2023-01-22 09:17:52 -05:00
|
|
|
(* 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.
|
|
|
|
|
2023-01-22 04:06:55 -05:00
|
|
|
(* on étend hd *)
|
|
|
|
destruct hd. inversion Q.
|
2023-01-22 08:17:44 -05:00
|
|
|
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.
|
2023-01-22 04:06:55 -05:00
|
|
|
|
|
|
|
(* on étend tl*)
|
|
|
|
destruct tl.
|
|
|
|
assert (tm_step n = rev (tm_step n)
|
|
|
|
\/ tm_step n = map negb (rev (tm_step n))).
|
2023-01-22 04:15:31 -05:00
|
|
|
apply tm_step_rev. destruct H5; rewrite H in H5 at 2;
|
|
|
|
rewrite rev_app_distr in H5; simpl in H5;
|
2023-01-22 04:06:55 -05:00
|
|
|
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.
|
2023-01-22 04:15:31 -05:00
|
|
|
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.
|
2023-01-22 08:17:44 -05:00
|
|
|
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.
|
2023-01-21 12:14:50 -05:00
|
|
|
|
2023-01-22 08:40:53 -05:00
|
|
|
(* on assigne les valeurs correctes aux deux extrémités *)
|
2023-01-22 08:17:44 -05:00
|
|
|
assert (b6 = b0). destruct b6; destruct b1; destruct b0.
|
|
|
|
reflexivity. contradiction n5. reflexivity. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
reflexivity. contradiction n5. reflexivity. 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. reflexivity. reflexivity.
|
|
|
|
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
|
|
|
reflexivity. contradiction n4. reflexivity. reflexivity.
|
|
|
|
rewrite H6 in H.
|
|
|
|
|
2023-01-22 08:40:53 -05:00
|
|
|
(* 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.
|
2023-01-22 09:17:52 -05:00
|
|
|
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).
|
2023-01-22 09:38:57 -05:00
|
|
|
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.
|
2023-01-22 09:17:52 -05:00
|
|
|
|
2023-01-22 09:38:57 -05:00
|
|
|
(* 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.
|
2023-01-22 09:17:52 -05:00
|
|
|
|
2023-01-22 09:48:06 -05:00
|
|
|
(* termes à prouver *)
|
2023-01-22 11:41:51 -05:00
|
|
|
(* lemmes initiaux *)
|
|
|
|
assert (Y: forall (k : bool) (x : list bool),
|
2023-01-22 10:33:37 -05:00
|
|
|
length (removelast (k::x)) = length x).
|
2023-01-22 11:41:51 -05:00
|
|
|
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 *)
|
2023-01-22 09:48:06 -05:00
|
|
|
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.
|
2023-01-22 11:41:51 -05:00
|
|
|
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.
|
2023-01-22 08:40:53 -05:00
|
|
|
|
2023-01-22 14:44:35 -05:00
|
|
|
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.
|
2023-01-22 14:17:38 -05:00
|
|
|
|
2023-01-22 13:19:39 -05:00
|
|
|
(* inutile
|
2023-01-22 11:45:16 -05:00
|
|
|
assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
|
2023-01-22 13:19:39 -05:00
|
|
|
*)
|
|
|
|
|
|
|
|
(* 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 *)
|
2023-01-22 13:35:41 -05:00
|
|
|
(* 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.
|
2023-01-22 14:17:38 -05:00
|
|
|
pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
|
2023-01-22 14:44:35 -05:00
|
|
|
fold lh in H1. fold lh in T.
|
2023-01-22 13:19:39 -05:00
|
|
|
|
2023-01-22 13:35:41 -05:00
|
|
|
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 *)
|
2023-01-22 14:17:38 -05:00
|
|
|
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.
|
2023-01-22 14:44:35 -05:00
|
|
|
assumption. assumption.
|
2023-01-22 11:41:51 -05:00
|
|
|
|
2023-01-22 14:44:35 -05:00
|
|
|
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.
|
2023-01-22 15:03:18 -05:00
|
|
|
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.
|
2023-01-22 15:29:01 -05:00
|
|
|
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''.
|
2023-01-22 15:36:25 -05:00
|
|
|
rewrite app_length.
|
2023-01-22 15:29:01 -05:00
|
|
|
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).
|
2023-01-22 15:36:25 -05:00
|
|
|
rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
|
|
|
|
simpl. apply le_n_S. apply le_0_n. 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 le_0_n. reflexivity. reflexivity.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
2023-01-22 15:48:19 -05:00
|
|
|
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.
|
2023-01-22 15:36:25 -05:00
|
|
|
|
2023-01-22 16:28:24 -05:00
|
|
|
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.
|
2023-01-22 16:36:48 -05:00
|
|
|
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.
|
2023-01-22 16:42:58 -05:00
|
|
|
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 *)
|
2023-01-23 12:40:17 -05:00
|
|
|
(* 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 le_0_n.
|
|
|
|
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 le_0_n. apply Nat.le_refl.
|
|
|
|
rewrite <- Nat.add_0_r at 1.
|
|
|
|
rewrite <- Nat.add_le_mono_l. apply le_0_n. 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 le_0_n.
|
|
|
|
|
|
|
|
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 le_0_n.
|
|
|
|
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é ???
|
2023-01-23 14:11:13 -05:00
|
|
|
c'est un palindrome fait avec un carré de palindrome ?
|
|
|
|
morphisme de FFTTFFTT sans doute impossible (testé)
|
2023-01-23 12:40:17 -05:00
|
|
|
*)
|
2023-01-23 14:11:13 -05:00
|
|
|
|
|
|
|
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.
|
|
|
|
|
2023-01-23 14:35:41 -05:00
|
|
|
(* 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.
|
2023-01-23 14:11:13 -05:00
|
|
|
|
2023-01-23 14:35:41 -05:00
|
|
|
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 *)
|
2023-01-23 15:01:27 -05:00
|
|
|
(* 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 *)
|
2023-01-23 15:10:50 -05:00
|
|
|
(* 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.
|
2023-01-23 15:01:27 -05:00
|
|
|
|
2023-01-23 15:43:16 -05:00
|
|
|
(* 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.
|
|
|
|
|
2023-01-23 15:56:54 -05:00
|
|
|
(* 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.
|
2023-01-23 15:43:16 -05:00
|
|
|
|
2023-01-23 16:22:56 -05:00
|
|
|
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.
|
2023-01-23 15:43:16 -05:00
|
|
|
|
2023-01-23 16:59:11 -05:00
|
|
|
(* à 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. 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.
|
2023-01-23 15:43:16 -05:00
|
|
|
|
2023-01-23 16:59:11 -05:00
|
|
|
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.
|
2023-01-21 09:14:07 -05:00
|
|
|
|
2023-01-23 16:59:11 -05:00
|
|
|
(* fin de la destructuration de a, désormais trop grand
|
|
|
|
cf. hypothèse I *)
|
2023-01-23 17:00:55 -05:00
|
|
|
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.
|
2023-01-21 09:14:07 -05:00
|
|
|
|
|
|
|
|
2023-01-26 04:08:29 -05:00
|
|
|
Theorem tm_step_palindromic_length_12 :
|
2023-01-22 02:16:44 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ rev a ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length (hd ++ a) mod 4 = 0.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
assert (J: even (length (hd ++ a)) = true).
|
|
|
|
assert (0 < length a).
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
assumption. generalize H0. generalize H.
|
|
|
|
apply tm_step_palindromic_even_center.
|
|
|
|
apply even_mod4 in J. destruct J. assumption.
|
|
|
|
|
|
|
|
rewrite <- firstn_skipn with (l := a) (n := length a - 4) in H.
|
|
|
|
rewrite rev_app_distr in H. rewrite <- app_assoc in H.
|
|
|
|
rewrite app_assoc in H.
|
|
|
|
assert (length (skipn (length a - 4) a) = 4). rewrite skipn_length.
|
|
|
|
replace (length a) with ((length a - 4) + 4) at 1. rewrite Nat.add_comm.
|
|
|
|
rewrite Nat.add_sub. reflexivity. rewrite Nat.add_comm.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. reflexivity.
|
|
|
|
apply Nat.le_refl. apply Nat.lt_le_incl.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
assumption.
|
|
|
|
|
|
|
|
pose (hd' := hd ++ firstn (length a - 4) a). fold hd' in H.
|
|
|
|
pose (a' := skipn (length a - 4) a). fold a' in H.
|
|
|
|
rewrite <- app_assoc in H.
|
|
|
|
pose (tl' := rev (firstn (length a - 4) a) ++ tl). fold tl' in H.
|
|
|
|
|
|
|
|
assert (K: length (hd' ++ a') mod 4 = 0
|
2023-01-22 03:13:36 -05:00
|
|
|
\/ nth_error hd' (length hd' - 3) <> nth_error tl' 2).
|
2023-01-22 02:16:44 -05:00
|
|
|
fold a' in H1. generalize H1. generalize H.
|
|
|
|
apply tm_step_palindromic_length_8.
|
|
|
|
destruct K.
|
2023-01-22 03:13:36 -05:00
|
|
|
unfold hd' in H2. unfold a' in H2. rewrite <- app_assoc in H2.
|
|
|
|
rewrite firstn_skipn in H2. assumption.
|
|
|
|
|
|
|
|
rewrite <- firstn_skipn with (l := a) (n := length a - 4) in I.
|
|
|
|
rewrite app_length in I. rewrite H1 in I. rewrite Nat.add_comm in I.
|
|
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
|
|
|
|
|
|
destruct (firstn (length a - 4) a). inversion I. destruct l.
|
|
|
|
apply Nat.succ_lt_mono in I. inversion I. destruct l.
|
|
|
|
apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I.
|
|
|
|
inversion I.
|
|
|
|
|
|
|
|
unfold hd' in H2. unfold tl' in H2.
|
|
|
|
rewrite nth_error_app2 in H2. rewrite nth_error_app1 in H2.
|
|
|
|
rewrite app_length in H2. rewrite Nat.add_comm in H2.
|
|
|
|
rewrite Nat.add_sub_swap in H2. rewrite Nat.add_sub in H2.
|
|
|
|
|
2023-01-22 04:06:55 -05:00
|
|
|
assert (K: forall m (u : list bool),
|
2023-01-24 01:56:21 -05:00
|
|
|
m < length u -> nth_error u m = nth_error (rev u) (length u - S m)).
|
|
|
|
intros m u. intro V.
|
|
|
|
assert (V' := V). apply nth_error_nth' with (d := false) in V'.
|
|
|
|
assert (exists l1 l2, u = l1 ++ (nth m u false)::l2 /\ length l1 = m).
|
|
|
|
apply nth_error_split. assumption. destruct H3. destruct H3. destruct H3.
|
|
|
|
rewrite V'.
|
|
|
|
assert (length u = length u). reflexivity. rewrite H3 in H5 at 2.
|
|
|
|
rewrite app_length in H5. rewrite H4 in H5.
|
|
|
|
rewrite H3 at 2. rewrite rev_app_distr. rewrite nth_error_app1.
|
|
|
|
replace (nth m u false :: x0) with ([nth m u false] ++ x0).
|
|
|
|
rewrite rev_app_distr. rewrite H5.
|
|
|
|
rewrite Nat.add_comm. replace (S m) with (m + 1).
|
|
|
|
rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc.
|
|
|
|
rewrite Nat.sub_diag. rewrite Nat.add_0_r.
|
|
|
|
rewrite nth_error_app2. rewrite rev_length. simpl.
|
2023-01-22 04:06:55 -05:00
|
|
|
rewrite Nat.sub_0_r. rewrite Nat.sub_diag. reflexivity.
|
2023-01-24 01:56:21 -05:00
|
|
|
rewrite rev_length. simpl. rewrite Nat.sub_0_r. apply Nat.le_refl.
|
|
|
|
apply Nat.le_refl. rewrite Nat.add_1_r. reflexivity. reflexivity.
|
|
|
|
rewrite rev_length. rewrite Nat.add_lt_mono_r with (p := m).
|
|
|
|
replace (S m) with (m + 1). rewrite <- Nat.add_sub_swap.
|
|
|
|
rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc.
|
|
|
|
rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite Nat.add_comm.
|
|
|
|
rewrite <- H5. apply Nat.sub_lt. rewrite H5. simpl.
|
|
|
|
rewrite Nat.add_succ_r. apply le_n_S. apply Nat.le_0_l.
|
|
|
|
apply Nat.lt_0_1. apply Nat.le_refl.
|
|
|
|
rewrite Nat.add_succ_r. rewrite Nat.add_0_r. rewrite Nat.le_succ_l.
|
|
|
|
assumption. apply Nat.add_1_r.
|
|
|
|
|
|
|
|
rewrite K with (u := rev (b::b0::b1::l)) in H2.
|
|
|
|
rewrite rev_involutive in H2. rewrite rev_length in H2.
|
|
|
|
contradiction H2. reflexivity.
|
|
|
|
|
|
|
|
rewrite rev_length. simpl. rewrite <- Nat.succ_lt_mono.
|
|
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
2023-01-22 04:06:55 -05:00
|
|
|
|
2023-01-24 01:56:21 -05:00
|
|
|
simpl. apply le_n_S. apply le_n_S. apply le_n_S.
|
|
|
|
apply Nat.le_0_l.
|
2023-01-22 02:16:44 -05:00
|
|
|
|
2023-01-24 01:56:21 -05:00
|
|
|
rewrite rev_length. simpl. rewrite <- Nat.succ_lt_mono.
|
|
|
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
2023-01-22 02:16:44 -05:00
|
|
|
|
2023-01-24 01:56:21 -05:00
|
|
|
rewrite app_length. simpl.
|
|
|
|
replace (S (S (S (length l)))) with (length l + 3).
|
|
|
|
rewrite <- Nat.add_sub_assoc. rewrite <- Nat.add_sub_assoc.
|
|
|
|
rewrite Nat.sub_diag. rewrite Nat.add_0_r.
|
|
|
|
apply Nat.le_add_r. apply Nat.le_refl.
|
|
|
|
apply Nat.le_add_l. rewrite Nat.add_comm. simpl. reflexivity.
|
|
|
|
Qed.
|
2023-01-22 02:16:44 -05:00
|
|
|
|
2023-01-27 08:06:30 -05:00
|
|
|
Lemma tm_step_palindromic_length_12_n :
|
2023-01-27 07:53:34 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
2023-01-27 08:49:38 -05:00
|
|
|
-> 6 < length a
|
|
|
|
-> 3 < n.
|
2023-01-27 07:53:34 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H W.
|
|
|
|
|
|
|
|
assert (length (tm_step n) <= length (tm_step n)).
|
2023-01-27 08:49:38 -05:00
|
|
|
reflexivity. rewrite H in H0 at 1.
|
|
|
|
rewrite app_length in H0.
|
|
|
|
|
|
|
|
assert (length (a++ rev a ++ tl) <= length hd + length (a ++ rev a ++ tl)).
|
|
|
|
apply Nat.le_add_l.
|
|
|
|
|
|
|
|
assert (length (a ++ rev a ++ tl) <= length (tm_step n)).
|
|
|
|
generalize H0. generalize H1. apply Nat.le_trans.
|
|
|
|
|
|
|
|
rewrite app_length in H2. rewrite app_length in H2. rewrite rev_length in H2.
|
|
|
|
rewrite Nat.add_comm in H2. rewrite Nat.add_shuffle0 in H2.
|
|
|
|
|
|
|
|
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
|
|
|
|
assert (4+4 < length a + length a). generalize W. generalize W.
|
|
|
|
apply Nat.add_lt_mono.
|
|
|
|
|
|
|
|
assert (length a + length a <= length a + length a + length tl).
|
|
|
|
apply Nat.le_add_r.
|
|
|
|
|
|
|
|
assert (length a + length a <= length (tm_step n)).
|
|
|
|
generalize H2. generalize H4. apply Nat.le_trans.
|
|
|
|
|
|
|
|
assert (4 + 4 < length (tm_step n)). generalize H5. generalize H3.
|
|
|
|
apply Nat.lt_le_trans. rewrite tm_size_power2 in H6.
|
|
|
|
replace (4+4) with (2^3) in H6.
|
|
|
|
|
|
|
|
rewrite <- Nat.pow_lt_mono_r_iff in H6.
|
|
|
|
assumption.
|
|
|
|
apply Nat.lt_1_2. reflexivity.
|
|
|
|
Admitted.
|
2023-01-27 07:53:34 -05:00
|
|
|
|
|
|
|
|
2023-01-26 04:08:29 -05:00
|
|
|
Theorem tm_step_palindromic_length_12_prefix :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
2023-01-27 08:49:38 -05:00
|
|
|
-> 6 < length a
|
2023-01-26 04:08:29 -05:00
|
|
|
-> length a mod 4 = 0 <-> length hd mod 4 = 0.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I. split; intro J;
|
|
|
|
apply tm_step_palindromic_length_12 with (n := n) (hd := hd) (tl := tl) in I.
|
|
|
|
rewrite app_length in I.
|
|
|
|
rewrite <- Nat.add_mod_idemp_r in I. rewrite J in I. rewrite Nat.add_0_r in I.
|
|
|
|
assumption. easy. assumption.
|
|
|
|
rewrite app_length in I.
|
|
|
|
rewrite <- Nat.add_mod_idemp_l in I. rewrite J in I. rewrite Nat.add_0_l in I.
|
|
|
|
assumption. easy. assumption.
|
|
|
|
Qed.
|
|
|
|
|
2023-01-27 07:53:34 -05:00
|
|
|
Theorem tm_step_palindromic_length_12_prefix2 :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
2023-01-27 08:49:38 -05:00
|
|
|
-> 6 < length a
|
2023-01-27 07:53:34 -05:00
|
|
|
-> length a mod 4 = 0 -> length tl mod 4 = 0.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I J.
|
|
|
|
assert (K: length hd mod 4 = 0).
|
|
|
|
generalize J. generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_length_12_prefix.
|
|
|
|
assert (L: length (hd ++ a ++ rev a ++ tl) mod 4 = 0).
|
|
|
|
rewrite <- H. rewrite tm_size_power2.
|
2023-01-26 04:08:29 -05:00
|
|
|
|
2023-01-27 08:49:38 -05:00
|
|
|
assert (V: 3 < n). generalize I. generalize H.
|
2023-01-27 08:06:30 -05:00
|
|
|
apply tm_step_palindromic_length_12_n.
|
2023-01-27 08:49:38 -05:00
|
|
|
apply Nat.lt_succ_l in V. apply Nat.lt_succ_l in V.
|
2023-01-27 08:06:30 -05:00
|
|
|
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
|
|
|
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
|
|
|
rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
|
|
|
|
rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
|
|
|
|
apply Nat.mod_mul. easy. apply le_0_n. apply le_0_n.
|
|
|
|
|
|
|
|
rewrite app_length in L.
|
|
|
|
rewrite <- Nat.add_mod_idemp_l in L. rewrite K in L.
|
|
|
|
rewrite app_length in L. rewrite Nat.add_0_l in L.
|
|
|
|
rewrite <- Nat.add_mod_idemp_l in L. rewrite J in L.
|
|
|
|
rewrite Nat.add_0_l in L. rewrite app_length in L.
|
|
|
|
rewrite <- Nat.add_mod_idemp_l in L. rewrite rev_length in L.
|
|
|
|
rewrite J in L. assumption. easy. easy. easy.
|
|
|
|
Qed.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
Lemma tm_step_palindromic_even_morphism1 :
|
2023-01-26 08:48:30 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
2023-01-26 09:28:49 -05:00
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 0 < length a
|
2023-01-26 08:48:30 -05:00
|
|
|
-> even (length a) = true
|
2023-01-26 09:28:49 -05:00
|
|
|
-> tm_morphism (tm_step (pred n)) =
|
|
|
|
tm_morphism
|
|
|
|
(firstn (Nat.div2 (length hd)) (tm_step (pred n)) ++
|
|
|
|
firstn (Nat.div2 (length a))
|
|
|
|
(skipn (Nat.div2 (length hd)) (tm_step (pred n))) ++
|
|
|
|
map negb
|
|
|
|
(rev
|
|
|
|
(firstn (Nat.div2 (length a))
|
|
|
|
(skipn (Nat.div2 (length hd)) (tm_step (pred n))))) ++
|
|
|
|
skipn (Nat.div2 (length hd) + length a) (tm_step (pred n))).
|
2023-01-26 08:48:30 -05:00
|
|
|
Proof.
|
2023-01-26 09:28:49 -05:00
|
|
|
intros n hd a tl. intros H Z J.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
(* proof that n <> 0 *)
|
|
|
|
destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
|
2023-01-26 08:48:30 -05:00
|
|
|
apply Nat.le_refl.
|
2023-01-26 09:28:49 -05:00
|
|
|
rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0.
|
|
|
|
rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0. simpl in H0.
|
|
|
|
apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0.
|
|
|
|
rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0.
|
|
|
|
assert (K: 1 <= length a + (length tl + length hd)).
|
|
|
|
rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption.
|
|
|
|
rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0.
|
|
|
|
rewrite H0 in Z. inversion Z.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
assert (even (length (hd ++ a)) = true). generalize Z. generalize H.
|
|
|
|
apply tm_step_palindromic_even_center.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
assert (I: even (length hd) = true). rewrite app_length in H0.
|
|
|
|
rewrite Nat.even_add in H0. rewrite J in H0.
|
|
|
|
destruct (even (length hd)). reflexivity. inversion H0.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
assert (K: even (length (rev a)) = true). rewrite rev_length. assumption.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
|
|
|
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
|
|
|
|
|
|
|
|
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
|
|
|
|
(tm_step n))).
|
|
|
|
generalize H0. generalize H. apply tm_morphism_app2.
|
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
rewrite <- app_assoc in H. symmetry in H1.
|
|
|
|
assert (even (length (hd ++ a ++ (rev a))) = true).
|
2023-01-26 08:48:30 -05:00
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite I.
|
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
|
|
|
|
reflexivity.
|
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a))))
|
2023-01-26 08:48:30 -05:00
|
|
|
(tm_step n))).
|
2023-01-26 09:28:49 -05:00
|
|
|
replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H.
|
|
|
|
generalize H2. generalize H. apply tm_morphism_app3.
|
2023-01-26 08:48:30 -05:00
|
|
|
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
|
|
|
|
|
|
|
|
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
|
|
|
|
generalize I. generalize H. apply tm_morphism_app2.
|
|
|
|
|
|
|
|
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
|
|
|
|
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
|
|
|
|
generalize I. generalize H1. apply tm_morphism_app3.
|
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
rewrite skipn_firstn_comm in H5. rewrite app_length in H5.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
|
|
|
replace (Nat.div2 (length hd + length a))
|
2023-01-26 09:28:49 -05:00
|
|
|
with ((length hd) / 2 + Nat.div2 (length a)) in H5.
|
|
|
|
rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5.
|
|
|
|
rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
rewrite H4 in H. rewrite H5 in H. rewrite H3 in H.
|
|
|
|
rewrite tm_morphism_rev in H.
|
2023-01-26 08:48:30 -05:00
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite tm_step_lemma in H.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
|
|
|
rewrite app_length in H. rewrite app_length in H. rewrite rev_length in H.
|
|
|
|
replace (length a + length a) with ((length a)*2) in H.
|
|
|
|
replace (Nat.div2 (length hd + length a * 2))
|
|
|
|
with ((length hd + length a * 2) / 2) in H.
|
|
|
|
rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
|
|
|
|
|
|
|
|
assumption. easy.
|
|
|
|
rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl.
|
|
|
|
rewrite Nat.add_0_r. reflexivity.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
|
|
|
apply Nat.le_refl.
|
|
|
|
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
|
|
|
|
rewrite Nat.mul_comm.
|
|
|
|
|
2023-01-26 09:28:49 -05:00
|
|
|
rewrite Nat.div2_odd with (a := length a) at 2.
|
|
|
|
rewrite <- Nat.negb_even. rewrite J. simpl.
|
|
|
|
rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy.
|
2023-01-26 08:48:30 -05:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
Lemma tm_step_palindromic_even_morphism2 :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
2023-01-27 08:49:38 -05:00
|
|
|
-> 6 < length a
|
2023-01-26 10:41:34 -05:00
|
|
|
-> (length a) mod 4 = 0
|
2023-01-27 07:53:34 -05:00
|
|
|
-> hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n)))))
|
2023-01-27 11:06:04 -05:00
|
|
|
/\ a = tm_morphism (tm_morphism
|
|
|
|
(firstn (length a / 4) (skipn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n))))))
|
2023-01-27 11:29:52 -05:00
|
|
|
/\ tl = tm_morphism (tm_morphism
|
|
|
|
(skipn (length hd / 4 + Nat.div2 (length a))
|
|
|
|
(tm_step (pred (pred n))))).
|
2023-01-26 10:41:34 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H W J0.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (Z: 0 < length a).
|
|
|
|
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
|
|
|
|
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
|
|
|
|
assumption.
|
2023-01-26 08:48:30 -05:00
|
|
|
|
2023-01-27 08:49:38 -05:00
|
|
|
assert (V: 3 < n). generalize W. generalize H.
|
2023-01-27 07:53:34 -05:00
|
|
|
apply tm_step_palindromic_length_12_n.
|
2023-01-27 08:49:38 -05:00
|
|
|
apply Nat.lt_succ_l in V. apply Nat.lt_succ_l in V.
|
2023-01-27 07:53:34 -05:00
|
|
|
destruct n. inversion V.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
|
|
|
|
generalize H. apply tm_step_palindromic_length_12_prefix.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (EVEN: forall m, m mod 4 = 0 -> even m = true).
|
|
|
|
intro m. intro U. rewrite <- Nat.div_exact in U.
|
|
|
|
rewrite U. rewrite Nat.even_mul. reflexivity. easy.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (J: even (length a) = true).
|
|
|
|
apply EVEN in J0. assumption.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (even (length (hd ++ a)) = true). generalize Z. generalize H.
|
|
|
|
apply tm_step_palindromic_even_center.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (I: even (length hd) = true). rewrite app_length in H0.
|
|
|
|
rewrite Nat.even_add in H0. rewrite J in H0.
|
|
|
|
destruct (even (length hd)). reflexivity. inversion H0.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (K: even (length (rev a)) = true). rewrite rev_length. assumption.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (hd ++ a = tm_morphism (firstn (Nat.div2 (length (hd ++ a)))
|
|
|
|
(tm_step n))).
|
|
|
|
generalize H0. generalize H. apply tm_morphism_app2.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
rewrite <- app_assoc in H. symmetry in H1.
|
|
|
|
assert (even (length (hd ++ a ++ (rev a))) = true).
|
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite I.
|
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite J. rewrite K.
|
|
|
|
reflexivity.
|
2023-01-26 09:28:49 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (tl = tm_morphism (skipn (Nat.div2 (length (hd ++ a ++ (rev a))))
|
|
|
|
(tm_step n))).
|
|
|
|
replace (hd ++ a ++ (rev a) ++ tl) with ((hd ++ a ++ (rev a)) ++ tl) in H.
|
|
|
|
generalize H2. generalize H. apply tm_morphism_app3.
|
|
|
|
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
|
2023-01-26 04:08:29 -05:00
|
|
|
|
2023-01-26 10:41:34 -05:00
|
|
|
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
|
|
|
|
generalize I. generalize H. apply tm_morphism_app2.
|
|
|
|
|
|
|
|
assert (a = tm_morphism (skipn (Nat.div2 (length hd))
|
|
|
|
(firstn (Nat.div2 (length (hd ++ a))) (tm_step n)))).
|
|
|
|
generalize I. generalize H1. apply tm_morphism_app3.
|
|
|
|
|
|
|
|
rewrite skipn_firstn_comm in H5. rewrite app_length in H5.
|
|
|
|
|
|
|
|
replace (Nat.div2 (length hd + length a))
|
|
|
|
with ((length hd) / 2 + Nat.div2 (length a)) in H5.
|
|
|
|
rewrite <- Nat.div2_div in H5. rewrite Nat.add_sub_swap in H5.
|
|
|
|
rewrite Nat.sub_diag in H5. rewrite Nat.add_0_l in H5.
|
|
|
|
|
|
|
|
rewrite H4 in H. rewrite H5 in H. rewrite H3 in H.
|
|
|
|
rewrite tm_morphism_rev in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H.
|
|
|
|
|
|
|
|
rewrite app_length in H. rewrite app_length in H. rewrite rev_length in H.
|
|
|
|
replace (length a + length a) with ((length a)*2) in H.
|
|
|
|
replace (Nat.div2 (length hd + length a * 2))
|
|
|
|
with ((length hd + length a * 2) / 2) in H.
|
|
|
|
rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
|
|
|
|
|
|
|
|
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) + length a) (tm_step n)).
|
|
|
|
fold hd' in H. fold a' in H. fold tl' in H.
|
|
|
|
|
2023-01-27 03:38:54 -05:00
|
|
|
assert (length hd' = Nat.div2 (length hd)). unfold hd'. rewrite H4.
|
|
|
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
|
|
|
replace (min (Nat.div2 (length hd)) (length (tm_step n)))
|
|
|
|
with (min (length (tm_step n)) (Nat.div2 (length hd))).
|
|
|
|
rewrite Nat.min_comm. rewrite Nat.min_assoc. rewrite Nat.min_id.
|
|
|
|
reflexivity. rewrite Nat.min_comm. reflexivity.
|
|
|
|
|
|
|
|
assert (length a' = Nat.div2 (length a)). unfold a'. rewrite H5.
|
|
|
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
|
|
|
rewrite Nat.min_comm. rewrite <- H6.
|
|
|
|
replace
|
|
|
|
(min (Nat.div2 (length a)) (length (skipn (length hd') (tm_step n))))
|
|
|
|
with
|
|
|
|
(min (length (skipn (length hd') (tm_step n))) (Nat.div2 (length a))).
|
|
|
|
rewrite Nat.min_assoc. rewrite Nat.min_id. reflexivity.
|
|
|
|
rewrite Nat.min_comm. reflexivity.
|
|
|
|
|
|
|
|
assert (length tl' = Nat.div2 (length tl)). unfold tl'. rewrite H3.
|
|
|
|
rewrite tm_morphism_length_half. rewrite app_length.
|
|
|
|
symmetry. rewrite Nat.div2_div.
|
|
|
|
rewrite app_length. rewrite rev_length.
|
|
|
|
replace (length a + length a) with (length a * 2).
|
|
|
|
rewrite Nat.div_add. rewrite <- Nat.div2_div. reflexivity. easy.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
|
|
|
|
assert (I': even (length hd') = true). rewrite H6.
|
|
|
|
rewrite <- Nat.div_exact in J1. rewrite J1.
|
|
|
|
replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite Nat.div2_double.
|
|
|
|
rewrite Nat.even_mul. reflexivity. reflexivity. easy.
|
|
|
|
|
|
|
|
assert (J': even (length a') = true). rewrite H7.
|
|
|
|
rewrite <- Nat.div_exact in J0. rewrite J0.
|
|
|
|
replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite Nat.div2_double.
|
|
|
|
rewrite Nat.even_mul. reflexivity. reflexivity. easy.
|
|
|
|
|
|
|
|
assert (K': even (length (map negb (rev a'))) = true).
|
|
|
|
rewrite map_length. rewrite rev_length. assumption.
|
|
|
|
|
2023-01-27 09:20:21 -05:00
|
|
|
assert (Q: length hd' <= length (tm_step n)).
|
|
|
|
rewrite H. rewrite app_length. apply Nat.le_add_r.
|
|
|
|
|
2023-01-27 11:06:04 -05:00
|
|
|
assert (Q': length hd' + length a' <= length (tm_step n)).
|
|
|
|
rewrite H. rewrite app_assoc. rewrite app_length.
|
|
|
|
rewrite <- app_length. apply Nat.le_add_r.
|
2023-01-27 09:20:21 -05:00
|
|
|
|
2023-01-27 04:05:25 -05:00
|
|
|
assert (H0': even (length (hd' ++ a')) = true).
|
|
|
|
rewrite app_length. rewrite Nat.even_add.
|
|
|
|
rewrite I'. rewrite J'. reflexivity.
|
|
|
|
|
|
|
|
destruct n. inversion V. inversion H10.
|
|
|
|
rewrite app_assoc in H. rewrite <- tm_step_lemma in H.
|
|
|
|
|
|
|
|
assert (H1': hd' ++ a' = tm_morphism (firstn (Nat.div2 (length (hd' ++ a')))
|
|
|
|
(tm_step n))).
|
|
|
|
generalize H0'. generalize H. apply tm_morphism_app2.
|
|
|
|
|
|
|
|
rewrite <- app_assoc in H. symmetry in H1'.
|
|
|
|
assert (H2': even (length (hd' ++ a' ++ (map negb (rev a')))) = true).
|
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite I'.
|
|
|
|
rewrite app_length. rewrite Nat.even_add. rewrite J'. rewrite K'.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
assert (H3': tl' = tm_morphism (skipn
|
|
|
|
(Nat.div2 (length (hd' ++ a' ++ (map negb (rev a')))))
|
|
|
|
(tm_step n))).
|
|
|
|
replace (hd' ++ a' ++ (map negb (rev a')) ++ tl')
|
|
|
|
with ((hd' ++ a' ++ (map negb (rev a'))) ++ tl') in H.
|
|
|
|
generalize H2'. generalize H. apply tm_morphism_app3.
|
|
|
|
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
|
|
|
|
|
|
|
|
assert (H4': hd' = tm_morphism (firstn (Nat.div2 (length hd')) (tm_step n))).
|
|
|
|
generalize I'. generalize H. apply tm_morphism_app2.
|
|
|
|
|
|
|
|
assert (H5': a' = tm_morphism (skipn (Nat.div2 (length hd'))
|
|
|
|
(firstn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))).
|
|
|
|
generalize I'. generalize H1'. apply tm_morphism_app3.
|
|
|
|
|
|
|
|
rewrite skipn_firstn_comm in H5'. rewrite app_length in H5'.
|
|
|
|
|
|
|
|
replace (Nat.div2 (length hd' + length a'))
|
|
|
|
with ((length hd') / 2 + Nat.div2 (length a')) in H5'.
|
|
|
|
rewrite <- Nat.div2_div in H5'. rewrite Nat.add_sub_swap in H5'.
|
|
|
|
rewrite Nat.sub_diag in H5'. rewrite Nat.add_0_l in H5'.
|
|
|
|
|
|
|
|
rewrite H4' in H. rewrite H5' in H. rewrite H3' in H.
|
|
|
|
rewrite tm_morphism_rev2 in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_eq in H.
|
|
|
|
|
|
|
|
rewrite app_length in H. rewrite app_length in H.
|
|
|
|
rewrite map_length in H. rewrite rev_length in H.
|
|
|
|
replace (length a' + length a') with ((length a')*2) in H.
|
|
|
|
replace (Nat.div2 (length hd' + length a' * 2))
|
|
|
|
with ((length hd' + length a' * 2) / 2) in H.
|
|
|
|
rewrite Nat.div_add in H. rewrite <- Nat.div2_div in H.
|
|
|
|
|
2023-01-27 04:11:47 -05:00
|
|
|
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') + length a') (tm_step n)).
|
|
|
|
fold hd'' in H. fold a'' in H. fold tl'' in H.
|
|
|
|
|
|
|
|
assert (length hd'' = Nat.div2 (length hd')). unfold hd''. rewrite H4'.
|
|
|
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
|
|
|
replace (min (Nat.div2 (length hd')) (length (tm_step n)))
|
|
|
|
with (min (length (tm_step n)) (Nat.div2 (length hd'))).
|
|
|
|
rewrite Nat.min_comm. rewrite Nat.min_assoc. rewrite Nat.min_id.
|
|
|
|
reflexivity. rewrite Nat.min_comm. reflexivity.
|
|
|
|
|
|
|
|
assert (length a'' = Nat.div2 (length a')). unfold a''. rewrite H5'.
|
|
|
|
rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
|
|
|
|
rewrite Nat.min_comm. rewrite <- H9.
|
|
|
|
replace
|
|
|
|
(min (Nat.div2 (length a')) (length (skipn (length hd'') (tm_step n))))
|
|
|
|
with
|
|
|
|
(min (length (skipn (length hd'') (tm_step n))) (Nat.div2 (length a'))).
|
|
|
|
rewrite Nat.min_assoc. rewrite Nat.min_id. reflexivity.
|
|
|
|
rewrite Nat.min_comm. reflexivity.
|
|
|
|
|
|
|
|
assert (length tl'' = Nat.div2 (length tl')). unfold tl''. rewrite H3'.
|
|
|
|
rewrite tm_morphism_length_half. rewrite app_length.
|
|
|
|
symmetry. rewrite Nat.div2_div.
|
|
|
|
rewrite app_length. rewrite map_length. rewrite rev_length.
|
|
|
|
replace (length a' + length a') with (length a' * 2).
|
|
|
|
rewrite Nat.div_add. rewrite <- Nat.div2_div. reflexivity. easy.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
|
2023-01-27 07:53:34 -05:00
|
|
|
split.
|
|
|
|
rewrite <- pred_Sn. rewrite <- pred_Sn.
|
|
|
|
rewrite H4 at 1. fold hd'. rewrite H4'. unfold hd'.
|
|
|
|
rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
|
|
|
|
rewrite Nat.div_div. reflexivity. easy. easy.
|
2023-01-27 09:20:21 -05:00
|
|
|
rewrite <- H6. assumption.
|
2023-01-27 07:53:34 -05:00
|
|
|
|
2023-01-27 11:06:04 -05:00
|
|
|
split.
|
|
|
|
rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H5 at 1. fold a'.
|
|
|
|
rewrite H5'. unfold a'.
|
|
|
|
rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
|
|
|
|
rewrite Nat.div_div.
|
|
|
|
replace (length hd / 4) with (Nat.div2 (length hd')). reflexivity.
|
|
|
|
replace 4 with (2*2). rewrite <- Nat.div_div.
|
|
|
|
rewrite <- Nat.div2_div. rewrite <- Nat.div2_div. rewrite <- H6. reflexivity.
|
|
|
|
easy. easy. reflexivity. easy. easy.
|
|
|
|
rewrite skipn_length.
|
|
|
|
apply Nat.le_add_le_sub_l.
|
|
|
|
rewrite <- H6. rewrite <- H7. assumption.
|
2023-01-27 07:53:34 -05:00
|
|
|
|
2023-01-27 11:29:52 -05:00
|
|
|
rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H3.
|
|
|
|
rewrite app_length.
|
|
|
|
rewrite app_length. rewrite rev_length.
|
|
|
|
replace (length a + length a) with (length a * 2).
|
|
|
|
rewrite Nat.div2_div. rewrite Nat.div_add.
|
|
|
|
rewrite <- Nat.div2_div. fold tl'. rewrite H3'.
|
|
|
|
rewrite app_length.
|
|
|
|
rewrite app_length. rewrite map_length. rewrite rev_length.
|
|
|
|
replace (length a' + length a') with (length a' * 2).
|
|
|
|
rewrite Nat.div2_div. rewrite Nat.div_add.
|
|
|
|
rewrite H6. rewrite H7.
|
|
|
|
rewrite Nat.div2_div. rewrite Nat.div_div. reflexivity.
|
|
|
|
easy. easy. easy.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
easy.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
easy.
|
|
|
|
rewrite Nat.div2_div. reflexivity.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
apply Nat.le_refl.
|
2023-01-27 07:53:34 -05:00
|
|
|
|
2023-01-27 11:39:07 -05:00
|
|
|
rewrite <- Nat.div_add. rewrite Nat.mul_comm.
|
|
|
|
replace (2 * Nat.div2 (length a'))
|
|
|
|
with (2 * Nat.div2 (length a') + Nat.b2n (Nat.odd (length a'))).
|
|
|
|
rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
|
|
|
|
rewrite <- Nat.negb_even. rewrite J'. simpl. rewrite Nat.add_0_r.
|
|
|
|
reflexivity. easy. easy. rewrite Nat.div2_div. reflexivity.
|
|
|
|
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
apply Nat.le_refl.
|
|
|
|
rewrite <- Nat.div_add. rewrite Nat.mul_comm.
|
|
|
|
replace (2 * Nat.div2 (length a))
|
|
|
|
with (2 * Nat.div2 (length a) + Nat.b2n (Nat.odd (length a))).
|
|
|
|
rewrite <- Nat.div2_odd. rewrite <- Nat.div2_div. reflexivity.
|
|
|
|
rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r.
|
|
|
|
reflexivity. easy.
|
|
|
|
Qed.
|
2023-01-26 10:41:34 -05:00
|
|
|
|
|
|
|
|
2023-02-01 15:02:44 -05:00
|
|
|
Lemma tm_step_palindromic_power2_even_alpha :
|
2023-01-31 16:03:20 -05:00
|
|
|
forall (m n : nat) (hd a tl : list bool),
|
2023-01-31 11:54:59 -05:00
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length a = 2^(Nat.double m)
|
|
|
|
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
|
|
|
<-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0.
|
|
|
|
Proof.
|
2023-01-31 16:03:20 -05:00
|
|
|
intros m n hd a tl. intros H I J.
|
2023-01-31 11:54:59 -05:00
|
|
|
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
inversion H3. inversion H5. inversion H7.
|
|
|
|
|
|
|
|
assert (W: (length a) mod 4 = 0).
|
|
|
|
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
|
|
|
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
|
|
|
rewrite Nat.mul_assoc in J.
|
|
|
|
replace (2*2) with 4 in J. rewrite J.
|
|
|
|
rewrite <- Nat.mul_mod_idemp_l. reflexivity.
|
|
|
|
easy. reflexivity. apply le_0_n. apply le_0_n.
|
|
|
|
|
|
|
|
assert (length (hd ++ a) mod 4 = 0).
|
|
|
|
assert (W' := W).
|
|
|
|
rewrite tm_step_palindromic_length_12_prefix
|
|
|
|
with (hd := hd) (n := n) (tl := tl) in W'.
|
|
|
|
rewrite app_length. rewrite Nat.add_mod.
|
|
|
|
rewrite W. rewrite W'. reflexivity. easy. assumption. assumption.
|
|
|
|
|
|
|
|
split.
|
|
|
|
- intro P.
|
|
|
|
rewrite <- Nat.mul_cancel_l with (p := 4).
|
|
|
|
rewrite <- Nat.mul_mod_distr_l.
|
|
|
|
replace 4 with (2*2) at 3. rewrite <- Nat.mul_assoc.
|
|
|
|
rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r.
|
|
|
|
|
|
|
|
replace (S (S (pred (Nat.double (pred (S (S m)))))))
|
|
|
|
with (pred (Nat.double (S (S m)))).
|
|
|
|
replace (4 * (length (hd ++ a) / 4))
|
|
|
|
with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4).
|
|
|
|
rewrite <- Nat.div_mod_eq. assumption.
|
|
|
|
rewrite H0. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
|
|
|
|
rewrite <- pred_Sn. rewrite Nat.double_S.
|
|
|
|
rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity.
|
|
|
|
rewrite Nat.neq_0_lt_0. rewrite Nat.double_S.
|
|
|
|
apply Nat.lt_0_succ. apply le_0_n. apply le_0_n.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
apply Nat.pow_nonzero. easy. easy. easy.
|
|
|
|
- intro P.
|
|
|
|
rewrite <- Nat.mul_cancel_l with (p := 4) in P.
|
|
|
|
rewrite <- Nat.mul_mod_distr_l in P.
|
|
|
|
replace 4 with (2*2) in P at 3. rewrite <- Nat.mul_assoc in P.
|
|
|
|
rewrite <- Nat.pow_succ_r in P. rewrite <- Nat.pow_succ_r in P.
|
|
|
|
|
|
|
|
replace (S (S (pred (Nat.double (pred (S (S m)))))))
|
|
|
|
with (pred (Nat.double (S (S m)))) in P.
|
|
|
|
replace (4 * (length (hd ++ a) / 4))
|
|
|
|
with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4) in P.
|
|
|
|
rewrite <- Nat.div_mod_eq in P. assumption.
|
|
|
|
rewrite H0. rewrite Nat.add_0_r. reflexivity.
|
|
|
|
|
|
|
|
rewrite <- pred_Sn. rewrite Nat.double_S.
|
|
|
|
rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity.
|
|
|
|
rewrite Nat.neq_0_lt_0. rewrite Nat.double_S.
|
|
|
|
apply Nat.lt_0_succ. apply le_0_n. apply le_0_n.
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
apply Nat.pow_nonzero. easy. easy. easy.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-02-01 15:02:44 -05:00
|
|
|
Lemma tm_step_palindromic_power2_even_beta :
|
2023-02-01 10:39:17 -05:00
|
|
|
forall (m n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length a = 2^(Nat.double m)
|
|
|
|
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
2023-02-01 12:41:16 -05:00
|
|
|
\/ 2^6 <= length a.
|
2023-02-01 10:39:17 -05:00
|
|
|
Proof.
|
|
|
|
intros m n hd a tl. intros H I J.
|
|
|
|
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
inversion H3. inversion H5. inversion H7.
|
|
|
|
|
|
|
|
destruct m. left.
|
|
|
|
|
|
|
|
assert (W: length a mod 4 = 0). rewrite J. reflexivity.
|
|
|
|
|
|
|
|
assert (
|
|
|
|
hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n)))))
|
|
|
|
/\ a = tm_morphism (tm_morphism
|
|
|
|
(firstn (length a / 4) (skipn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n))))))
|
|
|
|
/\ tl = tm_morphism (tm_morphism
|
|
|
|
(skipn (length hd / 4 + Nat.div2 (length a))
|
|
|
|
(tm_step (pred (pred n)))))).
|
|
|
|
generalize W. generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_even_morphism2.
|
|
|
|
destruct H0 as [K H0]. destruct H0 as [L M].
|
|
|
|
|
|
|
|
assert (V: 3 < n). generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_length_12_n.
|
|
|
|
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
|
|
|
|
|
|
|
rewrite K in H. rewrite L in H. rewrite M in H.
|
|
|
|
rewrite tm_morphism_twice_rev in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
|
|
rewrite <- tm_morphism_app 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_step_lemma in H.
|
|
|
|
rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
|
|
|
|
rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
|
|
|
|
|
|
|
|
pose (hd' := (firstn (length hd / 4) (tm_step n))).
|
|
|
|
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
|
|
|
|
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
|
|
|
|
fold hd' in H. fold a' in H. fold tl' in H.
|
|
|
|
|
|
|
|
rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K.
|
|
|
|
rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
|
|
|
|
fold hd' in K. fold a' in L.
|
|
|
|
assert (N: length a = length a). reflexivity. rewrite L in N at 2.
|
|
|
|
rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
|
|
|
|
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
|
|
|
assert (O: length hd = length hd). reflexivity. rewrite K in O at 2.
|
|
|
|
rewrite tm_morphism_length in O. rewrite tm_morphism_length in O.
|
|
|
|
rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O.
|
|
|
|
|
|
|
|
replace (2^ pred (Nat.double 2)) with (4*2).
|
|
|
|
rewrite app_length. rewrite N. rewrite O.
|
|
|
|
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
|
|
|
rewrite Nat.mul_eq_0. right. rewrite <- app_length.
|
|
|
|
|
|
|
|
assert (U: even (length (hd' ++ a')) = true).
|
|
|
|
assert (0 < length a').
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
rewrite N in I.
|
|
|
|
rewrite <- Nat.mul_1_r in I at 1.
|
|
|
|
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ.
|
|
|
|
generalize H0. generalize H. apply tm_step_palindromic_even_center.
|
|
|
|
|
|
|
|
replace (length (hd' ++ a'))
|
|
|
|
with (2 * Nat.div2 (length (hd' ++ a'))
|
|
|
|
+ Nat.b2n (Nat.odd (length (hd' ++ a')))).
|
|
|
|
rewrite <- Nat.negb_even. rewrite U. rewrite Nat.add_0_r.
|
|
|
|
rewrite Nat.mul_mod. reflexivity. easy. symmetry. apply Nat.div2_odd.
|
|
|
|
easy. easy. reflexivity. reflexivity. reflexivity.
|
|
|
|
|
|
|
|
right. rewrite J. rewrite Nat.double_S. rewrite Nat.double_S.
|
2023-02-01 12:41:16 -05:00
|
|
|
rewrite Nat.double_S. apply Nat.pow_le_mono_r. easy.
|
|
|
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
|
|
|
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
|
|
|
|
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
|
|
|
|
apply le_0_n.
|
2023-02-01 10:39:17 -05:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-02-01 15:02:44 -05:00
|
|
|
Theorem tm_step_palindromic_power2_even :
|
2023-02-01 12:41:16 -05:00
|
|
|
forall (m n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length a = 2^(Nat.double m)
|
|
|
|
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0.
|
|
|
|
Proof.
|
|
|
|
intros m n hd a tl. intros H I J.
|
|
|
|
assert (E: length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
|
|
|
\/ 2^6 <= length a).
|
|
|
|
generalize J. generalize I. generalize H.
|
2023-02-01 15:02:44 -05:00
|
|
|
apply tm_step_palindromic_power2_even_beta.
|
2023-02-01 12:41:16 -05:00
|
|
|
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
destruct m. rewrite J in I. inversion I. inversion H1.
|
|
|
|
inversion H3. inversion H5. inversion H7.
|
2023-02-01 10:39:17 -05:00
|
|
|
|
2023-02-01 12:41:16 -05:00
|
|
|
generalize dependent hd.
|
|
|
|
generalize dependent a.
|
|
|
|
generalize dependent tl.
|
|
|
|
generalize dependent n.
|
|
|
|
|
|
|
|
induction m.
|
|
|
|
- intros n tl a I J hd H E. destruct E. assumption.
|
|
|
|
rewrite J in H0. rewrite <- Nat.pow_le_mono_r_iff in H0.
|
|
|
|
inversion H0. inversion H2. inversion H4.
|
|
|
|
inversion H6. apply Nat.nle_succ_0 in H8.
|
|
|
|
contradiction H8. apply Nat.lt_1_2.
|
|
|
|
- intros n tl a I J hd H E. assert (E' := E).
|
|
|
|
destruct E as [E0 | E1]. assumption.
|
2023-02-01 15:02:44 -05:00
|
|
|
rewrite tm_step_palindromic_power2_even_alpha with (n := n) (tl := tl).
|
2023-02-01 12:41:16 -05:00
|
|
|
rewrite <- pred_Sn.
|
|
|
|
|
|
|
|
|
|
|
|
assert (W: (length a) mod 4 = 0).
|
|
|
|
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
|
|
|
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
|
|
|
rewrite Nat.mul_assoc in J.
|
|
|
|
replace (2*2) with 4 in J. rewrite J.
|
|
|
|
rewrite <- Nat.mul_mod_idemp_l. reflexivity.
|
|
|
|
easy. reflexivity. apply le_0_n. apply le_0_n.
|
|
|
|
|
|
|
|
assert (
|
|
|
|
hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n)))))
|
|
|
|
/\ a = tm_morphism (tm_morphism
|
|
|
|
(firstn (length a / 4) (skipn (length hd / 4)
|
|
|
|
(tm_step (pred (pred n))))))
|
|
|
|
/\ tl = tm_morphism (tm_morphism
|
|
|
|
(skipn (length hd / 4 + Nat.div2 (length a))
|
|
|
|
(tm_step (pred (pred n)))))).
|
|
|
|
generalize W. generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_even_morphism2.
|
|
|
|
destruct H0 as [K H0]. destruct H0 as [L M].
|
|
|
|
|
|
|
|
assert (V: 3 < n). generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_length_12_n.
|
|
|
|
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
|
|
|
|
|
|
|
rewrite K in H. rewrite L in H. rewrite M in H.
|
|
|
|
rewrite tm_morphism_twice_rev in H.
|
|
|
|
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
|
|
|
rewrite <- tm_morphism_app 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_step_lemma in H.
|
|
|
|
rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
|
|
|
|
rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
|
|
|
|
|
|
|
|
pose (hd' := (firstn (length hd / 4) (tm_step n))).
|
|
|
|
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
|
|
|
|
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
|
|
|
|
fold hd' in H. fold a' in H. fold tl' in H.
|
|
|
|
|
|
|
|
rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K.
|
|
|
|
rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
|
|
|
|
fold hd' in K. fold a' in L.
|
|
|
|
assert (N: length a = length a). reflexivity. rewrite L in N at 2.
|
|
|
|
rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
|
|
|
|
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
|
|
|
assert (O: length hd = length hd). reflexivity. rewrite K in O at 2.
|
|
|
|
rewrite tm_morphism_length in O. rewrite tm_morphism_length in O.
|
|
|
|
rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O.
|
|
|
|
|
|
|
|
rewrite app_length. rewrite N. rewrite O. rewrite <- Nat.mul_add_distr_l.
|
|
|
|
rewrite Nat.mul_comm. rewrite Nat.div_mul. rewrite <- app_length.
|
|
|
|
|
|
|
|
assert (Y: length a' = 2 ^ Nat.double (S (S m))).
|
|
|
|
rewrite J in N. rewrite Nat.double_S in N.
|
|
|
|
rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N.
|
|
|
|
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
|
|
|
rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity.
|
|
|
|
apply le_0_n. apply le_0_n.
|
|
|
|
|
|
|
|
assert (Y': 6 < length a').
|
|
|
|
rewrite N in E1.
|
|
|
|
rewrite Nat.pow_succ_r in E1. rewrite Nat.pow_succ_r in E1.
|
|
|
|
rewrite Nat.mul_assoc in E1. replace (2*2) with 4 in E1.
|
|
|
|
rewrite <- Nat.mul_le_mono_pos_l in E1.
|
|
|
|
assert (6 < 2^4). 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.
|
|
|
|
apply Nat.lt_0_succ. generalize E1. generalize H0.
|
|
|
|
apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity.
|
|
|
|
apply le_0_n. apply le_0_n.
|
|
|
|
|
|
|
|
apply IHm with (n := n) (tl := tl').
|
|
|
|
assumption. assumption. assumption.
|
|
|
|
generalize Y. generalize Y'. generalize H.
|
2023-02-01 15:02:44 -05:00
|
|
|
apply tm_step_palindromic_power2_even_beta.
|
2023-02-01 12:41:16 -05:00
|
|
|
easy. reflexivity. reflexivity.
|
|
|
|
assumption. assumption. assumption.
|
|
|
|
Qed.
|
2023-02-01 10:39:17 -05:00
|
|
|
|
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
Lemma tm_step_palindrome_7_destruct :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> length a = 7
|
|
|
|
-> exists x, a = [negb x; negb x; x; negb x; x; x; negb x].
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
|
|
|
|
assert (J: 6 < length a). rewrite I. apply Nat.lt_succ_diag_r.
|
|
|
|
assert (K: length (hd ++ a) mod 4 = 0). generalize J. generalize H.
|
|
|
|
apply tm_step_palindromic_length_12.
|
|
|
|
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I.
|
|
|
|
|
|
|
|
destruct a.
|
|
|
|
replace (rev [b; b0; b1; b2; b3; b4; b5])
|
|
|
|
with ([b5; b4; b3; b2; b1; b0; b]) in H.
|
|
|
|
|
|
|
|
assert (even (length (hd ++ [b; b0; b1; b2; b3; b4; b5])) = true).
|
|
|
|
rewrite <- Nat.div_exact in K. rewrite K. rewrite Nat.even_mul.
|
|
|
|
reflexivity. easy.
|
|
|
|
assert (odd (length hd) = true). rewrite app_length in H0.
|
|
|
|
rewrite Nat.even_add in H0. simpl in H0. apply eqb_prop in H0.
|
|
|
|
rewrite <- Nat.negb_even. rewrite H0. reflexivity.
|
|
|
|
assert (length hd mod 4 = 1 \/ length hd mod 4 = 3).
|
|
|
|
apply odd_mod4. assumption.
|
|
|
|
destruct H2.
|
|
|
|
|
|
|
|
assert (b3 = b4).
|
|
|
|
replace (hd ++ [b; b0; b1; b2; b3; b4; b5]
|
|
|
|
++ [b5; b4; b3; b2; b1; b0; b] ++ tl)
|
|
|
|
with ((hd ++ [b; b0]) ++ [b1; b2; b3; b4]
|
|
|
|
++ [b5; b5; b4; b3; b2; b1; b0; b] ++ tl) in H.
|
|
|
|
assert (length (hd ++ [b; b0]) mod 4 = 3).
|
|
|
|
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2.
|
|
|
|
reflexivity. easy.
|
|
|
|
assert (exists x, skipn 2 [b1; b2; b3; b4] = [x; x]).
|
|
|
|
generalize H3.
|
|
|
|
apply tm_step_factor4_3mod4 with (n' := n)
|
|
|
|
(y := [b5; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption.
|
|
|
|
reflexivity. destruct H4. inversion H4. reflexivity.
|
|
|
|
rewrite <- app_assoc. reflexivity. rewrite H3 in H.
|
|
|
|
|
|
|
|
assert (b4 <> b5).
|
|
|
|
replace (hd ++ [b; b0; b1; b2; b4; b4; b5]
|
|
|
|
++ [b5; b4; b4; b2; b1; b0; b] ++ tl)
|
|
|
|
with ((hd ++ [b; b0; b1; b2]) ++ [b4] ++ [b4] ++ [b5]
|
|
|
|
++ [b5; b4; b4; b2;b1;b0;b] ++ tl) in H.
|
|
|
|
apply tm_step_cubefree in H. destruct b4; destruct b5.
|
|
|
|
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
|
|
|
|
|
|
|
assert (b4 <> b2).
|
|
|
|
replace (hd ++ [b; b0; b1; b2; b4; b4; b5]
|
|
|
|
++ [b5; b4; b4; b2; b1; b0; b] ++ tl)
|
|
|
|
with ((hd ++ [b; b0; b1; b2; b4; b4; b5; b5])
|
|
|
|
++ [b4] ++ [b4] ++ [b2] ++ [b1;b0;b] ++ tl) in H.
|
|
|
|
apply tm_step_cubefree in H. destruct b4; destruct b2.
|
|
|
|
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
|
|
|
|
|
|
|
assert (b2 = b5). destruct b2; destruct b4; destruct b5.
|
|
|
|
contradiction H4. reflexivity. contradiction H5. reflexivity.
|
|
|
|
reflexivity. contradiction H4. reflexivity.
|
|
|
|
contradiction H4. reflexivity. reflexivity.
|
|
|
|
contradiction H5. reflexivity. contradiction H4. reflexivity.
|
|
|
|
rewrite H6 in H.
|
|
|
|
|
|
|
|
assert (b = b0).
|
|
|
|
replace (hd ++ [b; b0; b1; b5; b4; b4; b5]
|
|
|
|
++ [b5; b4; b4; b5; b1; b0; b] ++ tl)
|
|
|
|
with (hd ++ [b; b0; b1; b5]
|
|
|
|
++ [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl) in H.
|
|
|
|
assert (exists x, firstn 2 [b; b0; b1; b5] = [x; x]).
|
|
|
|
generalize H2.
|
|
|
|
apply tm_step_factor4_1mod4 with (n' := n)
|
|
|
|
(y := [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl). assumption.
|
|
|
|
reflexivity. destruct H7. inversion H7. reflexivity. reflexivity.
|
|
|
|
rewrite H7 in H.
|
|
|
|
|
|
|
|
assert ({b1=b5} + {~ b1=b5}). apply bool_dec. destruct H8. rewrite e in H.
|
|
|
|
replace (hd ++ [b0; b0; b5; b5; b4; b4; b5]
|
|
|
|
++ [b5; b4; b4; b5; b5; b0; b0] ++ tl)
|
|
|
|
with ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4]
|
|
|
|
++ [b5; b5; b4; b4] ++ [b5; b5; b0; b0] ++ tl) in H.
|
|
|
|
assert (even (length ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4])) = true).
|
|
|
|
assert (0 < length ([b5; b5; b4; b4])). apply Nat.lt_0_succ.
|
|
|
|
generalize H8. generalize H. apply tm_step_square_pos.
|
|
|
|
rewrite app_length in H8. rewrite app_length in H8.
|
|
|
|
rewrite <- Nat.add_assoc in H8. rewrite Nat.even_add in H8.
|
|
|
|
rewrite <- Nat.negb_odd in H8.
|
|
|
|
rewrite H1 in H8. inversion H8. rewrite <- app_assoc. reflexivity.
|
|
|
|
|
|
|
|
assert (b1 = b4). destruct b1; destruct b4; destruct b5.
|
|
|
|
reflexivity. reflexivity. contradiction n0. reflexivity.
|
|
|
|
contradiction H4. reflexivity. contradiction H4. reflexivity.
|
|
|
|
contradiction n0. reflexivity. reflexivity. reflexivity.
|
|
|
|
rewrite H8 in H.
|
|
|
|
|
|
|
|
assert (b0 <> b4).
|
|
|
|
replace (hd ++ [b0; b0; b4; b5; b4; b4; b5]
|
|
|
|
++ [b5; b4; b4; b5; b4; b0; b0] ++ tl)
|
|
|
|
with (hd ++ [b0] ++ [b0] ++ [b4]
|
|
|
|
++ [b5;b4;b4;b5;b5; b4; b4; b5; b4; b0; b0] ++ tl) in H.
|
|
|
|
apply tm_step_cubefree in H. destruct b0; destruct b4.
|
|
|
|
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_1. reflexivity.
|
|
|
|
|
|
|
|
assert (b0 = b5). destruct b0; destruct b4; destruct b5.
|
|
|
|
reflexivity. contradiction H9. reflexivity. reflexivity.
|
|
|
|
contradiction H4. reflexivity. contradiction H4. reflexivity.
|
|
|
|
reflexivity. contradiction H9. reflexivity. reflexivity.
|
|
|
|
rewrite H10 in H.
|
|
|
|
|
|
|
|
assert (b5 = negb b4). destruct b4; destruct b5.
|
|
|
|
contradiction H4. reflexivity. reflexivity. reflexivity.
|
|
|
|
contradiction H4. reflexivity. rewrite H11 in H.
|
|
|
|
|
|
|
|
exists b4. rewrite H3. rewrite H6. rewrite H7. rewrite H8. rewrite H10.
|
|
|
|
rewrite H11. reflexivity.
|
|
|
|
rewrite app_length in K. rewrite <- Nat.add_mod_idemp_l in K.
|
|
|
|
rewrite H2 in K. inversion K. easy. reflexivity.
|
|
|
|
inversion I.
|
|
|
|
Qed.
|
|
|
|
|
2023-02-02 15:00:26 -05:00
|
|
|
Lemma tm_step_palindrome_8_destruct :
|
2023-02-02 04:22:38 -05:00
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> length a = 8
|
2023-02-02 14:59:25 -05:00
|
|
|
-> exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x].
|
2023-02-02 04:22:38 -05:00
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
|
|
|
|
(*
|
2023-02-02 04:22:38 -05:00
|
|
|
assert (J: length a mod 4 = 0). rewrite I. reflexivity.
|
|
|
|
assert (K := J).
|
|
|
|
rewrite tm_step_palindromic_length_12_prefix
|
|
|
|
with (n := n) (hd := hd) (tl := tl) in K.
|
2023-02-02 12:44:05 -05:00
|
|
|
assert (L: even (length hd) = true).
|
|
|
|
rewrite <- Nat.div_exact in K. rewrite K.
|
|
|
|
rewrite Nat.even_mul. reflexivity. easy.
|
2023-02-03 02:53:31 -05:00
|
|
|
*)
|
2023-02-02 04:22:38 -05:00
|
|
|
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
destruct a. inversion I. destruct a. inversion I.
|
|
|
|
|
|
|
|
destruct a.
|
|
|
|
replace (rev [b; b0; b1; b2; b3; b4; b5; b6])
|
|
|
|
with ([b6; b5; b4; b3; b2; b1; b0; b]) in H.
|
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
assert (exists x, [b0; b1; b2; b3; b4; b5; b6]
|
|
|
|
= [negb x; negb x; x; negb x; x; x; negb x]).
|
|
|
|
apply tm_step_palindrome_7_destruct
|
|
|
|
with (n := n) (hd := hd ++ [b]) (tl := [b] ++ tl).
|
|
|
|
rewrite <- app_assoc. assumption. reflexivity.
|
2023-02-02 04:22:38 -05:00
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
destruct H0. inversion H0. rewrite H2 in H. rewrite H3 in H.
|
|
|
|
rewrite H4 in H. rewrite H5 in H. rewrite H6 in H. rewrite H7 in H.
|
|
|
|
rewrite H8 in H.
|
2023-02-01 10:39:17 -05:00
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
assert ({b=x} + {~ b=x}). apply bool_dec. destruct H1.
|
|
|
|
exists x. rewrite e. reflexivity.
|
|
|
|
assert (b = negb x). destruct b; destruct x.
|
|
|
|
contradiction n0. reflexivity. reflexivity. reflexivity.
|
|
|
|
contradiction n0. reflexivity.
|
|
|
|
rewrite H1 in H.
|
|
|
|
replace (hd ++ [negb x; negb x; negb x; x; negb x; x; x; negb x] ++
|
|
|
|
[negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl)
|
|
|
|
with (hd ++ [negb x] ++ [negb x] ++ [negb x]
|
|
|
|
++ [x; negb x; x; x; negb x;
|
|
|
|
negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl) in H.
|
2023-02-02 12:48:40 -05:00
|
|
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
|
|
|
apply Nat.lt_0_1. reflexivity.
|
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
reflexivity. inversion I.
|
2023-02-02 14:59:25 -05:00
|
|
|
Qed.
|
|
|
|
|
2023-02-02 15:28:19 -05:00
|
|
|
|
2023-02-03 10:35:31 -05:00
|
|
|
Lemma tm_step_palindrome_mod8 :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length (hd ++ a) mod 8 = 0.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I. assert (Z := H).
|
|
|
|
|
|
|
|
assert (X : 3 < n). rewrite Nat.pow_lt_mono_r_iff with (a := 2).
|
|
|
|
simpl. rewrite <- tm_size_power2. rewrite H.
|
|
|
|
rewrite app_length. rewrite Nat.add_comm. rewrite app_length.
|
|
|
|
rewrite app_length. rewrite Nat.add_assoc.
|
|
|
|
assert (6+6 < length a + length (rev a)). rewrite rev_length.
|
|
|
|
apply Nat.add_lt_mono; assumption.
|
|
|
|
assert (length a + length (rev a)
|
|
|
|
<= length a + length (rev a) + length tl + length hd).
|
|
|
|
rewrite <- Nat.add_assoc. apply Nat.le_add_r.
|
|
|
|
assert (6+6 < length a + length (rev a) + length tl + length hd).
|
|
|
|
generalize H1. generalize H0. apply Nat.lt_le_trans.
|
|
|
|
replace (6+6) with 12 in H2.
|
|
|
|
apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2.
|
|
|
|
apply Nat.lt_succ_l in H2. apply Nat.lt_succ_l in H2. assumption.
|
|
|
|
reflexivity. apply Nat.lt_1_2.
|
|
|
|
|
|
|
|
assert (N: length (hd ++ a) mod 4 = 0). generalize I. generalize H.
|
|
|
|
apply tm_step_palindromic_length_12.
|
|
|
|
|
|
|
|
assert (O: length (hd++a) mod 8 = 0 \/ length (hd++a) mod 8 = 4).
|
|
|
|
assert (length (hd ++ a) mod (4*2)
|
|
|
|
= (length (hd ++ a) mod 4 + 4 * (length (hd ++ a) / 4 mod 2))).
|
|
|
|
apply Nat.mod_mul_r. easy. easy.
|
|
|
|
rewrite N in H0. rewrite <- Nat.bit0_mod in H0.
|
|
|
|
replace (4*2) with 8 in H0. rewrite Nat.add_0_l in H0.
|
|
|
|
destruct (Nat.testbit (length (hd ++ a) / 4)).
|
|
|
|
right. apply H0. left. apply H0. reflexivity.
|
|
|
|
|
|
|
|
assert (J: firstn (length a - 7) a ++ skipn (length a - 7) a = a).
|
|
|
|
apply firstn_skipn. rewrite <- J in H. rewrite rev_app_distr in H.
|
|
|
|
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
|
|
|
|
|
|
|
|
assert (K: exists x, skipn (length a - 7) a
|
|
|
|
= [negb x; negb x; x; negb x; x; x; negb x]).
|
|
|
|
assert (length (skipn (length a - 7) a) = 7). rewrite skipn_length.
|
|
|
|
assert ((length a - 7) - (length a - 7) = 0). apply Nat.sub_diag.
|
|
|
|
rewrite <- Nat.add_cancel_r with (p := 7) in H0.
|
|
|
|
rewrite <- Nat.add_sub_swap in H0. rewrite <- Nat.add_sub_swap in H0.
|
|
|
|
rewrite Nat.add_sub in H0. assumption. apply Nat.le_succ_l. assumption.
|
|
|
|
apply Nat.le_refl. generalize H0. rewrite app_assoc in H. generalize H.
|
|
|
|
apply tm_step_palindrome_7_destruct.
|
|
|
|
destruct K. rewrite H0 in H.
|
|
|
|
|
|
|
|
destruct O as [O | O]. assumption.
|
|
|
|
assert (nth_error (tm_step 3) 3 = nth_error (tm_step 3) 4
|
|
|
|
<-> nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 3)
|
|
|
|
= nth_error (tm_step (3 + (n-3))) ((length (hd ++ a) / 8) * 2^3 + 4)).
|
|
|
|
apply tm_step_repeating_patterns. 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 := length (hd ++ a) mod 8).
|
|
|
|
rewrite <- Nat.div_mod_eq. rewrite O.
|
|
|
|
|
|
|
|
replace 8 with (2*2*2).
|
|
|
|
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
|
|
|
|
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_succ_r.
|
|
|
|
rewrite <- Nat.pow_succ_r. rewrite <- Nat.sub_succ_l.
|
|
|
|
rewrite <- Nat.sub_succ_l. rewrite <- Nat.sub_succ_l.
|
|
|
|
replace (S (S (S n))) with (n + 3). rewrite Nat.add_sub.
|
|
|
|
|
|
|
|
assert (length (hd++a) <= length (tm_step n)).
|
|
|
|
rewrite Z. rewrite app_assoc.
|
|
|
|
replace (length ((hd ++ a) ++ rev a ++ tl))
|
|
|
|
with (length (hd ++ a) + length ((rev a) ++ tl)).
|
|
|
|
apply Nat.le_add_r. symmetry. rewrite app_length. reflexivity.
|
|
|
|
|
|
|
|
assert (length (tm_step n) < 2^n + 4). rewrite tm_size_power2.
|
|
|
|
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
|
|
|
|
|
|
|
|
generalize H2. generalize H1. apply Nat.le_lt_trans.
|
|
|
|
rewrite Nat.add_comm. reflexivity.
|
|
|
|
apply le_S. apply le_S. apply Nat.lt_le_incl. assumption.
|
|
|
|
apply le_S. apply Nat.lt_le_incl. assumption.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
apply le_S. apply le_S. apply Nat.lt_le_incl.
|
|
|
|
rewrite Nat.add_lt_mono_r with (p := 3).
|
|
|
|
rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
apply le_S. apply Nat.lt_le_incl.
|
|
|
|
rewrite Nat.add_lt_mono_r with (p := 3).
|
|
|
|
rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
apply Nat.lt_le_incl.
|
|
|
|
rewrite Nat.add_lt_mono_r with (p := 3).
|
|
|
|
rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. assumption.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
reflexivity. apply Nat.lt_0_succ.
|
|
|
|
|
|
|
|
replace (3 + (n-3)) with n in H1.
|
|
|
|
|
|
|
|
assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 3) = Some (negb x)).
|
|
|
|
rewrite H. rewrite app_assoc. rewrite nth_error_app2.
|
|
|
|
|
|
|
|
rewrite Nat.mul_comm. replace (2^3) with 8.
|
|
|
|
replace 3 with (length (hd++a) mod 8 - 1) at 4.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq.
|
|
|
|
rewrite app_length. rewrite app_length.
|
|
|
|
rewrite firstn_length_le.
|
|
|
|
rewrite <- Nat.add_sub_assoc.
|
|
|
|
replace (length a - 1) with (6 + length a - 7).
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_assoc.
|
|
|
|
rewrite <- Nat.add_sub_assoc.
|
|
|
|
replace (length hd + 6) with (6 + length hd).
|
|
|
|
rewrite <- Nat.add_assoc. rewrite Nat.add_sub. simpl. reflexivity.
|
|
|
|
rewrite Nat.add_comm. reflexivity. apply Nat.le_succ_l. assumption.
|
|
|
|
rewrite Nat.le_succ_l. rewrite <- Nat.add_0_l at 1.
|
|
|
|
apply Nat.add_lt_mono. apply Nat.lt_0_succ. assumption.
|
|
|
|
|
|
|
|
rewrite Nat.add_comm.
|
|
|
|
rewrite Nat.add_sub_swap. replace 6 with (7 - 1) at 2.
|
|
|
|
rewrite <- Nat.add_sub_swap.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
|
|
|
rewrite Nat.add_sub. reflexivity.
|
|
|
|
|
|
|
|
rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. assumption.
|
|
|
|
|
|
|
|
apply Nat.le_succ_l. apply Nat.lt_0_succ.
|
|
|
|
apply Nat.le_succ_l. assumption. reflexivity.
|
|
|
|
apply Nat.le_succ_l. assumption.
|
|
|
|
|
|
|
|
rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. assumption.
|
|
|
|
|
|
|
|
apply Nat.le_sub_l. rewrite O.
|
|
|
|
apply Nat.le_succ_l. apply Nat.lt_0_succ.
|
|
|
|
rewrite O. reflexivity. reflexivity.
|
|
|
|
|
|
|
|
rewrite Nat.mul_comm. replace (2^3) with 8.
|
|
|
|
replace 3 with (length (hd++a) mod 8 - 1) at 4.
|
|
|
|
rewrite Nat.add_sub_assoc. rewrite <- Nat.div_mod_eq.
|
|
|
|
rewrite app_length. rewrite app_length.
|
|
|
|
rewrite <- Nat.add_sub_assoc. rewrite <- Nat.add_le_mono_l.
|
|
|
|
rewrite firstn_length_le.
|
|
|
|
apply Nat.sub_le_mono_l. apply Nat.le_succ_l. apply Nat.lt_0_succ.
|
|
|
|
rewrite <- Nat.sub_0_r.
|
|
|
|
apply Nat.sub_le_mono_l. apply le_0_n.
|
|
|
|
|
|
|
|
rewrite Nat.le_succ_l. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
|
|
|
apply Nat.lt_succ_l in I. assumption.
|
|
|
|
|
|
|
|
rewrite O. apply Nat.le_succ_l. apply Nat.lt_0_succ.
|
|
|
|
rewrite O. reflexivity. reflexivity.
|
|
|
|
|
|
|
|
assert (nth_error (tm_step n) (length (hd ++ a)/8 * 2^3 + 4) = Some (negb x)).
|
|
|
|
rewrite H. rewrite app_assoc. rewrite app_assoc. rewrite app_assoc.
|
|
|
|
rewrite nth_error_app1.
|
|
|
|
|
|
|
|
rewrite Nat.mul_comm. replace (2^3) with 8.
|
|
|
|
replace 4 with (length (hd++a) mod 8) at 4.
|
|
|
|
rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1.
|
|
|
|
rewrite nth_error_app2. rewrite <- app_assoc. rewrite firstn_skipn.
|
|
|
|
rewrite Nat.sub_diag. reflexivity.
|
|
|
|
rewrite <- app_assoc. rewrite firstn_skipn. apply Nat.le_refl.
|
|
|
|
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
rewrite Nat.mul_comm. replace (2^3) with 8.
|
|
|
|
replace 4 with (length (hd++a) mod 8) at 3.
|
|
|
|
rewrite <- Nat.div_mod_eq. rewrite <- H0 at 1.
|
|
|
|
replace ((hd ++ firstn (length a - 7) a) ++ skipn (length a - 7) a)
|
|
|
|
with (hd ++ firstn (length a - 7) a ++ skipn (length a - 7) a).
|
|
|
|
rewrite firstn_skipn.
|
|
|
|
replace (length ((hd ++ a) ++ rev [negb x; negb x; x; negb x; x; x; negb x]))
|
|
|
|
with (length (hd ++ a)
|
|
|
|
+ length (rev [negb x; negb x; x; negb x; x; x; negb x])).
|
|
|
|
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
|
|
|
|
rewrite app_length. rewrite app_length. rewrite app_length. reflexivity.
|
|
|
|
rewrite <- app_assoc. reflexivity. reflexivity.
|
|
|
|
|
|
|
|
rewrite H2 in H1. rewrite H3 in H1. simpl in H1.
|
2023-02-03 11:21:27 -05:00
|
|
|
destruct H1. assert (Some false = Some true).
|
|
|
|
apply H4. reflexivity. inversion H5.
|
2023-02-03 10:35:31 -05:00
|
|
|
|
2023-02-03 11:21:27 -05:00
|
|
|
rewrite Nat.add_comm.
|
|
|
|
rewrite Nat.sub_add. reflexivity.
|
|
|
|
apply Nat.lt_le_incl. assumption.
|
|
|
|
Qed.
|
2023-02-03 10:35:31 -05:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-02-02 15:28:19 -05:00
|
|
|
Lemma tm_step_palindrome_8_mod8 :
|
|
|
|
forall (n : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> length a = 8
|
|
|
|
-> length (hd ++ a) mod 8 = 0.
|
|
|
|
Proof.
|
|
|
|
intros n hd a tl. intros H I.
|
|
|
|
|
|
|
|
assert (J: length a mod 4 = 0). rewrite I. reflexivity.
|
|
|
|
assert (K := J).
|
|
|
|
rewrite tm_step_palindromic_length_12_prefix
|
|
|
|
with (n := n) (hd := hd) (tl := tl) in K.
|
|
|
|
assert (L: even (length hd) = true).
|
|
|
|
rewrite <- Nat.div_exact in K. rewrite K.
|
|
|
|
rewrite Nat.even_mul. reflexivity. easy.
|
|
|
|
|
|
|
|
assert (M: exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x]).
|
|
|
|
generalize I. generalize H. apply tm_step_palindrome_8_destruct.
|
|
|
|
destruct M as [x M].
|
|
|
|
|
2023-02-03 02:53:31 -05:00
|
|
|
assert (N: length (hd ++ a) mod 4 = 0).
|
|
|
|
rewrite app_length. rewrite Nat.add_mod.
|
|
|
|
rewrite J. rewrite K. reflexivity. easy.
|
|
|
|
|
|
|
|
assert (O: length (hd++a) mod 8 = 0 \/ length (hd++a) mod 8 = 4).
|
|
|
|
assert (length (hd ++ a) mod (4*2)
|
|
|
|
= (length (hd ++ a) mod 4 + 4 * (length (hd ++ a) / 4 mod 2))).
|
|
|
|
apply Nat.mod_mul_r. easy. easy.
|
|
|
|
rewrite N in H0. rewrite <- Nat.bit0_mod in H0.
|
|
|
|
replace (4*2) with 8 in H0. rewrite Nat.add_0_l in H0.
|
|
|
|
destruct (Nat.testbit (length (hd ++ a) / 4)).
|
|
|
|
right. apply H0. left. apply H0. reflexivity.
|
|
|
|
|
|
|
|
destruct O as [O | O]. assumption.
|
|
|
|
|
2023-02-02 15:28:19 -05:00
|
|
|
|
|
|
|
|
2023-02-01 12:44:14 -05:00
|
|
|
(*
|
2023-01-27 13:32:41 -05:00
|
|
|
Lemma tm_step_proper_palindrome_center :
|
|
|
|
forall (m n k : nat) (hd a tl : list bool),
|
|
|
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
|
|
|
-> 6 < length a
|
|
|
|
-> length a = 2^(Nat.double m) (* palindrome non propre *)
|
|
|
|
-> skipn (length hd - length a) hd = rev (firstn (length a) tl).
|
2023-02-01 12:44:14 -05:00
|
|
|
*)
|