From 6f6aa8b0db42a763e109f5d20ba5aeae233e4994 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sun, 22 Jan 2023 20:17:38 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index b3a8abd..42df08b 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -860,6 +860,8 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite e0 in H7. inversion H7. assumption. easy. +(* TODO : prouver le très important 8 <= lh *) + (* inutile assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity. *) @@ -877,14 +879,28 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM : rewrite H7. destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity. reflexivity. + pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])). + fold lh in H1. assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H8. rewrite e1 in H. (* si centre = 8n + 2, alors les cinq premiers sont absurdes *) (* si centre = 8n + 6, alors les cinq derniers sont absurdes *) apply H7 in H1. destruct H1. (* on commence par supposer le centre en 8n+2 : hypothèse H1 *) + assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy. + rewrite H1 in H8. rewrite <- Nat.succ_pred_pos with (n := lh/8) in H8. + assert (lh - 8 = 8 * Nat.pred (lh / 8) + 2). + rewrite <- Nat.add_cancel_r with (p := 8). rewrite <- Nat.add_sub_swap. + rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r. + assumption. + + + +Nat.div_mod: forall x y : nat, y <> 0 -> x = y * (x / y) + x mod y + + False, True, True, False, True, False, False, True, True, False, False Admitted.