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-19 08:48:12 +01:00
parent 90556d8cf7
commit ef33834ed8
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/thue_morse3.v
View File

@ -260,6 +260,16 @@ Proof.
Qed.
Theorem tm_step_palindromic_full : forall (n : nat),
odd n = true -> tm_step (S n) = (tm_step n) ++ rev (tm_step n).
Proof.
intro n. intro H.
apply Nat.odd_OddT in H. apply Nat.OddT_Odd in H.
apply Nat.Odd_double in H. rewrite H. rewrite tm_step_odd_step.
rewrite <- tm_build. reflexivity.
Qed.
(*
Lemma tm_step_palindromic_full : forall (n : nat),
tm_step (Nat.double (S n)) =
(tm_step (S (Nat.double n))) ++ rev (tm_step (S (Nat.double n))).
@ -267,7 +277,7 @@ Proof.
intro n. rewrite tm_step_odd_step. rewrite <- tm_build.
rewrite Nat.double_S. reflexivity.
Qed.
*)
(*
Lemma tm_step_palindromic_even_seed :