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-27 14:06:30 +01:00
parent 24b8b2434d
commit 819109531c
1 changed files with 18 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/thue_morse3.v
View File

@ -1357,7 +1357,8 @@ Proof.
Qed.
Theorem tm_step_palindromic_length_12_n :
(* TODO: this theorem could be made more powerful with 2 < n *)
Lemma tm_step_palindromic_length_12_n :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
-> length a > 6
@ -1410,7 +1411,22 @@ Proof.
assert (L: length (hd ++ a ++ rev a ++ tl) mod 4 = 0).
rewrite <- H. rewrite tm_size_power2.
Admitted.
assert (V: 1 < n). generalize I. generalize H.
apply tm_step_palindromic_length_12_n.
destruct n. inversion V. destruct n. inversion V. inversion H1.
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
apply Nat.mod_mul. easy. apply le_0_n. apply le_0_n.
rewrite app_length in L.
rewrite <- Nat.add_mod_idemp_l in L. rewrite K in L.
rewrite app_length in L. rewrite Nat.add_0_l in L.
rewrite <- Nat.add_mod_idemp_l in L. rewrite J in L.
rewrite Nat.add_0_l in L. rewrite app_length in L.
rewrite <- Nat.add_mod_idemp_l in L. rewrite rev_length in L.
rewrite J in L. assumption. easy. easy. easy.
Qed.
Lemma tm_step_palindromic_even_morphism1 :
forall (n : nat) (hd a tl : list bool),