From 688a9b1892df44d858b44f8ea7fa81d3b4a572f6 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 15 Jan 2023 17:54:43 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index eee4b1d..d094e8d 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1430,6 +1430,39 @@ Proof. apply IHn in H0. assumption. Qed. +Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl + -> 0 < length a -> even (length (hd ++ a)) = true. +Proof. + intros n hd a tl. intros H I. + assert (J: Nat.even (length a) || Nat.odd (length a) = true). + apply Nat.orb_even_odd. apply orb_prop in J. + assert (K: Nat.even (length hd) || Nat.odd (length hd) = true). + apply Nat.orb_even_odd. apply orb_prop in K. + destruct J; destruct K. + - rewrite app_length. rewrite Nat.even_add. rewrite H0. rewrite H1. + reflexivity. + - assert (exists (hd' a' tl' : list bool), + tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a' + /\ odd (length hd') = true /\ even (length a') = true). + assert (exists (hd' a' tl' : list bool), + tm_step n = hd' ++ a' ++ a' ++ tl' /\ 0 < length a' + /\ odd (length hd') = true /\ even (length a') = true). + exists hd. exists a. exists tl. split. assumption. + split. assumption. split. assumption. assumption. + generalize H2. apply tm_step_square_pos_even'''. + destruct H2. destruct H2. destruct H2. + destruct H2. destruct H3. destruct H4. + + assert (0 < 0). generalize H5. generalize H3. generalize H2. + apply tm_step_not_nil_factor_even. inversion H6. + - assert (even (length hd) = false). + generalize H0. generalize H. apply tm_step_odd_prefix_square. + rewrite H1 in H2. inversion H2. + - rewrite app_length. rewrite Nat.even_add. + rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd. + rewrite H0. rewrite H1. reflexivity. +Qed. (* TODO: la taille du facteur divise la taille du préfixe ? *)