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 10:15:31 +01:00
parent 3beb2eddaa
commit e94afc71e1
1 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/thue_morse3.v
View File

@ -703,8 +703,8 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
destruct tl. destruct tl.
assert (tm_step n = rev (tm_step n) assert (tm_step n = rev (tm_step n)
\/ tm_step n = map negb (rev (tm_step n))). \/ tm_step n = map negb (rev (tm_step n))).
apply tm_step_rev. destruct H5. rewrite H in H5 at 2. apply tm_step_rev. destruct H5; rewrite H in H5 at 2;
rewrite rev_app_distr in H5. simpl in H5. rewrite rev_app_distr in H5; simpl in H5;
assert (odd 0 = true). assert (odd 0 = true).
assert (nth_error (tm_step n) (S (2*0) * 2^0) = assert (nth_error (tm_step n) (S (2*0) * 2^0) =
nth_error (tm_step n) (pred (S (2*0) * 2^0))). nth_error (tm_step n) (pred (S (2*0) * 2^0))).
@ -712,7 +712,12 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1. apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6. apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
assert (nth_error (tm_step n) (S (2*0) * 2^0) =
nth_error (tm_step n) (pred (S (2*0) * 2^0))).
rewrite H5. reflexivity. generalize H6.
apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.