From a59cfa8944725a8c0a73e3940962bf074e21fbdc Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Thu, 26 Jan 2023 10:08:29 +0100
Subject: [PATCH] Update

---
 src/thue_morse3.v | 62 +++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 60 insertions(+), 2 deletions(-)

diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index e72b833..e7059ae 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -2,7 +2,10 @@
 
    TODO
 
-   tm_step_rev
+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 :
 *)
 
 Require Import thue_morse.
@@ -1248,7 +1251,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
 Qed.
 
 
-Lemma tm_step_palindromic_length_12 :
+Theorem tm_step_palindromic_length_12 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ rev a ++ tl
   -> 6 < length a
@@ -1354,6 +1357,61 @@ Proof.
 Qed.
 
 
+Theorem tm_step_palindromic_length_12_prefix :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> length a > 6
+  -> 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.
+
+
+Lemma tm_step_palindromic_even_morphism1 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> 0 < length a
+  -> even (length a) = true
+  -> 11= 42.
+Proof.
+  intros n hd a tl. intros H I J.
+  destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
+  apply Nat.le_refl.
+  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 I. inversion I.
+
+  assert (even (length (hd ++ a)) = true). generalize I. generalize H.
+  apply tm_step_palindromic_even_center.
+
+  assert (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.
+
+  rewrite <- tm_step_lemma in H.
+  assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
+  generalize H1. generalize H. apply tm_morphism_app2.
+
+
+
+
+
+
+
+
+