From 0d4ca4243925e7e43198b28317f0c9eb74fa3993 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 31 Dec 2022 18:29:09 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 141 ++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 124 insertions(+), 17 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 9c3ac0f..7746978 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -744,33 +744,110 @@ Proof.
 Qed.
 
 
-
-
-
-
-
-
-
-Require Import BinPosDef.
-Require Import BinNatDef.
-
-Lemma tm_step_double_index_pos : forall (p : positive),
-  nth_error (tm_step (Pos.size_nat p)) (Pos.to_nat p) =
-  nth_error (tm_step (S (Pos.size_nat p))) (Pos.to_nat (p~0)).
+Lemma tm_morphism_count_occ : forall (l : list bool),
+  count_occ Bool.bool_dec (tm_morphism l) true
+    = count_occ Bool.bool_dec (tm_morphism l) false.
 Proof.
-  intro p.
-  simpl.
+  intro l. induction l.
+  - reflexivity.
+  - destruct a.
+    + simpl. apply eq_S. assumption.
+    + simpl. apply eq_S. assumption.
+Qed.
+
+Lemma tm_morphism_app : forall (l1 l2 : list bool),
+  tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
+Proof.
+  intros l1 l2.
+  induction l1.
+  - reflexivity.
+  - simpl. rewrite IHl1. reflexivity.
+Qed.
+
+Lemma tm_morphism_eq : forall (l1 l2 : list bool),
+  l1 = l2 <-> tm_morphism l1 = tm_morphism l2.
+Proof.
+  intros l1 l2. split.
+  - intro H. rewrite H. reflexivity.
+  - generalize l2. induction l1.
+    + intro l. intro H. simpl in H.
+      induction l. reflexivity. simpl in H. inversion H.
+    + simpl. intro l0. intro H.
+      induction l0. simpl in H. inversion H.
+      simpl in H. inversion H. apply IHl1 in H3. rewrite H3.
+      reflexivity.
+Qed.
+
+Lemma tm_morphism_app2 : forall (l hd tl : list bool),
+  tm_morphism l = hd ++ tl
+  -> even (length hd) = true
+  -> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
+Proof.
+  intros l hd tl. intros H I.
+  assert (J : l = (firstn (Nat.div2 (length hd)) l) ++ (skipn (Nat.div2 (length hd)) l)).
+  symmetry. apply firstn_skipn.
+  rewrite tm_morphism_eq in J.
+  rewrite tm_morphism_app in J.
 
 
 
 
-Theorem tm_step_double_index : forall (n k : nat),
-  nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
 
 
 
 
 
+Lemma tm_morphism_app2 : forall (l hd tl : list bool),
+  tm_morphism l = hd ++ tl -> even (length hd) = true
+  -> exists l2, hd = tm_morphism l2.
+Proof.
+  intros l hd tl. intros H I.
+  exists (firstn (Nat.div2 (length hd)) l).
+  generalize I. generalize H.
+  induction l.
+
+  - assert (J: hd = nil). destruct hd. reflexivity.
+    simpl in H. inversion H.
+    rewrite J. reflexivity.
+  - 
+
+
+
+
+  induction tl.
+  rewrite <- app_nil_end in H.
+  exists l. symmetry. assumption.
+
+
+
+
+
+
+Lemma tm_step_even_prefix : forall (hd tl : list bool) (k : nat),
+  tm_step k = hd ++ tl -> even (length hd) = true
+  -> exists l, hd = tm_morphism l.
+Proof.
+  intros hd tl k. intros H I.
+  destruct k.
+  - assert (J: hd = nil). destruct hd. reflexivity.
+    simpl in H. inversion H.
+    symmetry in H2. apply app_eq_nil in H2.
+    destruct H2. rewrite H0 in I. simpl in I. inversion I.
+    rewrite J. exists []. reflexivity.
+  - rewrite <- tm_step_lemma in H.
+    exists (firstn (Nat.div2 (length hd)) (tm_step k)).
+    apply app_inv_tail with (l := tl).
+    rewrite <- H.
+
+
+
+
+
+  
+
+
+
+
 
 
 
@@ -790,6 +867,11 @@ Proof.
     destruct H2. rewrite H0 in I. simpl in I. inversion I.
     rewrite J. reflexivity.
   - rewrite <- tm_step_lemma in H.
+
+
+
+
+
     generalize I. generalize H. induction hd.
     reflexivity.
 
@@ -807,6 +889,31 @@ PeanoNat.Nat.neq_succ_0: forall n : nat, S n <> 0
 
 
 
+Prouver l'énoncé du concours général
+(parmi les n premiers termes avec n pairs, il y en a autant de chaque)
+
+Prouver que si un cube existe il est de taille paire
+
+Prouver que si un cube existe de taille k, il existe aussi un cube
+de même taille précédé par un préfixe de taille pair (par décalage éventuel de 1)
+
+Prouver que si un cube existe, de taille paire, précédé par un préfixe pair,
+alors (par référence au morphisme, il existait à la génération précédente
+un cube de taille moitié précédé par un préfixe pair
+
+--> absurdité : on ne peut diviser indéfiniment par 2 et rester sur du pair
+
+
+
+
+
+
+
+
+
+
+
+
 
   (* TODO: supprimer head_2 *)