Update

thue-morse.v

@@ -963,7 +963,7 @@ Proof.
   assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
   generalize I. apply Nat.add_lt_mono_r.
 
-  (* Part 2 *)
+  (* Part 2: main proof *)
   assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
   generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
   assert (nth_error (tm_step n) m = Some (nth m (tm_step n) false)).
@@ -978,7 +978,7 @@ Proof.
   apply nth_error_nth'.
   rewrite H2. rewrite H3. rewrite H4. rewrite H5.
 
-  (* Part 3 *)
+  (* Part 3: handling 16 different cases *)
   destruct (nth k (tm_step n) false).
   destruct (nth m (tm_step n) false).
   destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
@@ -1078,6 +1078,194 @@ Proof.
 Qed.
 
 
+Require Import BinNat.
+Require Import BinPosDef.
+Require Import BinPos.
+
+
+(* Hamming weight of a positive; argument can not be 0! *)
+Fixpoint hamming_weight_positive (x: positive) :=
+  match x with
+  | xH   => 1
+  | xO p => hamming_weight_positive p
+  | xI p => 1 + hamming_weight_positive p
+  end.
+
+Fixpoint hamming_weight_n (x: N) :=
+  match x with
+  | N0 => 0
+  | Npos x => hamming_weight_positive x
+  end.
+
+
+Lemma hamming_weight_positive_nonzero : forall (x: positive),
+  hamming_weight_positive x > 0.
+Proof.
+  intros x.
+  induction x.
+  - simpl. apply Arith_prebase.gt_Sn_O_stt.
+  - simpl. apply IHx.
+  - simpl. apply Arith_prebase.gt_Sn_O_stt.
+Qed.
+
+
+Lemma size_double_bin : forall (x: positive),
+  Pos.size_nat (Pos.succ (Pos.pred_double x)) = S (Pos.size_nat x).
+Proof.
+  intros x.
+  rewrite Pos.succ_pred_double.
+  reflexivity.
+Qed.
+
+Lemma succ_succ_pred_double_succ : forall (x: positive),
+  Pos.pred_double (Pos.succ x) = Pos.succ (Pos.succ (Pos.pred_double x)).
+Proof.
+  intros x.
+  rewrite <- Pos.add_1_l.
+  rewrite Pos.add_xO_pred_double.
+  rewrite <- Pos.add_1_l.
+  rewrite <- Pos.add_1_l.
+  rewrite Pos.add_assoc.
+  reflexivity.
+Qed.                                                                                  
+Lemma size_double_bin2 : forall (x: positive),
+  Pos.size_nat (Pos.pred_double (Pos.succ x)) = S (Pos.size_nat x).
+Proof.
+  intros x.
+  rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
+  reflexivity.
+Qed.
+
+Lemma size_succ_double_bin : forall (x: positive),
+  Pos.size_nat (Pos.succ (Pos.succ (Pos.pred_double x))) = S (Pos.size_nat x).
+Proof.
+  intros x.
+  rewrite <- succ_succ_pred_double_succ. rewrite size_double_bin2.
+  reflexivity.
+Qed.
+
+Lemma nat_size_pos_size : forall (x: positive),
+  N.size_nat (N.pos x) = Pos.size_nat x.
+Proof.
+  intros x. reflexivity.
+Qed.
+
+Lemma hamming_weight_increase : forall (x: positive),
+  hamming_weight_positive x~1 = S (hamming_weight_positive x).
+Proof.
+  intros x. reflexivity.
+Qed.
+
+Lemma tm_step_hamming : forall (x: N),
+  nth_error (tm_step (N.size_nat x)) (N.to_nat x)
+  = Some (odd (hamming_weight_n x)).
+Proof.
+  intros x.
+  destruct x.
+  - reflexivity.
+  - induction p.
+    + rewrite <- Pos.pred_double_succ.
+
+      rewrite nat_size_pos_size.
+      rewrite succ_succ_pred_double_succ at 1.
+      rewrite size_succ_double_bin.
+
+      unfold hamming_weight_n. rewrite Pos.pred_double_succ.
+      rewrite hamming_weight_increase. rewrite Nat.odd_succ.
+      rewrite <- Nat.negb_odd.
+
+      rewrite tm_build. rewrite nth_error_app2. apply map_nth_error.
+
+
+
+
+      rewrite succ_succ_pred_double_succ.
+
+
+
+
+
+
+
+      simpl. rewrite Pos.succ_pred_double.
+      rewrite size_double_bin.
+
+
+      unfold N.to_nat at 2. unfold Pos.to_nat. simpl.
+      
+      rewrite Pos.xI_succ_xO.   transforme p~1 en Pos.succ p~0
+      Lemma pred_double_succ p : pred_double (succ p) = p~1.
+      Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
+      Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
+
+
+
+
+Theorem tm_step_hamming_index : forall (n : N),
+  nth_error (tm_step (N.to_nat n)) (N.to_nat n)
+     = Some (odd (hamming_weight_n n)).
+Proof.
+  intros n.
+  destruct n.
+  - reflexivity.
+  - induction p. simpl.
+
+
+
+
+Theorem tm_step_hamming_index : forall (n m : nat) (k j: N),
+  (N.to_nat k) < 2^n -> (N.to_nat j) < 2^m ->
+    hamming_weight_n k = hamming_weight_n j ->
+    nth_error (tm_step n) (N.to_nat k) = nth_error (tm_step m) (N.to_nat j).
+Proof.
+  intros n m k j. intros H I K.
+  induction k.
+  - simpl in K. assert (j = N0). induction j. reflexivity.
+    rewrite <- N.succ_pos_pred. 
+    unfold hamming_weight_n in K.
+    assert (L: hamming_weight_positive p > 0).
+    apply hamming_weight_positive_nonzero. rewrite <- K in L.
+    apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
+    rewrite H0. rewrite H0 in I.
+    generalize I. generalize H. apply tm_step_stable.
+  - induction j. simpl in K. assert (L: hamming_weight_positive p > 0).
+    apply hamming_weight_positive_nonzero. rewrite K in L.
+    apply Arith_prebase.gt_irrefl_stt in L. contradiction L.
+    (* coeur de l'induction *)
+
+
+    induction p. simpl in K.
+    symmetry in K. apply Nat.neq_succ_0 in K. contradiction K.
+
+
+
+    Theorem N. succ_0_discr n : succ n <> 0.
+  Nat.neq_succ_0: forall n : nat, S n <> 0
+
+
+
+
+
+
+Fixpoint tm_step (n: nat) : list bool :=
+  match n with
+  | 0 => false :: nil
+  | S n' => tm_morphism (tm_step n')
+
+
+
+
+
+
+Lemma tm_step_index_split :
+  forall (a b n m : nat),
+  (* every natural number k can be written according to the following form *)
+  a < 2^n -> (a + 2^n * b) < 2^m
+    -> nth_error (tm_step m) (a + 2^n * b)
+        = nth_error (tm_step (S m)) (a + 2^S n * b).
+Proof.
+  intros a b n m. intros H I.
+
 
 
 
@@ -1086,27 +1274,73 @@ Qed.
 
 Lemma tm_step_cancel_high_bits :
   forall (k b n m : nat),
-  (* every natral number k can be written according to the following form *)
+  (* every natural number k can be written according to the following form *)
   S k < 2^m -> k = 2^n - 1 + 2^S n * b
     -> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
       <-> odd n = true.
 Proof.
   intros k b n m. intros H I.
+
+  assert (L: 2^n - 1 < 2^n). apply Nat.sub_lt. replace (1) with (2^0) at 1.
+  apply Nat.pow_le_mono_r. easy.
+  apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
+
+  assert (M: S(2^n - 1) = 2^n). rewrite Nat.sub_1_r. apply Nat.succ_pred.
+  apply Nat.pow_nonzero. apply Nat.neq_succ_0.
+
+  assert (N: 2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  apply Nat.lt_succ_diag_r.
+
   assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
               <-> odd n = true).
-  assert (2^n - 1 < 2^n).
-  apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
-  easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
   rewrite tm_step_single_bit_index.
   assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
-  apply tm_step_stable. apply H0.
+  apply tm_step_stable. apply L.
   assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
   apply Nat.lt_succ_diag_r.
-  generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
+  generalize H0. generalize L. apply Nat.lt_trans. rewrite <- H0.
   rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
   rewrite <- J. rewrite I.
 
 
+  destruct b.
+
+  (* case b = 0 *)
+  rewrite Nat.mul_0_r. rewrite Nat.add_0_r.
+  rewrite J. rewrite Nat.mul_0_r in I. rewrite Nat.add_0_r in I.
+  rewrite I in H. rewrite M.
+
+  assert (nth_error (tm_step m) (2^n-1) = nth_error (tm_step n) (2^n-1)).
+  generalize L. apply tm_step_stable. apply Nat.lt_succ_l. apply H.
+  rewrite H0. rewrite tm_step_repunit_index.
+
+  assert (nth_error (tm_step m) (2^n) = nth_error (tm_step (S n)) (2 ^ n)).
+  generalize N. rewrite M in H. generalize H. apply tm_step_stable.
+  rewrite H1. rewrite tm_step_single_bit_index.
+
+  split. intros. inversion H2. reflexivity. intros. inversion H2.
+  reflexivity.
+
+  (* case b > 0 *)
+  assert (S b = Pos.to_nat (Pos.of_nat (S b))).
+
+
+
+
+  destruct n.
+  - rewrite Nat.pow_0_r. rewrite Nat.sub_diag. rewrite plus_O_n.
+    rewrite Nat.pow_1_r.
+    rewrite Nat.pow_0_r in I. simpl in I. rewrite Nat.add_0_r in I.
+    induction m.
+    + rewrite Nat.pow_0_r in H.
+      assert (K := H). rewrite Nat.lt_1_r in K.
+      apply Nat.neq_succ_0 in K. contradiction K.
+    +
+
+
+
+
+
   induction k.
   - rewrite <- I.
     assert (b=0).
@@ -1134,7 +1368,8 @@ Proof.
     apply Nat.pred_inj. apply Nat.neq_succ_0. apply Nat.pow_nonzero.
     easy. simpl. rewrite Nat.sub_1_r. reflexivity.
 
-  -
+  - apply IHk. apply Nat.lt_succ_l in H. apply H.
+    rewrite <- I.