From cacda16dd26e562268c6fe4264edf194267f00db Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Thu, 15 Dec 2022 10:03:42 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 65 ++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 56 insertions(+), 9 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 5ec2df5..0c9fe97 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -934,7 +934,6 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
-Require Import Ltac2.Option.
 Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
   k < 2^n -> m < 2^n ->
     nth_error (tm_step n) k = nth_error (tm_step n) m
@@ -1210,20 +1209,19 @@ Proof.
   assumption.
 
   assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
-
   destruct G as [G1|G2].
 
   (* k = 0 *)
   rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
-  replace (nth_error (tm_step n) 0) with (Some false).
+  rewrite tm_step_head_1 at 1.
   assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
-  destruct S. rewrite Nat.lt_succ_r in H0.
-  apply Nat.pow_le_mono_r with (a := 2) in H0.
-  rewrite <- tm_size_power2 in H0. rewrite <- nth_error_None in H0.
-  rewrite H0. easy. easy.
-  rewrite Nat.le_succ_l in H0. apply Nat.pow_lt_mono_r with (a := 2) in H0.
+  destruct S as [S1|S2]. rewrite Nat.lt_succ_r in S1.
+  apply Nat.pow_le_mono_r with (a := 2) in S1.
+  rewrite <- tm_size_power2 in S1. rewrite <- nth_error_None in S1.
+  rewrite S1. easy. easy.
+  rewrite Nat.le_succ_l in S2. apply Nat.pow_lt_mono_r with (a := 2) in S2.
   rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
-  apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity.
+  apply Nat.lt_1_2.
 
   (* k < 0 *)
   assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
@@ -1269,6 +1267,55 @@ Proof.
 Qed.
 
 
+Lemma tm_step_double_index : forall (n k: nat),
+  2^n <= k -> k < 2^(S n)
+  -> nth_error (tm_step (S n)) k = nth_error (tm_step (S (S n))) (2*k).
+Proof.
+  intros n k. intros H I.
+  destruct n.
+  - simpl in H. simpl in I. rewrite Nat.lt_succ_r in I.
+    assert (J: k = 1). generalize H. generalize I. apply Nat.le_antisymm.
+    rewrite J. reflexivity.
+  - symmetry. rewrite tm_build. rewrite nth_error_app2.
+    rewrite tm_size_power2.
+
+    assert (J: 2 ^ S (S n) <= 2 * k).
+    rewrite Nat.pow_succ_r'. apply Nat.mul_le_mono_l. assumption.
+
+    assert (K: nth_error (tm_step (S (S n))) (2*k - 2^(S (S n)))
+    <> nth_error (tm_step (S (S (S n)))) (2*k - 2^(S (S n)) + 2^(S (S n)))).
+    apply tm_step_next_range2.
+    apply Nat.add_lt_mono_r with (p := 2^(S (S n))). rewrite Nat.sub_add.
+    replace (2*k) with (k+k). apply Nat.add_lt_mono ; assumption.
+    simpl. rewrite Nat.add_0_r. reflexivity. assumption.
+
+    rewrite Nat.sub_add in K.
+    replace (nth_error (tm_step (S (S (S n)))) (2 * k))
+      with (nth_error (tm_step (S (S n))) (2 * k)) in K.
+
+    rewrite nth_error_map.
+
+
+
+
+
+
+
+
+
+
+
+    destruct (nth_error (tm_step (S (S n))) (2 * k - 2 ^ S (S n)));
+    destruct (nth_error (tm_step (S (S n))) k).
+
+
+
+
+Lemma tm_step_next_range2 :
+  forall (n k : nat),
+  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
+
+
 
 (* vérifier si les deux sont nécessaires *)
 Require Import BinPosDef.