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:10:34 +01:00
parent 5af7d7df3a
commit ab1bf0886b
2 changed files with 13 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/thue_morse.v
View File

@ -354,6 +354,16 @@ Proof.
rewrite negb_involutive. reflexivity.
Qed.
Lemma tm_step_odd_step : forall (n : nat),
rev (tm_step (S (Nat.double n))) = map negb (tm_step (S (Nat.double n))).
Proof.
intro n. induction n.
- reflexivity.
- rewrite <- tm_step_lemma. rewrite tm_morphism_rev.
rewrite Nat.double_S. rewrite tm_build. rewrite rev_app_distr.
rewrite tm_build_negb. rewrite IHn. rewrite <- IHn at 1.
rewrite rev_involutive. reflexivity.
Qed.
Theorem tm_step_double_index : forall (n k : nat),
nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).

11
src/thue_morse3.v
View File

@ -260,18 +260,13 @@ Proof.
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))).
Proof.
intro n. induction n.
- reflexivity.
- rewrite Nat.double_S. rewrite tm_build. rewrite app_inv_head_iff.
rewrite <- tm_step_lemma. rewrite IHn.
rewrite tm_morphism_rev. rewrite tm_morphism_app. rewrite rev_app_distr.
rewrite map_app. rewrite map_app. rewrite tm_morphism_app.
rewrite rev_involutive. rewrite tm_build_negb. rewrite tm_build_negb.
reflexivity.
intro n. rewrite tm_step_odd_step. rewrite <- tm_build.
rewrite Nat.double_S. reflexivity.
Qed.