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-27 17:29:52 +01:00
parent 10abcb7965
commit 4b5ab5a9c6
1 changed files with 23 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/thue_morse3.v
View File

@ -1556,7 +1556,9 @@ Lemma tm_step_palindromic_even_morphism2 :
/\ a = tm_morphism (tm_morphism
(firstn (length a / 4) (skipn (length hd / 4)
(tm_step (pred (pred n))))))
/\ 11 = 42.
/\ tl = tm_morphism (tm_morphism
(skipn (length hd / 4 + Nat.div2 (length a))
(tm_step (pred (pred n))))).
Proof.
intros n hd a tl. intros H W J0.
@ -1809,10 +1811,26 @@ Proof.
apply Nat.le_add_le_sub_l.
rewrite <- H6. rewrite <- H7. assumption.
Nat.div2 (length hd) + Nat.div2 (length a) <= length (tm_step (S n))
rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H3.
rewrite app_length.
rewrite app_length. rewrite rev_length.
replace (length a + length a) with (length a * 2).
rewrite Nat.div2_div. rewrite Nat.div_add.
rewrite <- Nat.div2_div. fold tl'. rewrite H3'.
rewrite app_length.
rewrite app_length. rewrite map_length. rewrite rev_length.
replace (length a' + length a') with (length a' * 2).
rewrite Nat.div2_div. rewrite Nat.div_add.
rewrite H6. rewrite H7.
rewrite Nat.div2_div. rewrite Nat.div_div. reflexivity.
easy. easy. easy.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
easy.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
easy.
rewrite Nat.div2_div. reflexivity.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
apply Nat.le_refl.
Admitted.
@ -1839,7 +1857,6 @@ Admitted.
Lemma tm_step_proper_palindromic_center :