From dcfa1b363cec23d9a7738e4d2769f07bf4a26029 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 4 Jan 2023 15:26:06 +0100 Subject: [PATCH] Update --- thue-morse.v | 113 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 111 insertions(+), 2 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 1741d1c..59cec86 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -753,6 +753,116 @@ Proof. Qed. +Lemma tm_step_pred : forall (n k m : nat), + S (2*k) * 2^m < 2^n -> + nth_error (tm_step n) (S (2*k) * 2^m) + = nth_error (tm_step n) (pred (S (2*k) * 2^m)) + <-> odd m = true. +Proof. + intros n k m. + + generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r. + destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r. + intro H. apply Nat.neq_succ_0 in H. contradiction H. + rewrite Nat.odd_0. rewrite Nat.pred_succ. + rewrite <- tm_step_double_index. intro H. split; intro I. + symmetry in I. apply tm_step_succ_double_index in I. contradiction I. + apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H. + rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2. + inversion I. + + intro n0. intro I. + destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I. + rewrite Nat.mul_eq_0 in I. destruct I. + apply Nat.neq_succ_0 in H. contradiction H. + apply Nat.pow_nonzero in H. contradiction H. easy. + rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc. + replace (S (2*k) * 2) with (2* (S (2*k))). + rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index. + + rewrite Nat.pow_succ_r' in I. + rewrite Nat.pow_succ_r' in I. + rewrite Nat.mul_assoc in I. + replace (S (2*k) * 2) with (2* (S (2*k))) in I. + rewrite <- Nat.mul_assoc in I. + rewrite <- Nat.mul_lt_mono_pos_l in I. + assert (J := I). apply IHm in J. + + assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + + assert (L: pred( S (2 * k) * 2 ^ m) < S (2 * k) * 2 ^ m). + apply Nat.lt_pred_l. apply Nat.neq_mul_0. + split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0. assumption. + + assert (N: pred (2 * (S (2 * k) * 2 ^ m)) < length (tm_step (S n0))). + rewrite tm_size_power2. + rewrite <- Nat.le_succ_l. rewrite Nat.succ_pred_pos. rewrite Nat.pow_succ_r. + apply Nat.mul_le_mono_l. generalize I. apply Nat.lt_le_incl. + apply Nat.le_0_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2. + apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption. + + assert(T: pred (S (2 * k) * 2 ^ m) < 2 ^ n0). + generalize I. generalize L. apply Nat.lt_trans. + + assert (nth_error (tm_step n0) (pred (S (2 * k) * 2 ^ m)) + <> nth_error (tm_step (S n0)) (S (2 * (pred(S (2 * k) * 2 ^ m))))). + apply tm_step_succ_double_index. assumption. + + replace (S (2 * (pred(S (2 * k) * 2 ^ m)))) with (pred(2 * (S (2*k) * 2^m))) in H. + rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m). + + split. intro K. rewrite <- K in H. + destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); + destruct (nth_error (tm_step n0) (pred(S (2 * k) * 2 ^ m))). + destruct J. replace (Some b) with (Some b0) in H. contradiction H. + reflexivity. symmetry. apply H1. reflexivity. + destruct J. replace (Some b) with (None : option bool) in H. + contradiction H. reflexivity. symmetry. apply H1. reflexivity. + destruct J. replace (None : option bool) with (Some b) in H. + contradiction H. reflexivity. symmetry. apply H1. reflexivity. + contradiction H. reflexivity. + + destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); + destruct (nth_error (tm_step n0) (pred(S (2 * k) * 2 ^ m))); + intro K; simpl in K; inversion K. + + rewrite nth_error_nth' with (d := false) in J. + rewrite nth_error_nth' with (d := false) in J. + rewrite nth_error_nth' with (d := false) in H. + rewrite nth_error_nth' with (d := false) in H. + rewrite nth_error_nth' with (d := false). + rewrite nth_error_nth' with (d := false). + destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false); + destruct (nth (pred (S (2 * k) * 2 ^ m)) (tm_step n0) false); + destruct (nth (pred (2 * (S (2 * k) * 2 ^ m))) (tm_step (S n0)) false). + simpl; split; reflexivity. + destruct J. rewrite H0 in H. contradiction H. reflexivity. + reflexivity. + simpl; split; reflexivity. contradiction H. reflexivity. + contradiction H. reflexivity. + simpl; split; reflexivity. + destruct J. rewrite H0 in H. contradiction H. reflexivity. + reflexivity. + simpl; split; reflexivity. + + assumption. rewrite tm_size_power2. assumption. assumption. + rewrite tm_size_power2. assumption. + rewrite tm_size_power2. assumption. + rewrite tm_size_power2. assumption. + + rewrite <- Nat.add_1_r at 4. + rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l. + rewrite <- Nat.add_1_r at 1. + rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l. + rewrite <- Nat.add_succ_l. rewrite Nat.succ_pred_pos. rewrite <- Nat.add_pred_r. + reflexivity. apply Nat.neq_mul_0. split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0. + assumption. apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption. + apply Nat.lt_0_2. + + apply Nat.mul_comm. apply Nat.mul_comm. +Qed. + +(* TODO: remove Lemma tm_step_pred : forall (n k m : nat), S (2*k) * 2^m < 2^n -> nth_error (tm_step n) (S (2*k) * 2^m) @@ -865,7 +975,7 @@ Proof. apply Nat.mul_comm. apply Nat.mul_comm. Qed. - + *) (* From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022 @@ -1340,4 +1450,3 @@ Qed. -