From a4b2592b016e884ada2e986a8fa2150f4da29c9c Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 10 Dec 2022 18:16:27 +0100 Subject: [PATCH] Update --- thue-morse.v | 29 ++++++----------------------- 1 file changed, 6 insertions(+), 23 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index b0117c9..9392fb2 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1197,22 +1197,6 @@ 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. intro k. - replace (k*2^m) with (k*2^m+0) at 1. - apply tm_step_repeating_patterns. - rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. - apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. - rewrite Nat.add_0_r. reflexivity. -Qed. - Theorem tm_step_flip_low_bit : forall (n m k j : nat), 0 < k -> j < m -> k * 2^m < 2^n @@ -1222,16 +1206,19 @@ Proof. 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 + 0) = nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ). - apply tm_step_add_small_power2. - assumption. + apply tm_step_repeating_patterns. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. 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. + rewrite Nat.add_0_r in H0. replace (nth_error (tm_step (m + n)) (k * 2 ^ m)) with (nth_error (tm_step n) (k * 2 ^ m)) in H0. @@ -1280,10 +1267,6 @@ Qed. - - - - Require Import BinNat. Require Import BinPosDef. Require Import BinPos.