Update

src/thue_morse.v

@@ -97,6 +97,21 @@ Proof.
   apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l.
 Qed.
 
+Lemma app_eq_length_head : forall x0 x1 y0 y1 : list bool,
+    x0 ++ x1 = y0 ++ y1 -> length x0 = length y0 -> x0 = y0.
+Proof.
+  intro x0. induction x0. destruct y0. intros. reflexivity.
+  intros. inversion H0. destruct y0. intros. inversion H0.
+  intros. simpl in H0. apply Nat.succ_inj in H0.
+  rewrite <- app_comm_cons in H.
+  rewrite <- app_comm_cons in H.
+
+  destruct a; destruct b. inversion H.
+  apply IHx0 with (x1 := x1) (y1 := y1) in H2. rewrite H2. reflexivity.
+  assumption. inversion H. inversion H. inversion H.
+  apply IHx0 with (x1 := x1) (y1 := y1) in H2. rewrite H2. reflexivity.
+  assumption.
+Qed.
 
 (**
    Some lemmas related to the first function (tm_morphism) are proved here.

src/thue_morse3.v

@@ -177,24 +177,9 @@ Proof.
   rewrite rev_app_distr in I. rewrite rev_app_distr in I.
   rewrite <- app_assoc in I.
 
-  assert (forall x0 x1 y0 y1 : list bool,
-    x0 ++ x1 = y0 ++ y1 -> length x0 = length y0 -> x0 = y0).
-
-  intro x0. induction x0. destruct y0. intros. reflexivity.
-  intros. inversion H7. destruct y0. intros. inversion H7.
-  intros. simpl in H7. apply Nat.succ_inj in H7.
-  rewrite <- app_comm_cons in H6.
-  rewrite <- app_comm_cons in H6.
-
-  destruct a0; destruct b. inversion H6.
-  apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
-  assumption. inversion H6. inversion H6. inversion H6.
-  apply IHx0 with (x1 := x1) (y1 := y1) in H7. rewrite H7. reflexivity.
-  assumption.
-
   assert (u = rev w). generalize H5. rewrite <- rev_length with (l := w).
-  generalize I. apply H6.
-  rewrite H7 in I. rewrite rev_involutive in I.
+  generalize I. apply app_eq_length_head.
+  rewrite H6 in I. rewrite rev_involutive in I.
   apply app_inv_head in I. apply app_inv_tail in I. assumption.
 
   assert (length v <> 5).
@@ -275,11 +260,136 @@ Proof.
 Qed.
 
 
+Lemma tm_step_palindromic_full : forall (n : nat),
+  tm_step (Nat.double (S n)) =
+    (tm_step (S (Nat.double n))) ++ rev (tm_step (S (Nat.double n))).
+Proof.
+  intro n. induction n.
+  - reflexivity.
+  - rewrite Nat.double_S. rewrite tm_build. rewrite app_inv_head_iff.
+    rewrite <- tm_step_lemma. rewrite IHn.
+
+    rewrite tm_morphism_rev. rewrite tm_morphism_app. rewrite rev_app_distr.
+    rewrite map_app. rewrite map_app. rewrite tm_morphism_app.
+    rewrite rev_involutive. rewrite tm_build_negb. rewrite tm_build_negb.
+    reflexivity.
+Qed.
+
+
+(*
+Lemma tm_step_palindromic_even_seed :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step (S n) = hd ++ a ++ (rev a) ++ tl
+  -> 0 < length a
+  -> (2^n <= length hd) \/ (2^n <= length tl) \/ (length (hd ++a) = 2^n).
+Proof.
+  intro n. induction n.
+  - intros hd a tl. intros H I. destruct a.
+    + inversion I.
+    + destruct a.
+      assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
+      rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
+      rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
+      apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
+      destruct hd; destruct tl. right. right. reflexivity.
+      right. left. simpl. apply le_n_S. apply le_0_n.
+      rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
+      contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
+      assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
+      rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
+      rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
+      apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
+      rewrite app_length in H0. rewrite app_length in H0.
+      rewrite app_length in H0. simpl in H0.
+      rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
+      rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
+      rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
+  - intros hd a tl. intros H I. rewrite tm_build in H.
+    assert (2^S n <= length hd \/ length hd < 2^S n). apply Nat.le_gt_cases.
+    assert (2^S n <= length tl \/ length tl < 2^S n). apply Nat.le_gt_cases.
+    destruct H0. left. assumption. destruct H1. right. left. assumption.
+    right. right.
+    assert (2^S n <= length (hd++a) \/ length (hd++a) < 2^S n).
+    apply Nat.le_gt_cases. destruct H2. apply Nat.lt_eq_cases in H2.
+    destruct H2.
+    pose (c := length (hd ++ a) - 2^ S n). (* ce qui dépasse, excès de a *)
+    pose (d := skipn ((length a) - c) a). (* on cherche le milieu de tm_step S (S n) *)
+    pose (e := d ++ firstn c (rev a)).
+    (* TODO e = rev e est-il vraiment utile ??? *)
+    assert (e = rev e). (* nouveau palindrome dans la seconde moitié *)
+    unfold e. unfold d.
+    rewrite firstn_rev. rewrite rev_app_distr. rewrite rev_involutive.
+    reflexivity.
+
+    (* montrer que e est dans la seconde moitié, excentré *)
+    assert (a = (firstn (length a - c) a) ++ d). unfold d.
+    symmetry. apply firstn_skipn.
+
+    rewrite H4 in H. rewrite <- app_assoc in H. rewrite rev_app_distr in H.
+    rewrite <- app_assoc in H. rewrite app_assoc in H.
+
+    assert (length hd + length a - 2 ^ S n <= length a).
+    rewrite Nat.add_le_mono_r with (p := 2^S n).
+    rewrite Nat.sub_add. rewrite Nat.add_comm at 1.
+    rewrite <- Nat.add_le_mono_l. apply Nat.lt_le_incl. assumption.
+    rewrite <- app_length. apply Nat.lt_le_incl. assumption.
+
+    assert (length (tm_step (S n)) = length (hd ++ firstn (length a - c) a)).
+    unfold c. rewrite app_length. rewrite tm_size_power2.
+    rewrite firstn_length_le. rewrite app_length.
+    rewrite Nat.add_sub_assoc.
+
+    replace (length hd + length a)
+      with (length hd + length a - 2^S n + 2^S n) at 1.
+    rewrite Nat.add_sub_swap. rewrite <- Nat.add_0_l at 1.
+    rewrite Nat.add_cancel_r. symmetry. apply Nat.sub_diag.
+    apply Nat.le_refl. rewrite <- Nat.add_sub_swap.
+    rewrite Nat.add_sub. reflexivity. apply Nat.lt_le_incl.
+    rewrite <- app_length. assumption. assumption.
+
+    apply Nat.le_sub_le_add_r. rewrite <- Nat.add_0_r at 1.
+    rewrite <- Nat.add_le_mono_l. apply le_0_n.
+
+    assert (tm_step (S n) = hd ++ firstn (length a - c) a).
+    generalize H6. generalize H.
+    apply app_eq_length_head. rewrite <- H7 in H.
+    apply app_inv_head in H.
+
+
+
+    assert (map negb (tm_step (S n)) = e ++ ??? ++ tl). unfold e. unfold d.
+
+
+
+
+
+
+
+
+
+  intros n hd a tl. intros H I.
+  induction n.
+  - right. right. destruct a. inversion I. destruct a.
+    assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
+    rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
+    rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
+    apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
+    destruct hd; destruct tl. reflexivity. reflexivity.
+    rewrite Nat.add_0_r in H0. simpl in H0. apply O_S in H0.
+    contradiction H0. simpl in H0. apply O_S in H0. contradiction H0.
+    assert (length (tm_step 1) = length (tm_step 1)). reflexivity.
+    rewrite H in H0 at 2. rewrite app_length in H0. simpl in H0.
+    rewrite Nat.add_succ_r in H0. rewrite Nat.add_succ_r in H0.
+    apply Nat.succ_inj in H0. apply Nat.succ_inj in H0.
+    rewrite app_length in H0. rewrite app_length in H0.
+    rewrite app_length in H0. simpl in H0.
+    rewrite Nat.add_succ_r in H0. rewrite Nat.add_0_r in H0.
+    rewrite Nat.add_succ_l in H0. rewrite Nat.add_succ_r in H0.
+    rewrite Nat.add_succ_r in H0. apply O_S in H0. contradiction H0.
+  -
   
 
-
-
-  (* TODO: voir si une preuve du lemme précédent est plus rapide comme ceci *)
+ *)
 
 
 (*