From 12a7ea541c7d28032cf6bb76fc5ce759a8335e49 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 15 Jan 2023 17:40:57 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 115 +++++++++++++++++++++++++++++++--------------- 1 file changed, 79 insertions(+), 36 deletions(-) diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 83b4b25..eee4b1d 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -1069,9 +1069,9 @@ Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool), -> even (length a) = true -> exists (hd' a' tl' : list bool), tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl' + /\ 0 < length a' /\ odd (length hd') = true - /\ even (length a') = true - /\ length a' < length a. + /\ even (length a') = true. Proof. intros n hd a tl. intros H I J K. @@ -1181,6 +1181,32 @@ Proof. split. + rewrite firstn_length_le. + rewrite Nat.mul_lt_mono_pos_l with (p := 2). + rewrite Nat.mul_0_r. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite M3. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. + rewrite skipn_length. + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite M0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + + split. rewrite firstn_length_le. apply eq_S in M2. rewrite Nat.succ_pred_pos in M2. apply eq_S in M2. rewrite <- L2 in M2. rewrite <- M2 in H0. @@ -1194,7 +1220,7 @@ Proof. assumption. - split. rewrite firstn_length_le. + rewrite firstn_length_le. rewrite M3. apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. rewrite skipn_length. rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd'')). @@ -1215,15 +1241,6 @@ Proof. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. assumption. - rewrite firstn_length. - assert (min (Nat.div2 (length a'')) - (length (skipn (Nat.div2 (length hd'')) (tm_step n))) - <= (Nat.div2 (length a''))). - apply Nat.le_min_l. - assert (Nat.div2 (length a'') < length a). rewrite M3. - apply Nat.lt_div2. assumption. - generalize H3. generalize H2. apply Nat.le_lt_trans. - + (* case Nat.div2 (length hd') has an odd length *) exists (firstn (Nat.div2 (length hd')) (tm_step n)). exists (firstn (Nat.div2 (length a')) @@ -1244,11 +1261,38 @@ Proof. split. + rewrite firstn_length_le. + rewrite Nat.mul_lt_mono_pos_l with (p := 2). + rewrite Nat.mul_0_r. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite L3. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. + rewrite skipn_length. + rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')). + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + + rewrite Nat.mul_le_mono_pos_l with (p := 2). + rewrite tm_size_power2. rewrite Nat.mul_add_distr_l. + rewrite <- Nat.double_twice. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. rewrite <- Nat.Even_double. + rewrite <- Nat.pow_succ_r'. rewrite <- tm_size_power2. rewrite L0. + rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono. rewrite app_length. apply Nat.eq_le_incl. + reflexivity. + apply le_0_n. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. + assumption. + + split. + rewrite firstn_length_le. apply Nat.OddT_odd. apply Nat.Odd_OddT. assumption. assumption. - split. rewrite firstn_length_le. + rewrite firstn_length_le. rewrite L3. apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. rewrite skipn_length. rewrite Nat.add_le_mono_l with (p := Nat.div2 (length hd')). @@ -1268,15 +1312,6 @@ Proof. apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. apply Nat.lt_0_2. apply Nat.eq_le_incl. reflexivity. assumption. - - rewrite firstn_length. - assert (min (Nat.div2 (length a')) - (length (skipn (Nat.div2 (length hd')) (tm_step n))) - <= (Nat.div2 (length a'))). - apply Nat.le_min_l. - assert (Nat.div2 (length a') < length a). rewrite L3. - apply Nat.lt_div2. assumption. - generalize H3. generalize H2. apply Nat.le_lt_trans. - (* second case, a'0 is odd and we are looking for an even prefix *) assert (Nat.Even (Nat.div2 (length hd')) \/ Nat.Odd (Nat.div2 (length hd'))). apply Nat.Even_or_Odd. destruct H0. @@ -1372,20 +1407,28 @@ Proof. assumption. Qed. - - -(* -Lemma tm_step_square_pos_even'' : forall (n : nat) (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' a' tl' : list bool), - tm_step (Nat.pred n) = hd' ++ a' ++ a' ++ tl' - /\ odd (length hd') = true - /\ even (length a') = true - /\ length a' < length a. - *) +Lemma tm_step_square_pos_even''' : forall (n : nat), + (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' a' tl' : list bool), + tm_step 0 = hd' ++ a' ++ a' ++ tl' /\ 0 < length a' + /\ odd (length hd') = true /\ even (length a') = true). +Proof. + intro n. intro. + induction n. + - destruct H. destruct H. destruct H. + exists x. exists x0. exists x1. assumption. + - assert (exists hd' a' tl' : list bool, + tm_step (Nat.pred (S n)) = hd' ++ a' ++ a' ++ tl' /\ + 0 < length a' /\ + odd (length hd') = true /\ even (length a') = true). + destruct H. destruct H. destruct H. + destruct H. destruct H0. destruct H1. + generalize H2. generalize H1. generalize H0. generalize H. + apply tm_step_square_pos_even''. rewrite <- pred_Sn in H0. + apply IHn in H0. assumption. +Qed.