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

Update

This commit is contained in:
Thomas Baruchel 2023-01-23 21:01:27 +01:00
parent 1dccd289fc
commit 14e85d0b24
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/thue_morse3.v
View File

@ -1118,6 +1118,24 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
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 *)
(* proof that b12 <> b1 *)
assert ({b12=b1} + {~ b12=b1}). apply bool_dec. destruct H10. rewrite e1 in H.
assert (even (length (hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])) = false).
replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1
:: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b1 :: tl)
with ((hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])
++ [ b0;b1;b1] ++ [b0;b1;b1] ++ tl) in H.
assert (odd (length [b0;b1;b1]) = true). reflexivity.
generalize H10. generalize H. apply tm_step_odd_prefix_square.
rewrite <- app_assoc. reflexivity. unfold hd'' in H10.
rewrite removelast_firstn_len in H10. rewrite Y'' in H10.
rewrite app_length in H10. rewrite firstn_length_le in H10. simpl in H10.
rewrite Nat.even_add in H10.
simpl in Q. rewrite Q in H10. inversion H10.
rewrite Y''. apply Nat.le_pred_l.
(* now we know that b12 <> b1 *)