From 0a9f4f3bb5cdceb190db3c7b8e8f6c89b9527dd8 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 23 Jan 2023 18:40:17 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 100 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 92 insertions(+), 8 deletions(-) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index 7e9ba36..a38cf3c 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -970,20 +970,104 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite Nat.le_succ_l in T. assumption. easy. easy. (* on change de modulo ; on travaille sur 8k+6 maintenant *) + (* si centre = 8n + 6, alors les cinq derniers sont absurdes *) + assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy. + rewrite H1 in H8. rewrite <- Nat.pred_succ with (n := lh/8) in H8. + rewrite Nat.mul_pred_r in H8. + + assert (lh + 8 = 8 * S (lh / 8) + 6). + rewrite <- Nat.add_cancel_r with (p := 8) in H8. + rewrite <- Nat.add_sub_swap in H8. rewrite Nat.sub_add in H8. assumption. + rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono. + assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. + apply Nat.mul_le_mono_l with (p := 8) in H9. + rewrite Nat.mul_1_r in H9. assumption. apply le_0_n. + assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ. + apply Nat.mul_le_mono_l with (p := 8) in H9. + rewrite Nat.mul_1_r in H9. assumption. + + assert (nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 3) + = nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 4)). + rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub. + rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9. + symmetry in H9. rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9. + apply Nat.succ_inj in H9. apply Nat.succ_inj in H9. + rewrite Nat.mul_comm in H9. rewrite H9. + rewrite Nat.add_succ_r in H9. symmetry in H9. rewrite Nat.add_succ_r in H9. + apply Nat.succ_inj in H9. rewrite <- H9. rewrite H. 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.add_comm. rewrite <- Nat.add_sub_assoc. + rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. symmetry. + rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc. + rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity. + apply Nat.le_refl. rewrite <- Nat.add_0_r at 1. + rewrite <- Nat.add_le_mono_l. apply le_0_n. apply Nat.le_refl. + rewrite <- Nat.add_0_r at 1. + rewrite <- Nat.add_le_mono_l. apply le_0_n. reflexivity. + + rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. + rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. + rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. + rewrite <- Nat.add_le_mono_l. apply le_0_n. + + rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r. + rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r. + rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. + rewrite <- Nat.add_le_mono_l. apply le_0_n. + apply Nat.lt_le_incl. assumption. + + rewrite <- tm_step_repeating_patterns in H10. inversion H10. + simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. + simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ. + + rewrite Nat.mul_lt_mono_pos_l with (p := 8). + rewrite Nat.add_lt_mono_r with (p := 6). rewrite <- H9. + replace (8) with (2^3) at 2. rewrite <- Nat.pow_add_r. + rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. + rewrite Nat.sub_diag. rewrite Nat.add_0_l. + rewrite <- tm_size_power2. rewrite H'. unfold lh. + rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc. + rewrite <- Nat.add_assoc. + + rewrite <- Nat.add_lt_mono_l. simpl. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. + rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r. + rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r. + apply Nat.lt_0_succ. apply Nat.le_refl. + apply Nat.lt_le_incl. assumption. reflexivity. apply Nat.lt_0_succ. + + (* on arrive à la suite du cas b8 = b9 avec cette fois b9 = b1 + et non plus b9 = b0 *) + assert (b9 = b1). destruct b9; destruct b1; destruct b0. + reflexivity. reflexivity. contradiction n6. reflexivity. + contradiction n1. reflexivity. contradiction n1. reflexivity. + contradiction n6. reflexivity. reflexivity. reflexivity. + rewrite H8 in H. + + (* le premier nouveau sous cas est lh mod 4 = 2 en H1 + FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ? + c'est un carré ??? + *) + + + - (* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *) -Lemma tm_step_repeating_patterns : - forall (n m i j : nat), - i < 2^m -> j < 2^m - -> forall k, k < 2^n -> nth_error (tm_step m) i - = nth_error (tm_step m) j - <-> nth_error (tm_step (m+n)) (k * 2^m + i) - = nth_error (tm_step (m+n)) (k * 2^m + j). Proof.