From 14e85d0b24ef21b89e55812168e4022310c7ef05 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 23 Jan 2023 21:01:27 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index c8ec5b2..d23cb05 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -1118,6 +1118,24 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption. apply Nat.lt_1_2. reflexivity. (* now we have added b12 in front of tl *) + (* proof that b12 <> b1 *) + assert ({b12=b1} + {~ b12=b1}). apply bool_dec. destruct H10. rewrite e1 in H. + assert (even (length (hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])) = false). + replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1 + :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b1 :: tl) + with ((hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1]) + ++ [ b0;b1;b1] ++ [b0;b1;b1] ++ tl) in H. + assert (odd (length [b0;b1;b1]) = true). reflexivity. + generalize H10. generalize H. apply tm_step_odd_prefix_square. + rewrite <- app_assoc. reflexivity. unfold hd'' in H10. + rewrite removelast_firstn_len in H10. rewrite Y'' in H10. + rewrite app_length in H10. rewrite firstn_length_le in H10. simpl in H10. + rewrite Nat.even_add in H10. + simpl in Q. rewrite Q in H10. inversion H10. + rewrite Y''. apply Nat.le_pred_l. + (* now we know that b12 <> b1 *) + +