Update

src/thue_morse.v

@@ -1012,30 +1012,10 @@ Proof.
 Qed.
 
 
-Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
+Lemma tm_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool),
-  tm_step n = hd ++ a ++ tl
-  -> length a = 4 -> odd (length hd) = true
-  -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
-Proof.
-  intros n hd a tl. intros H I J.
-
-  assert (K: 1 = (length hd) mod 2).
-  apply Nat.mod_unique with (q := Nat.div2 (length hd)). apply Nat.lt_1_2.
-  replace (1) with (Nat.b2n (Nat.odd (length hd))) at 2.
-  apply Nat.div2_odd. rewrite J.  reflexivity.
-
-  assert (L: (length hd) mod (2*2)
-    = (length hd) mod 2 + 2 * (((length hd) / 2) mod 2)).
-  apply Nat.mod_mul_r; easy. rewrite <- K in L.
-  replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
-
-  assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3). rewrite L.
-  destruct (Nat.testbit (length hd / 2) 0) ; [right | left] ; reflexivity.
-
-  assert (forall (n' : nat) (w z y : list bool),
     tm_step n' = w ++ z ++ y
     -> length z = 4 -> length w mod 4 = 1
-    -> exists (x : bool), firstn 2 z = [x;x]).
+    -> exists (x : bool), firstn 2 z = [x;x].
   intros n' w z y. intros G0 G1 G2.
   assert (U: 4 * (length w / 4) <= length w).
   apply Nat.mul_div_le. easy.
@@ -1070,11 +1050,11 @@ Proof.
   rewrite nth_error_app1 in O. rewrite nth_error_app2 in O.
   rewrite Nat.sub_succ_l in O. rewrite Nat.sub_diag in O.
   rewrite nth_error_app1 in O. destruct O.
-  assert (nth_error z 0 = nth_error z 1). apply H0. reflexivity.
+  assert (nth_error z 0 = nth_error z 1). apply H. reflexivity.
-  rewrite nth_error_nth' with (d := false) in H2.
+  rewrite nth_error_nth' with (d := false) in H1.
-  rewrite nth_error_nth' with (d := false) in H2.
+  rewrite nth_error_nth' with (d := false) in H1.
-  exists (nth 0 z false). inversion H2.
+  exists (nth 0 z false). inversion H1.
-  rewrite H4 at 2.
+  rewrite H3 at 2.
   destruct z. inversion G1. destruct z. inversion G1. reflexivity.
   rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
   rewrite G1. apply Nat.lt_0_succ.
@@ -1085,53 +1065,87 @@ Proof.
   reflexivity. easy. assumption.
   rewrite Nat.add_succ_r. rewrite <- Nat.div_mod_eq. reflexivity.
   reflexivity. apply Nat.lt_1_2. reflexivity.
+Qed.
+
+Lemma tm_step_factor4_3mod4 : forall (n' : nat) (w z y : list bool),
+    tm_step n' = w ++ z ++ y
+    -> length z = 4 -> length w mod 4 = 3
+    -> exists (x : bool), skipn 2 z = [x;x].
+Proof.
+  intros n hd a tl. intros H I M.
+  assert ((length (hd ++ (firstn 2 a))) mod 4 = 1).
+  rewrite app_length. rewrite firstn_length. rewrite I.
+  rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy.
+  assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)).
+  apply tm_build. rewrite H in H1.
+  assert (length ((skipn 2 a)
+    ++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4).
+  rewrite app_length. rewrite skipn_length. rewrite I.
+  rewrite firstn_length. rewrite app_length. rewrite <- H.
+  rewrite map_length.
+  assert (4 <= length tl + length (tm_step n)).
+  assert (Q: length a <= length (tm_step n)). rewrite H.
+  rewrite app_length. rewrite app_length.
+  rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
+  apply Nat.le_add_l. rewrite I in Q.
+  rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
+  apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity.
+  assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l.
+  generalize H2. generalize H3. apply Nat.le_trans.
+  replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl))
+    with ((hd ++ firstn 2 a)
+      ++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
+      ++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H1.
+  assert (exists (x : bool), 
+    firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
+    = [x;x]).
+  generalize H0. generalize H2. generalize H1. apply tm_step_factor4_1mod4.
+  destruct H3. exists x.
+  rewrite <- H3. rewrite firstn_app. rewrite skipn_length. rewrite I.
+  replace (2 - (4 - 2)) with 0. rewrite firstn_O.
+  rewrite app_nil_r.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. reflexivity. inversion I.
+  reflexivity.
+  rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
+  apply app_inv_head_iff.
+  rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
+  rewrite firstn_skipn.
+  rewrite <- firstn_skipn with (n := 2) (l := a) at 4.
+  rewrite <- app_assoc. reflexivity.
+Admitted.
+
+
+Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl
+  -> length a = 4 -> odd (length hd) = true
+  -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
+Proof.
+  intros n hd a tl. intros H I J.
+
+  assert (K: 1 = (length hd) mod 2).
+  apply Nat.mod_unique with (q := Nat.div2 (length hd)). apply Nat.lt_1_2.
+  replace (1) with (Nat.b2n (Nat.odd (length hd))) at 2.
+  apply Nat.div2_odd. rewrite J.  reflexivity.
+
+  assert (L: (length hd) mod (2*2)
+    = (length hd) mod 2 + 2 * (((length hd) / 2) mod 2)).
+  apply Nat.mod_mul_r; easy. rewrite <- K in L.
+  replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
+
+  assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3). rewrite L.
+  destruct (Nat.testbit (length hd / 2) 0) ; [right | left] ; reflexivity.
 
   destruct M as [M | M].
   - assert (exists (x : bool), firstn 2 a = [x;x]).
-    generalize M. generalize I. generalize H. apply H0.
+    generalize M. generalize I. generalize H. apply tm_step_factor4_1mod4.
-    destruct H1. exists x. exists nil. exists (skipn 2 a).
+    destruct H0. exists x. exists nil. exists (skipn 2 a).
-    rewrite app_nil_l. rewrite <- H1. symmetry. apply firstn_skipn.
+    rewrite app_nil_l. rewrite <- H0. symmetry. apply firstn_skipn.
-  - assert ((length (hd ++ (firstn 2 a))) mod 4 = 1).
+  - assert (exists (x : bool), skipn 2 a = [x;x]).
-    rewrite app_length. rewrite firstn_length. rewrite I.
+    generalize M. generalize I. generalize H. apply tm_step_factor4_3mod4.
-    rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy.
+    destruct H0. exists x. exists (firstn 2 a). exists nil.
-    assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)).
+    rewrite app_nil_r. rewrite <- H0. symmetry. apply firstn_skipn.
-    apply tm_build. rewrite H in H2.
-    assert (length ((skipn 2 a)
-      ++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4).
-    rewrite app_length. rewrite skipn_length. rewrite I.
-    rewrite firstn_length. rewrite app_length. rewrite <- H.
-    rewrite map_length.
-    assert (4 <= length tl + length (tm_step n)).
-    assert (Q: length a <= length (tm_step n)). rewrite H.
-    rewrite app_length. rewrite app_length.
-    rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
-    apply Nat.le_add_l. rewrite I in Q.
-    rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
-    apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity.
-    assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l.
-    generalize H3. generalize H4. apply Nat.le_trans.
-    replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl))
-      with ((hd ++ firstn 2 a)
-        ++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
-        ++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H2.
-    assert (exists (x : bool), 
-      firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
-      = [x;x]).
-    generalize H1. generalize H3. generalize H2. apply H0.
-    destruct H4. exists x. exists (firstn 2 a). exists nil.
-    rewrite <- H4. rewrite firstn_app. rewrite skipn_length. rewrite I.
-    replace (2 - (4 - 2)) with 0. rewrite firstn_O.
-    rewrite app_nil_r. rewrite app_nil_r.
-    destruct a. inversion I. destruct a. inversion I.
-    destruct a. inversion I. destruct a. inversion I.
-    destruct a. reflexivity. inversion I.
-    reflexivity.
-    rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
-    apply app_inv_head_iff.
-    rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
-    rewrite firstn_skipn.
-    rewrite <- firstn_skipn with (n := 2) (l := a) at 4.
-    rewrite <- app_assoc. reflexivity.
   - reflexivity.
 Qed.
 

src/thue_morse3.v

@@ -280,6 +280,78 @@ Proof.
 Qed.
 
 
+Lemma tm_step_palindromic_negb_center :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ map negb (rev a) ++ tl
+  -> 1 < length a
+  -> even (length (hd ++ a)) = true.
+Proof.
+  intros n hd a tl. intros H I.
+  assert (J: a = firstn (length a - 2) a ++ skipn (length a - 2) a).
+  symmetry. apply firstn_skipn. rewrite J in H.
+  rewrite rev_app_distr in H. rewrite map_app in H.
+  rewrite <- app_assoc in H. rewrite <- app_assoc in H.
+  rewrite app_assoc in H.
+  replace ( skipn (length a - 2) a ++
+            map negb (rev (skipn (length a - 2) a)) ++
+            map negb (rev (firstn (length a - 2) a)) ++ tl )
+    with ( ( skipn (length a - 2) a ++
+             map negb (rev (skipn (length a - 2) a)) ) ++
+             map negb (rev (firstn (length a - 2) a)) ++ tl ) in H.
+
+  assert (length (skipn (length a - 2) a) = 2). rewrite skipn_length.
+  replace (length a) with (2 + (length a - 2)) at 1. rewrite Nat.add_sub.
+  reflexivity. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
+  rewrite Nat.sub_diag. reflexivity. easy. rewrite Nat.le_succ_l.
+  assumption.
+
+  assert (length
+    (skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a))) = 4).
+  rewrite app_length. rewrite map_length. rewrite rev_length.
+  rewrite H0. reflexivity.
+
+  assert (K: {even (length (hd ++ firstn (length a - 2) a))=true}
+         + {~ even (length (hd ++ firstn (length a - 2) a))=true}).
+  apply bool_dec. destruct K.
+  rewrite J. rewrite app_assoc. rewrite app_length. rewrite Nat.even_add.
+  rewrite e. rewrite H0. reflexivity. apply not_true_is_false in n0.
+
+  assert (exists (x : bool) (u v : list bool),
+     (skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a)))
+     = u ++ [x;x] ++ v).
+  assert (odd (length (hd ++ firstn (length a - 2) a)) = true).
+  rewrite <- Nat.negb_even. rewrite n0. reflexivity. generalize H2.
+  generalize H1. generalize H. apply tm_step_factor4_odd_prefix.
+
+  destruct H2. destruct H2. destruct H2. rewrite H2 in H1.
+  
+  destruct x0.
+  assert (skipn (length a - 2) a = [x;x]).
+  assert (length (skipn (length a - 2) a) = length ([x;x])). rewrite H0.
+  reflexivity. generalize H3. generalize H2. rewrite app_nil_l.
+  apply app_eq_length_head. rewrite H3 in H.
+
+  TODO contradiction en H
+    
+
+
+
+Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl
+  -> length a = 4 -> odd (length hd) = true
+  -> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
+
+
+
+  pose (hd' := hd ++ firstn (length a - 2) a).
+  pose (tl' := map negb (rev (firstn (length a - 2) a)) ++ tl).
+  pose (a' := skipn (length a - 2) a).
+  fold hd' in H. fold tl' in H. fold a' in H.
+  replace (a' ++ map negb (rev a') ++ tl')
+    with ((a' ++ map negb (rev a')) ++ tl') in H.
+  assert (length pat = 4).
+
+
 (**
    In this notebook I call "proper palindrome" in the Thue-Morse sequence,
    any palindromic subsequence such that the middle (of the palindromic
@@ -355,6 +427,8 @@ Proof.
     rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
     generalize H0. generalize H. apply tm_step_palindromic_even_center.
 
+    assert (H' := H).
+
     (* proof that 0 < n *)
     destruct n.
     assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
@@ -421,7 +495,7 @@ Proof.
                           (skipn (Nat.div2 (length hd)) (tm_step n)))).
     fold hd' in H. fold a' in H. fold tl' in H.
 
-    assert (length a' = 2^S (Nat.double m)). unfold a'.
+    assert (I': length a' = 2^S (Nat.double m)). unfold a'.
     rewrite firstn_length_le. rewrite I. rewrite Nat.double_S.
     rewrite Nat.pow_succ_r. rewrite Nat.div2_double. reflexivity.
     apply le_0_n. rewrite skipn_length.
@@ -429,10 +503,29 @@ Proof.
     rewrite Nat.mul_comm. rewrite <- Nat.add_0_r at 1.
     replace 0 with (Nat.b2n (Nat.odd (length a))) at 2.
     rewrite <- Nat.div2_odd. rewrite Nat.mul_sub_distr_r.
+    replace (length (tm_step n) * 2) with (length (tm_step (S n))).
+    replace (Nat.div2 (length hd) * 2) with (length hd).
+    rewrite H'. rewrite app_length. rewrite Nat.add_sub_swap.
+    rewrite Nat.sub_diag. simpl. rewrite app_length.
+    rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_le_mono_l.
+    apply Nat.le_0_l. apply Nat.le_refl.
+    rewrite Nat.mul_comm. symmetry. rewrite <- Nat.add_0_r at 1.
+    replace 0 with (Nat.b2n (Nat.odd (length hd))) at 2.
+    rewrite <- Nat.div2_odd. reflexivity.
+    rewrite <- Nat.negb_even. rewrite L. reflexivity.
+    rewrite tm_build. rewrite app_length. rewrite Nat.mul_comm.
+    simpl. rewrite Nat.add_0_r. rewrite map_length. reflexivity.
+    rewrite <- Nat.negb_even. rewrite K. reflexivity.
+    apply Nat.lt_0_2.
+
+    assert (K': even (length a') = true). rewrite I'.
+    rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
+    apply le_0_n.
 
 
-    re
+    (* montrer que length (hd'++a') est pair à l'aide de
-
+H : tm_step n = hd' ++ a' ++ map negb (rev a') ++ tl'
+     *)
 
 
 
@@ -807,6 +900,8 @@ Proof.
 
  *)
 
+ (* TODO: reprendre tous les lemmes hd ++ a ++ rev a ++ tl
+           et trouver un équivalent pour hd ++ a ++ map negb (rev a) ++ tl *)
 
 (*
   TODO: les palindromes de longueur 16 sont centrés autour