From 65adb7ec02033d3ddb764eef4d1281b330242fc1 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 14:26:11 +0100 Subject: [PATCH] Update --- thue-morse.v | 147 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 143 insertions(+), 4 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 33951e9..9e2f716 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1256,16 +1256,155 @@ Proof. generalize H2. generalize J. apply Nat.le_trans. Qed. +Lemma tm_step_add_small_power2 : + forall (n m j : nat), + j < m + -> forall k, k < 2^n -> nth_error (tm_step m) 0 + = nth_error (tm_step m) (2^j) + <-> nth_error (tm_step (m+n)) (k * 2^m ) + = nth_error (tm_step (m+n)) (k * 2^m + (2^j)). +Proof. + intros n m j. intros H. + induction n. + - rewrite Nat.add_0_r. intro k. intro. simpl in H0. + assert (k = 0). generalize H0. apply Nat.lt_1_r. + rewrite H1. easy. + - rewrite Nat.add_succ_r. intro k. intro. + rewrite tm_build. + assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases. + destruct S. + + assert (k*2^m < 2^(m+n)). + destruct k. + + simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + + rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1. + rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm. + assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + + rewrite nth_error_app1. rewrite nth_error_app1. + generalize H1. apply IHn. + + rewrite tm_size_power2. + assert (k * 2^m + 2^j < 2^(m+n)). + destruct k. simpl. apply Nat.log2_lt_cancel. + rewrite Nat.log2_pow2. rewrite Nat.log2_pow2. + apply Nat.lt_lt_add_r. assumption. apply Nat.le_0_l. apply Nat.le_0_l. + generalize H2. apply lt_split_bits. + apply Nat.lt_0_succ. assumption. assumption. + + rewrite tm_size_power2. assumption. + + assert (J: 2 ^ (m + n) <= k * 2 ^ m). + rewrite Nat.pow_add_r. rewrite Nat.mul_comm. + apply Nat.mul_le_mono_r. assumption. + + rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2. + + assert (forall a b, option_map negb a = option_map negb b <-> a = b). + intros a b. destruct a. destruct b. destruct b0. destruct b. + simpl. split. intro. reflexivity. intro. reflexivity. + simpl. split. intro. inversion H2. intro. inversion H2. + destruct b. simpl. split. intro. inversion H2. intro. inversion H2. + simpl. split. intro. reflexivity. intro. reflexivity. + split. intro. inversion H2. intro. inversion H2. + destruct b. split. intro. inversion H2. intro. inversion H2. + split. intro. reflexivity. intro. reflexivity. + + replace (k * 2 ^ m - 2^(m + n)) with ((k-2^n)*2^m). + replace (k * 2 ^ m + 2^j - 2^(m + n)) with ((k-2^n)*2^m + 2^j). + rewrite nth_error_map. rewrite nth_error_map. + + rewrite H2. apply IHn. + rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add. + rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0. + rewrite Nat.mul_add_distr_r in H0. simpl in H0. + rewrite Nat.add_0_r in H0. assumption. reflexivity. + apply Nat.le_0_l. assumption. + + rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity. + rewrite Nat.add_comm. reflexivity. assumption. + + rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r. + replace (n+m) with (m+n). reflexivity. + rewrite Nat.add_comm. reflexivity. + + rewrite tm_size_power2. + assert (k*2^m <= k*2^m + 2^j). apply Nat.le_add_r. + generalize H2. generalize J. apply Nat.le_trans. + + rewrite tm_size_power2. assumption. +Qed. + Lemma tm_step_add_small_power : forall (n m k j : nat), - 0 < k -> 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) - -> nth_error (tm_step (S n)) ((S k) * 2^m) <> nth_error (tm_step (S n)) ((S k) * 2^m + 2^j). + 0 < k -> j < m -> k * 2^m < 2^n + -> 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 G H I J. + intros n m k j. intros G H I. + + assert ( nth_error (tm_step m) 0 + = nth_error (tm_step m) (2^j) + <-> nth_error (tm_step (m+n)) (k * 2^m) + = nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ). + apply tm_step_add_small_power2. + assumption. + assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg. + apply Nat.le_0_1. rewrite Nat.le_succ_l. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0. + rewrite Nat.mul_comm in H0. + generalize I. generalize H0. apply Nat.le_lt_trans. + + replace (nth_error (tm_step (m + n)) (k * 2 ^ m)) + with (nth_error (tm_step n) (k * 2 ^ m)) in H0. + replace (nth_error (tm_step (m + n)) (k * 2 ^ m + 2^j)) + with (nth_error (tm_step n) (k * 2 ^ m + 2^j)) in H0. + replace (nth_error (tm_step m) 0) with (Some false) in H0. + replace (nth_error (tm_step m) (2^j)) with (Some true) in H0. + + destruct (nth_error (tm_step n) (k * 2 ^ m)). + destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)). + destruct b. destruct b0. + destruct H0. + assert (Some true = Some true). reflexivity. + apply H1 in H2. rewrite <- H2 at 1. easy. easy. + destruct b0. easy. destruct H0. + assert (Some false = Some false). reflexivity. + apply H1 in H2. rewrite H2 at 1. easy. easy. + rewrite nth_error_nth' with (d := false). easy. + rewrite tm_size_power2. apply lt_split_bits. + assumption. assumption. assumption. + + +Lemma lt_split_bits : forall n m k j, + 0 < k -> j < m -> k * 2^m < 2^n -> k * 2^m +2^j < 2^n. + +nth_error_nth': + forall [A : Type] (l : list A) [n : nat] (d : A), + n < length l -> nth_error l n = Some (nth n l d) + + + +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. + + + + +Nat.mul_le_mono_nonneg: + forall n m p q : nat, + 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q + + +Lemma tm_step_add_small_power2 : + forall (n m j : nat), + j < m + -> forall k, k < 2^n -> nth_error (tm_step m) 0 + = nth_error (tm_step m) (2^j) + <-> nth_error (tm_step (m+n)) (k * 2^m ) + = nth_error (tm_step (m+n)) (k * 2^m + (2^j)). assert (N0: 2^m < 2^n). assert (2^m <= k * 2^m). replace (k * 2^m) with (1*2^m + (k-1)*2^m).