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:44:35 +01:00
parent 6f6aa8b0db
commit 2f6a74098a
1 changed files with 22 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/thue_morse3.v
View File

@ -860,7 +860,12 @@ 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 *) assert (T: 8 <= length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
destruct hd. inversion Q. rewrite app_length. simpl.
rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
apply Nat.le_0_l. apply Nat.le_refl.
(* 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.
@ -880,7 +885,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
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])). pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
fold lh in H1. fold lh in H1. fold lh in T.
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 *)
@ -892,13 +897,26 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
assert (lh - 8 = 8 * Nat.pred (lh / 8) + 2). 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_cancel_r with (p := 8). rewrite <- Nat.add_sub_swap.
rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r. rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r.
assumption. assumption. assumption.
assert (nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 3)
= nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 4)).
rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
rewrite H.
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.
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