From 8fd8fbf561ba2188ac03daae7c86f0a83b1b58a9 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 21:46:41 +0100 Subject: [PATCH] Update --- thue-morse.v | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index df678ad..e642972 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -993,8 +993,7 @@ Proof. assert (n < S n + S m). rewrite Nat.add_succ_comm. apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1. - apply Nat.pow_lt_mono_r. generalize H0. generalize H. - apply Nat.lt_trans. + apply Nat.pow_lt_mono_r. generalize H0. generalize H. apply Nat.lt_trans. + rewrite <- I. rewrite <- IHm. assert (U: S k < 2^(S n+m)). @@ -1012,26 +1011,17 @@ Proof. generalize J. rewrite <- tm_size_power2. apply nth_error_nth'. assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)). generalize K. rewrite <- tm_size_power2. apply nth_error_nth'. - - (* assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false). *) assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k). generalize K. generalize J. apply tm_step_stable. - - rewrite <- H2 in H1. rewrite H0 in H1. inversion H1. - rewrite H4. + rewrite <- H2 in H1. rewrite H0 in H1. inversion H1. rewrite H4. assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)). generalize H. rewrite <- tm_size_power2. apply nth_error_nth'. assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)). - generalize U. rewrite <- tm_size_power2. apply nth_error_nth'. - assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)). - generalize U. generalize H. apply tm_step_stable. - rewrite H3 in H6. rewrite H5 in H6. - inversion H6. rewrite H8. - reflexivity. + rewrite H3 in H6. rewrite H5 in H6. inversion H6. rewrite H8. reflexivity. Qed.