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

Update

This commit is contained in:
Thomas Baruchel 2023-02-09 21:30:09 +01:00
parent c05caff356
commit 953689efe1
1 changed files with 91 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

91
src/thue_morse4.v
View File

@ -454,9 +454,100 @@ Proof.
generalize H14. generalize H14. generalize H17. generalize H'.
apply tm_step_morphism4.
pose (hd'' := firstn (Nat.div2 (length hd')) (tm_step n)).
pose (a'' := firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length hd')) (tm_step n))).
pose (tl'' := skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n)).
fold hd'' in H18. fold a'' in H18. fold tl'' in H18.
assert (length hd'' = Nat.div2 (length hd')). unfold hd''.
rewrite firstn_length_le. reflexivity.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite <- Nat.pow_succ_r.
rewrite <- tm_size_power2. rewrite <- Nat.Even_double.
rewrite H'. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia.
assert (length hd' = length (tm_morphism hd'')).
rewrite tm_morphism_length. rewrite H19. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
assert (length a'' = Nat.div2 (length a')). unfold a''.
rewrite firstn_length_le. reflexivity. rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H'. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (length a' = length (tm_morphism a'')).
rewrite tm_morphism_length. rewrite H21. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double. reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite H' in H18. rewrite tm_morphism_app in H18.
assert (hd' = tm_morphism hd''). generalize H20. generalize H18.
apply app_eq_length_head. rewrite <- H23 in H18.
apply app_inv_head in H18. rewrite tm_morphism_app in H18.
assert (a' = tm_morphism a''). generalize H22. generalize H18.
apply app_eq_length_head. rewrite <- H24 in H18.
apply app_inv_head in H18. rewrite tm_morphism_app in H18.
assert (length a' = length (tm_morphism (
firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n))))).
rewrite tm_morphism_length. rewrite firstn_length_le.
rewrite <- Nat.double_twice. rewrite <- Nat.Even_double.
reflexivity.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H'. rewrite app_assoc.
rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
rewrite app_length. lia. apply Nat.le_refl.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.
assert (a' = tm_morphism (
firstn (Nat.div2 (length a'))
(skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)))).
generalize H25. generalize H18. apply app_eq_length_head.
rewrite <- H26 in H18. apply app_inv_head in H18.
assert (H'' := H').
rewrite H23 in H''. rewrite H24 in H''. rewrite H18 in H''.
rewrite <- tm_morphism_app in H''.
rewrite <- tm_morphism_app in H''.
rewrite <- tm_morphism_app in H''.
rewrite <- tm_step_lemma in H''. rewrite <- tm_morphism_eq in H''.
assert (0 < length a''). unfold a''. rewrite firstn_length_le.
destruct (length a'). inversion H15. destruct n0. inversion H14.
replace (S (S n0)) with (n0 + 1*2).
rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia.
easy. lia.
rewrite skipn_length.
rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice.
rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l.
rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2.
rewrite <- Nat.Even_double. rewrite <- Nat.double_twice.
rewrite <- Nat.Even_double.
rewrite H'. rewrite app_length. rewrite app_length. lia.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
lia. lia.