From 7ac1cd560836fd9246c5db2871dea03929e5cbc1 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 3 Jan 2023 21:16:18 +0100 Subject: [PATCH] Update --- thue-morse.v | 98 +++++++++++++++++++++++++++++----------------------- 1 file changed, 54 insertions(+), 44 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index eb98929..19bb9d8 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -762,7 +762,7 @@ Proof. 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. - intro I. apply diff_false_true in I. contradiction I. + intro I. inversion I. intro n0. intro I. destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I. @@ -822,11 +822,8 @@ Proof. contradiction H. reflexivity. destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m)); - destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)). - intro K. simpl in K. apply diff_false_true in K. contradiction K. - intro K. simpl in K. apply diff_false_true in K. contradiction K. - intro K. simpl in K. apply diff_false_true in K. contradiction K. - intro K. simpl in K. apply diff_false_true in K. contradiction K. + destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)); + 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. @@ -1204,13 +1201,13 @@ Qed. Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool), tm_step n = hd ++ a ++ a ++ a ++ tl -> 0 < length a - -> exists (hd2 b tl2 : list bool), tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 - /\ 0 < length b. + -> exists (hd2 b tl2 : list bool), + tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b. Proof. intros n a hd tl. intros H I. - assert(J: exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2 - /\ length a = length b - /\ even (length hd2) = true). + assert(J: exists (hd2 b tl2 : list bool), + tm_step n = hd2 ++ b ++ b ++ b ++ tl2 + /\ length a = length b /\ even (length hd2) = true). generalize I. generalize H. apply tm_step_cube5. destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2]. destruct J2 as [J3 J4]. destruct J4 as [J5 J6]. @@ -1222,9 +1219,12 @@ Proof. - rewrite <- tm_step_lemma in J3. assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))). generalize J6. generalize J3. apply tm_morphism_app2. - assert (M: b ++ b ++ b ++ tl2 = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))). + assert (M: b ++ b ++ b ++ tl2 + = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))). generalize J6. generalize J3. apply tm_morphism_app3. - assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))). + assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) + (tm_step n)))). generalize J. symmetry in M. generalize M. apply tm_morphism_app2. assert (even (length (b++b++b)) = true). rewrite app_length. rewrite app_length. @@ -1232,17 +1232,23 @@ Proof. apply Nat.EvenT_Even. apply Nat.even_EvenT. rewrite Nat.even_add_even. assumption. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. - assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) (skipn (Nat.div2 (length hd2)) (tm_step n)))). + assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) + (skipn (Nat.div2 (length hd2)) + (tm_step n)))). generalize H0. symmetry in M. generalize M. replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3. rewrite app_assoc_reverse. apply app_inv_head_iff. rewrite app_assoc_reverse. reflexivity. assert (hd2 ++ b ++ b ++ b ++ tl2 = (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))) - ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))))). + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n)))) + ++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) + (skipn (Nat.div2 (length hd2)) (tm_step n))))). rewrite <- L. rewrite <- N. rewrite <- O. reflexivity. rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1. @@ -1250,15 +1256,19 @@ Proof. rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1. exists (firstn (Nat.div2 (length hd2)) (tm_step n)). - exists (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))). - exists (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))). + exists (firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length hd2)) (tm_step n))). + exists (skipn (Nat.div2 (length (b ++ b ++ b))) + (skipn (Nat.div2 (length hd2)) (tm_step n))). split. assumption. - assert (2 <= length b). - destruct b. simpl in J5. rewrite J5 in I. apply Nat.lt_irrefl in I. contradiction I. - destruct b0. simpl in J. inversion J. - simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l. - assert (length (b++b++b++tl2) = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))). + assert (2 <= length b). destruct b. simpl in J5. rewrite J5 in I. + apply Nat.lt_irrefl in I. contradiction I. + destruct b0. simpl in J. inversion J. simpl. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. apply Nat.le_0_l. + + assert (length (b++b++b++tl2) + = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))). rewrite M. apply tm_morphism_size. assert (2 <= length (b++b++b++tl2)). @@ -1270,7 +1280,8 @@ Proof. rewrite firstn_length. rewrite <- Nat.le_succ_l. assert (1 <= Nat.div2 (length b)). rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r. - replace (2 * Nat.div2 (length b)) with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))). + replace (2 * Nat.div2 (length b)) + with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))). rewrite <- Nat.div2_odd. assumption. rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity. apply Nat.lt_0_2. @@ -1290,9 +1301,11 @@ Proof. - destruct H. destruct H. destruct H. destruct H. exists x. exists x0. exists x1. split; assumption. - destruct H. destruct H. destruct H. destruct H. - assert (J: exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2). - generalize H0. generalize H. apply tm_step_cube6. rewrite Nat.pred_succ in J. - apply IHn. apply J. + assert (J: exists (hd2 b2 tl2 : list bool), + tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 + /\ 0 < length b2). + generalize H0. generalize H. apply tm_step_cube6. + rewrite Nat.pred_succ in J. apply IHn. apply J. Qed. @@ -1302,21 +1315,18 @@ Proof. intros n hd a b tl. intros H I. assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec. - - destruct J. rewrite <- e in H. - - assert (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl - /\ 0 < length a). - exists hd. exists a. exists tl. split; assumption. - - assert (exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 - /\ 0 < length b). - generalize H0. apply tm_step_cube7. - destruct H1. destruct H1. destruct H1. destruct H1. - - assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2. - apply Nat.lt_irrefl in H3. contradiction H3. - assumption. + destruct J. + - rewrite <- e in H. + assert (exists (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a). + exists hd. exists a. exists tl. split; assumption. + assert (exists (hd2 b tl2 : list bool), + tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b). + generalize H0. apply tm_step_cube7. + destruct H1. destruct H1. destruct H1. destruct H1. + assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2. + apply Nat.lt_irrefl in H3. contradiction H3. + - assumption. Qed.