From 787dab1159c2b3d74f7e1ce3fe1bd0ded1bd4c3e Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 14 Dec 2022 21:00:46 +0100 Subject: [PATCH] Update --- thue-morse.v | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 473146c..2e6eca0 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1152,9 +1152,9 @@ Proof. 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. split; intro; inversion H2. - destruct b; simpl. split; intro; inversion H2. split; intro; reflexivity. + intros a b. destruct a. destruct b. destruct b0; destruct b; simpl. + split; intro; reflexivity. split; intro; inversion H2. + split; intro; inversion H2. split; intro; reflexivity. split; intro; inversion H2. destruct b. split; intro; inversion H2. split; intro; reflexivity. @@ -1253,11 +1253,9 @@ Proof. 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. + 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. + apply H1 in H2. rewrite <- H2 at 1. easy. easy. easy. assert (Some false = Some false). reflexivity. apply H1 in H2. rewrite H2 at 1. easy. easy. rewrite nth_error_nth' with (d := false). easy.