From 2099d9f563dbb104aabc0ce63fccb4e48ec62403 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 2 Jan 2023 14:37:17 +0100 Subject: [PATCH] Update --- thue-morse.v | 37 ++++++++++++++++--------------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 09da27c..61bf3ac 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -799,19 +799,20 @@ Proof. rewrite tm_morphism_eq in J. rewrite tm_morphism_app in J. rewrite H in J. apply app_eq_app in J. + + assert (H2: length (tm_morphism l) = length hd + length tl). + rewrite H. apply app_length. + + assert (H3: length hd <= length (tm_morphism l)). + rewrite H2. apply Nat.le_add_r. + rewrite tm_morphism_length in H3. + destruct J. destruct H0; destruct H0. assert (L: length hd = length hd). reflexivity. rewrite H0 in L at 2. rewrite app_length in L. rewrite tm_morphism_length in L. - assert (length (tm_morphism l) = length hd + length tl). - rewrite H. apply app_length. - - assert (length hd <= length (tm_morphism l)). - rewrite H2. apply Nat.le_add_r. - rewrite tm_morphism_length in H3. - assert (Nat.div2 (length hd) <= length l). rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.add_0_r at 1. @@ -835,13 +836,6 @@ Proof. reflexivity. rewrite H0 in L at 2. rewrite app_length in L. rewrite tm_morphism_length in L. - assert (length (tm_morphism l) = length hd + length tl). - rewrite H. apply app_length. - - assert (length hd <= length (tm_morphism l)). - rewrite H2. apply Nat.le_add_r. - rewrite tm_morphism_length in H3. - assert (Nat.div2 (length hd) <= length l). rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.add_0_r at 1. @@ -869,26 +863,27 @@ 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 TODO Search "count_occ" *) -Theorem tm_step_count_occ : forall (hd tl : list bool) (k : nat), - tm_step k = hd ++ tl -> even (length hd) = true +Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat), + tm_step n = hd ++ tl -> even (length hd) = true -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false. Proof. - intros hd tl k. intros H I. - destruct k. + intros hd tl n. intros H I. + destruct n. - assert (J: hd = nil). destruct hd. reflexivity. simpl in H. inversion H. symmetry in H2. apply app_eq_nil in H2. destruct H2. rewrite H0 in I. simpl in I. inversion I. rewrite J. reflexivity. - rewrite <- tm_step_lemma in H. - assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step k))). + assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))). generalize I. generalize H. apply tm_morphism_app2. rewrite J. apply tm_morphism_count_occ. Qed. - - +Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool), + tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true. +Proof.