Update

thue-morse.v

@@ -874,11 +874,108 @@ Proof.
 Qed.
 
 
+Lemma count_occ_bool_list : forall (a: list bool),
+  length a = (count_occ bool_dec a true) + (count_occ bool_dec a false).
+Proof.
+  intro a.
+  induction a.
+  - reflexivity.
+  - destruct a.
+    + rewrite count_occ_cons_eq. rewrite count_occ_cons_neq.
+      simpl. rewrite IHa. reflexivity. easy. reflexivity.
+    + rewrite count_occ_cons_neq. rewrite count_occ_cons_eq.
+      simpl. rewrite Nat.add_succ_r. rewrite IHa. reflexivity. reflexivity. easy.
+Qed.
+
+
+Lemma count_occ_bool_list2 : forall (a: list bool),
+  count_occ bool_dec a false = count_occ bool_dec a true -> even (length a) = true.
+Proof.
+  intro a. intro H.
+  rewrite count_occ_bool_list. rewrite H.
+  replace (count_occ bool_dec a true) with (1 * (count_occ bool_dec a true)).
+  rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
+  replace (2 * count_occ bool_dec a true) with (0 + 2 * count_occ bool_dec a true).
+  apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l.
+Qed.
+
+
 Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
   tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
 Proof.
+  intros n a hd tl. intro H.
+  assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd.
+  assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd.
 
+  destruct H1.
+  - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
+  - destruct H0.
+    assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
+    assert (Nat.even (length hd) = true).
+    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
+    generalize H2. generalize H. apply tm_step_count_occ.
 
+    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I.
+    assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false).
+    assert (even (length (hd++a++a)) = true).
+    rewrite app_length. rewrite Nat.even_add_even.
+    apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption.
+
+    rewrite app_length. replace (length a) with (1*(length a)).
+    rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
+    rewrite <- Nat.add_0_l. apply Nat.EvenT_Even.
+    apply Nat.even_EvenT.
+    rewrite Nat.even_add_mul_2. reflexivity.
+    apply Nat.mul_1_l.
+    generalize H3. generalize I. apply tm_step_count_occ.
+
+    rewrite count_occ_app in H3. symmetry in H3.
+    rewrite count_occ_app in H3. rewrite H2 in H3.
+    rewrite Nat.add_cancel_l in H3.
+
+    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
+    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
+    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
+    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
+    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
+    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
+    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
+    rewrite app_assoc_reverse. reflexivity.
+
+    assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
+    assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
+    assert (even (length (hd++a)) = true).
+    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
+    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
+    generalize H2. generalize I. apply tm_step_count_occ.
+
+    assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J.
+    assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false).
+    assert (even (length (hd++a++a++a)) = true).
+    rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT.
+    rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length.
+    apply Nat.Even_Even_add.
+    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
+    rewrite app_length. apply Nat.Odd_Odd_add; assumption.
+    generalize H3. generalize J. apply tm_step_count_occ.
+
+    replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3.
+    rewrite count_occ_app in H3. symmetry in H3.
+    rewrite count_occ_app in H3. rewrite H2 in H3.
+    rewrite Nat.add_cancel_l in H3.
+
+    rewrite count_occ_app in H3. rewrite count_occ_app in H3.
+    replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3.
+    replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3.
+    rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
+    rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
+    assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
+    rewrite app_assoc_reverse. reflexivity.
+    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
+    rewrite app_assoc_reverse. rewrite app_inv_head_iff.
+    rewrite app_assoc_reverse. reflexivity.
+    rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity.
+Qed.
 
 
 Prouver l'énoncé du concours général