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-23 20:35:41 +01:00
parent 603a34db78
commit 1dccd289fc
1 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/thue_morse3.v
View File

@ -1088,11 +1088,44 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
rewrite app_length in Q. rewrite Nat.even_add in Q. rewrite H9 in Q.
inversion Q. reflexivity. rewrite Y''. apply Nat.le_pred_l.
(* proof ath b11 = b0 *)
assert (b11 = b0). destruct b11; destruct b1; destruct b0.
reflexivity. contradiction n7. reflexivity. reflexivity.
contradiction n1. reflexivity. contradiction n1. reflexivity.
reflexivity. contradiction n7. reflexivity. reflexivity.
rewrite H9 in H.
(* on élargit tl (adding b12 in front of tl) *)
destruct tl.
assert (tm_step n = rev (tm_step n)
\/ tm_step n = map negb (rev (tm_step n))).
apply tm_step_rev. destruct H10; rewrite H in H10 at 2;
rewrite rev_app_distr in H10;
assert (odd 1 = true). reflexivity.
rewrite <- tm_step_pred with (n := n) (k := 0) in H11.
rewrite H10 in H11. simpl in H11. inversion H11. rewrite H13 in n1.
contradiction n1. reflexivity. simpl.
replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff.
apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption.
apply Nat.lt_1_2. reflexivity.
reflexivity.
rewrite <- tm_step_pred with (n := n) (k := 0) in H11.
rewrite H10 in H11. simpl in H11. inversion H11.
destruct b0; destruct b1. contradiction n1. reflexivity.
inversion H13. inversion H13. contradiction n1. reflexivity. simpl.
replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff.
apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption.
apply Nat.lt_1_2. reflexivity.
(* now we have added b12 in front of tl *)
False, True, True, False, True, False, False, True, True, False, False, True, False, True, True, False]'
Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl