Update

2022-12-06 19:22:05 +01:00 · 2022-12-06 19:22:05 +01:00 · 1d362f5a4d
commit 1d362f5a4d
parent 4a753aa0d3
1 changed files with 391 additions and 2 deletions
--- a/thue-morse.v
+++ b/thue-morse.v
@ -1078,11 +1078,240 @@ Proof.
 Qed.


+(*
+
+Lemma tm_step_enlarge_window : forall (n m k i j k': nat),
+  k * 2^m < 2^n ->
+  k' * 2^m < 2^(S n) -> (
+  j < m -> i < 2^j ->
+  nth_error (tm_step n) (k*2^m + i) = nth_error (tm_step n) (k*2^m + i + 2^j)
+  <->
+  nth_error (tm_step (S n)) (k'*2^m + i) = nth_error (tm_step (S n)) (k'*2^m + i + 2^j)).
+Proof.
+  intros n m k i j k'. intros I J K L.
+  split.
+  - intros M. rewrite tm_build.
+    assert (S: k' * 2^m < 2^n \/ 2^n <= k' * 2^m). apply Nat.lt_ge_cases.
+    rewrite nth_error_app1. rewrite nth_error_app1. apply M.
+    
+
+
+    distinguer selon k4*2^m < 2^n ou non
+
+
+ *)
+
+
+
+Lemma lt_even_even : forall (a b : nat),
+  even a = true -> even b = true -> a < b -> S a < b.
+Proof.
+  intros a b. intros H I J.
+  assert (even (S a) = false). rewrite Nat.even_succ.
+  rewrite <- Nat.negb_odd in H. rewrite Bool.negb_true_iff in H. apply H.
+  assert (S a <> b).
+
+
+  assert (S (S a) <= b).
+
+
+
+
+Lemma tm_step_add_small_power :
+  forall (n m k j : nat),
+  k * 2^m < 2^n -> j < m
+  -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
+Proof.
+  intros n m k j. intros H I.
+
+  induction n.
+  - simpl. destruct k.
+    + (* hypothèse vraie : k = 0 *)
+      simpl. assert (0 < 2^j).
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+      assert (nth_error [false] (2^j) = None).
+      apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
+      rewrite H1. easy.
+    + (* hypothèse fausse : contradiction en H *)
+      assert ((S k) * (2^m) <> 0).
+      rewrite <- Nat.neq_mul_0.
+      split. easy. apply Nat.pow_nonzero. easy.
+      rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
+      rewrite H in H0. contradiction H0. reflexivity.
+  - rewrite tm_build.
+    assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
+    destruct S.
+    + rewrite nth_error_app1. rewrite nth_error_app1.
+      apply IHn. apply H0. rewrite tm_size_power2.
+
+      replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
+      apply Nat.mul_lt_mono_pos_r.
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+
+
+
+Nat.shiftl_mul_pow2: forall a n : nat, Nat.shiftl a n = a * 2 ^ n
+
+
+
+
+
+
+
+
+
+
+
+
+
+Lemma tm_step_add_small_power :
+  forall (n m k j : nat),
+  k * 2^m < 2^n -> j < m
+  -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
+Proof.
+  intros n m k j. intros H I.
+
+  (*
+  assert(J: nth_error (tm_step (S j)) 0 <> nth_error (tm_step (S j)) (2 ^ j)).
+  rewrite tm_build. rewrite nth_error_app1. rewrite nth_error_app2.
+  rewrite tm_size_power2. rewrite Nat.sub_diag.
+  rewrite tm_step_head_1. simpl. easy.
+  rewrite tm_size_power2. easy.
+  rewrite tm_size_power2.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  replace (nth_error (tm_step (S j)) 0) with (nth_error (tm_step m) 0) in J.
+  replace (nth_error (tm_step (S j)) (2^j)) with (nth_error (tm_step m) (2^j)) in J.
+   *)
+
+
+  (* à raccourcir avec tm_step build ! *)
+  assert (J: nth_error (tm_step j) 0 <> nth_error (tm_step (S j)) (2^j)).
+  replace (2^j) with (0 + 2^j).
+  apply tm_step_next_range2 with (k := 0).
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. reflexivity.
+  assert (K: nth_error (tm_step j) 0 = nth_error (tm_step m) 0).
+  apply tm_step_stable.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  assert (L: nth_error (tm_step (S j)) (2^j) = nth_error (tm_step m) (2^j)).
+  apply tm_step_stable. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  apply Nat.lt_succ_diag_r.
+  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply I.
+  rewrite K in J. rewrite L in J. clear K. clear L.
+  (* fin du à raccourcir *)
+
+  induction n.
+  - simpl. destruct k.
+    + (* hypothèse vraie : k = 0 *)
+      simpl. assert (0 < 2^j).
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+      assert (nth_error [false] (2^j) = None).
+      apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
+      rewrite H1. easy.
+    + (* hypothèse fausse : contradiction en H *)
+      assert ((S k) * (2^m) <> 0).
+      rewrite <- Nat.neq_mul_0.
+      split. easy. apply Nat.pow_nonzero. easy.
+      rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
+      rewrite H in H0. contradiction H0. reflexivity.
+  -
+    rewrite tm_build.
+    assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
+    destruct S.
+    rewrite nth_error_app1. rewrite nth_error_app1.
+    apply IHn. apply H0. rewrite tm_size_power2.
+
+
+
+    rewrite <- tm_size_power2 in H0.
+    rewrite <- nth_error_None in H0.
+
+
+
+
+
+
+
+
+
+
+
+  (*
+  induction k. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
+
+  assert(K: nth_error (tm_step n) 0 = nth_error (tm_step m) 0).
+  replace (nth_error (tm_step n) 0) with (Some false).
+  rewrite tm_step_head_1. simpl. reflexivity.
+  rewrite tm_step_head_1. simpl. reflexivity.
+  assert(L: nth_error (tm_step n) (2^j) = nth_error (tm_step m) (2^j)).
+  apply tm_step_stable.
+ *)
+
+
+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).
+
+Theorem tm_step_stable : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
+
+
+
+
+
+
+
+
+
+
+Lemma greedy_power2 : forall (n m : nat),
+  0 < n -> n = 2^(Nat.log2 n) + m -> m < 2^(Nat.log2 n).
+Proof.
+  intros n m. intros H I.
+  rewrite Nat.add_lt_mono_l with (p := 2^(Nat.log2 n)).
+  rewrite <- I.
+  replace (2^(Nat.log2 n) + 2^(Nat.log2 n)) with (2* (2^(Nat.log2 n))).
+  rewrite <- Nat.pow_succ_r.
+  apply Nat.log2_spec. apply H. apply Nat.log2_nonneg.
+  simpl. rewrite Nat.add_0_r. reflexivity.
+Qed.
+
+
+
+
+
+
+
 Require Import BinNat.
 Require Import BinPosDef.
 Require Import BinPos.


+
+(*
+PeanoNat.Nat.log2_spec_alt:
+  forall a : nat,
+  0 < a ->
+  exists r : nat,
+    a = 2 ^ PeanoNat.Nat.log2 a + r /\ 0 <= r < 2 ^ PeanoNat.Nat.log2 a
+N.log2_spec_alt:
+  forall a : N,
+  (0 < a)%N ->
+  exists r : N, a = (2 ^ N.log2 a + r)%N /\ (0 <= r < 2 ^ N.log2 a)%N
+
+
+PeanoNat.Nat.log2_shiftl:
+  forall a n : nat,
+  a <> 0 ->
+  PeanoNat.Nat.log2 (PeanoNat.Nat.shiftl a n) = PeanoNat.Nat.log2 a + n
+
+
+
+ *)
+
+
+
+
 (* Hamming weight of a positive; argument can not be 0! *)
 Fixpoint hamming_weight_positive (x: positive) :=
  match x with
@ -1091,12 +1320,26 @@ Fixpoint hamming_weight_positive (x: positive) :=
  | xI p => 1 + hamming_weight_positive p
  end.

-Fixpoint hamming_weight_n (x: N) :=
+Definition hamming_weight_n (x: N) :=
  match x with
  | N0 => 0
  | Npos x => hamming_weight_positive x
  end.

+Lemma hamming_weight_remove_high : forall (x : N),
+  (0 < x)%N -> hamming_weight_n x = S (hamming_weight_n (x - 2^(N.log2 x))).
+Proof.
+  intros x.
+
+
+
+
+
+
+N.shiftl_spec_alt:
+  forall a n m : N, N.testbit (N.shiftl a n) (m + n) = N.testbit a m
+
+

 Lemma hamming_weight_positive_nonzero : forall (x: positive),
  hamming_weight_positive x > 0.
@ -1109,6 +1352,7 @@ Proof.
 Qed.


+
 Lemma size_double_bin : forall (x: positive),
  Pos.size_nat (Pos.succ (Pos.pred_double x)) = S (Pos.size_nat x).
 Proof.
@ -1156,6 +1400,144 @@ Proof.
  intros x. reflexivity.
 Qed.

+
+Fixpoint bin2power (x : positive) (k : N) :=
+  match x with
+  | xH   => (2^k)%N
+  | xO y => bin2power y (N.succ k)
+  | xI y => (2^k + bin2power y (N.succ k))%N
+  end.
+
+Lemma bin2power_same : forall  (x : positive),
+  Npos x = bin2power x 0.
+Proof.
+  intros x. 
+  induction x.
+  - simpl.
+
+
+
+(*
+Fixpoint bin2power (x : positive) (k : nat) :=
+  match x with
+  | xH   => 2^k
+  | xO y => bin2power y (S k)
+  | xI y => 2^k + bin2power y (S k)
+  end.
+ *)
+
+Lemma bin2power_double : forall (x : positive) (k : N),
+  bin2power x~0 k = bin2power x (N.succ k).
+Proof.
+  intros x. simpl. reflexivity.
+Qed.
+
+Lemma bin2power_double2 : forall (x : positive),
+  bin2power x~0 0%N = (2 * bin2power x 0)%N.
+Proof.
+  intros x.
+  destruct x.
+  - simpl.
+
+
+N.testbit_even_succ:
+  forall a n : N, (0 <= n)%N -> N.testbit (2 * a) (N.succ n) = N.testbit a n
+
+
+
+
+
+
+
+  simpl. reflexivity.
+Qed.
+
+Lemma bin2power_succ : forall (x : positive) (k : N),
+  bin2power (x~1) k = ((2^k)%N + (bin2power (x~0) k))%N.
+Proof.
+  intros x k.
+  reflexivity.
+Qed.
+
+Lemma bin2power_double2 : forall (x : positive),
+  bin2power x 1%N = (2 * bin2power x 0)%N.
+Proof.
+  intros x.
+  induction x.
+  - rewrite bin2power_succ. rewrite bin2power_succ. rewrite N.pow_0_r.
+    rewrite N.mul_add_distr_l. rewrite N.pow_1_r. rewrite N.mul_1_r.
+    rewrite N.add_cancel_l.
+    replace (bin2power x~0 0) with (bin2power x 1%N).
+
+
+
+
+
+    assert ((2 * bin2power (Pos.succ x~0) 0)%N = (2 + 2*binpower (x~0) 0)%N).
+
+    replace (x~0) with ((N.pos (N.shiftl (x) 1) 1)%N).
+  
+
+
+
+  induction x.
+  - simpl. rewrite Nat.add_0_r. apply eq_S. rewrite <- plus_n_Sm.
+    apply eq_S.
+    destruct x.
+    + simpl.
+
+
+
+
+    rewrite Pos.xI_succ_xO.
+    rewrite <- bin2power_double.
+
+
+  rewrite bin2power_double.
+
+
+
+  - rewrite bin2power_double.
+    assert ( I: bin2power x~1 0 = S (bin2power x~0 0) ).
+    { simpl. reflexivity. } rewrite I.
+    assert ( J: bin2power x~1 1 = S (S (S (bin2power x~0 1) ))).
+    { rewrite <- I.
+
+
+
+
+
+
+  simpl. rewrite Nat.add_0_r.
+
+
+
+
+
+
+Qed.
+
+Lemma bin2power_same : forall (x: positive),
+  bin2power x 0 = Pos.to_nat x.
+Proof.
+  intros x.
+  induction x.
+  - simpl. rewrite <- Pos.pred_double_succ.
+    rewrite succ_succ_pred_double_succ. rewrite Pos.succ_pred_double.
+
+    rewrite <- Pos.xI_succ_xO.
+    rewrite <- bin2power_double.
+
+    assert (I: bin2power x 1 = 2 * (bin2power x 0)).
+    { induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
+      simpl in IHx.
+
+
+    assert (I: bin2power x 1 = 2 * (bin2power x 0)).
+    { induction x. simpl. rewrite Nat.add_0_r. rewrite <- plus_n_Sm.
+      simpl in IHx.
+
+
 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)).
@ -1174,7 +1556,14 @@ Proof.
      rewrite hamming_weight_increase. rewrite Nat.odd_succ.
      rewrite <- Nat.negb_odd.

-      rewrite tm_build. rewrite nth_error_app2. apply map_nth_error.
+      rewrite tm_build. rewrite nth_error_app1.
+
+
+
+
+
+
+      apply map_nth_error.