From 64537d4f504a805cd33620cd8a91ef6f816cd012 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 17:41:51 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 60 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 47 insertions(+), 13 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 23a4edd..feb87b3 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -803,11 +803,34 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : assumption. apply Nat.lt_1_2. reflexivity. (* termes à prouver *) - assert (Y: forall (k: bool) (x : list bool), + (* lemmes initiaux *) + assert (Y: forall (k : bool) (x : list bool), length (removelast (k::x)) = length x). - intros k x. rewrite removelast_firstn_len. simpl. - rewrite firstn_length_le. reflexivity. simpl. - apply Nat.le_succ_diag_r. + intros k x. rewrite removelast_firstn_len. + replace (length (k::x)) with (S (length x)). rewrite Nat.pred_succ. + rewrite firstn_length. simpl. apply Nat.min_l. apply Nat.le_succ_diag_r. + reflexivity. + assert (Y': forall (k1 k2 : bool) (x : list bool), + length (removelast (removelast (k1::k2::x))) = length x). + intros k1 k2 x. + rewrite removelast_firstn_len. rewrite Y. + replace (length (k2::x)) with (S (length x)). + rewrite Nat.pred_succ. rewrite firstn_length. rewrite Y. + apply Nat.min_l. apply Nat.le_succ_diag_r. reflexivity. + assert (Y'': forall (k1 k2 k3 : bool) (x : list bool), + length (removelast (removelast (removelast (k1::k2::k3::x)))) = length x). + intros k1 k2 k3 x. + rewrite removelast_firstn_len. rewrite removelast_firstn_len. + rewrite Y. replace (length (k2::k3::x)) with (S (length (k3::x))). + rewrite Nat.pred_succ. rewrite firstn_length. + rewrite firstn_length. rewrite Y. rewrite Nat.min_l. rewrite Nat.min_l. + reflexivity. apply Nat.le_succ_diag_r. rewrite Nat.min_l. + replace (length (k3 :: x)) with (S (length x)). rewrite Nat.pred_succ. + apply Nat.le_succ_diag_r. reflexivity. + replace (length (k2 :: k3::x)) with (S (length (k3::x))). + apply Nat.le_succ_diag_r. reflexivity. reflexivity. + + (* preuves *) assert (U: nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3) = Some b8). unfold b8. @@ -817,16 +840,27 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite app_removelast_last with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1. rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2. - rewrite removelast_firstn_len at 2. rewrite Y. - replace (length (b5::b7::hd)) with (S (S (length hd))). - rewrite <- pred_Sn. rewrite removelast_firstn. rewrite firstn_length_le. - replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). - rewrite <- Nat.sub_add_distr. rewrite Nat.sub_diag. - reflexivity. reflexivity. - rewrite Y. simpl. - - + rewrite Y''. rewrite <- Nat.sub_add_distr. + replace (length (b3::b5::b7::hd)) with (3 + length hd). + rewrite Nat.sub_diag. reflexivity. reflexivity. rewrite Y''. + replace (length (b3::b5::b7::hd)) with (length hd + 3). + rewrite Nat.add_sub. apply Nat.le_refl. rewrite Nat.add_comm. + reflexivity. + assert (0 < length (removelast (removelast (b3 :: b5 :: b7 :: hd)))). + rewrite Y'. simpl. apply Nat.lt_0_succ. + assert ({removelast (removelast (b3 :: b5 :: b7 :: hd))=nil} + + {~ removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}). + apply list_eq_dec. apply bool_dec. destruct H8. + rewrite e0 in H7. inversion H7. assumption. + assert (0 < length (removelast (b3 :: b5 :: b7 :: hd))). + rewrite Y. simpl. apply Nat.lt_0_succ. + assert ({removelast (b3 :: b5 :: b7 :: hd)=nil} + + {~ removelast (b3 :: b5 :: b7 :: hd)=nil}). + apply list_eq_dec. apply bool_dec. destruct H8. + rewrite e0 in H7. inversion H7. assumption. + easy. + False, True, True, False, True, False, False, True, True, False, False