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 19:35:41 +01:00
parent 52b462d85c
commit b5369923d6
1 changed files with 14 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/thue_morse3.v
View File

@ -868,10 +868,21 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H.
(* premier sous-cas : b8 = b9, contradiction lié à repeating_patterns *)
assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H7. rewrite e1 in H.
(* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
(* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
(* lemme initial *)
assert (forall n : nat, n mod 4 = 2 -> n mod 8 = 2 \/ n mod 8 = 6).
intro m. intro A.
assert (m mod (4*2) = m mod 4 + 4 * ((m / 4) mod 2)).
apply Nat.mod_mul_r; easy. rewrite A in H7.
rewrite <- Nat.bit0_mod in H7. replace (4*2) with 8 in H7.
rewrite H7.
destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity.
reflexivity.
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 *)
False, True, True, False, True, False, False, True, True, False, False