baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-22 20:17:38 +01:00
parent b5369923d6
commit 6f6aa8b0db
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/thue_morse3.v
View File

@ -860,6 +860,8 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite e0 in H7. inversion H7. assumption. rewrite e0 in H7. inversion H7. assumption.
easy. easy.
(* TODO : prouver le très important 8 <= lh *)
(* inutile (* inutile
assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity. assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
*) *)
@ -877,12 +879,26 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite H7. rewrite H7.
destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity. destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity.
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. 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 + 2, alors les cinq premiers sont absurdes *)
(* si centre = 8n + 6, alors les cinq derniers sont absurdes *) (* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
apply H7 in H1. destruct H1. apply H7 in H1. destruct H1.
(* on commence par supposer le centre en 8n+2 : hypothèse 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 False, True, True, False, True, False, False, True, True, False, False