From a304f0a9a84b0659e501d2ff00d3a000d3e5e70e Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 21:29:01 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index bb99ccb..647eef6 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -908,7 +908,30 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite H9. apply eq_S in H9. rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9. - rewrite H9. unfold lh. + rewrite H9. unfold lh. unfold hd'. + + rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''. + rewrite app_length. + replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). + rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. + rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. + rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. + rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. reflexivity. + apply Nat.le_refl. unfold lh in T. + rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm. + rewrite <- Nat.add_succ_comm. rewrite app_length in T. + assumption. reflexivity. rewrite Y''. +rewrite app_length. + replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))). + rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm. + rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l. + rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. + apply Nat.le_succ_diag_r. rewrite Nat.add_succ_r. + rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. + rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. + rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4). + rewrite <- Nat.add_le_mono_r. + (* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)