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-04 18:14:10 +01:00
parent c2f9b2a0d5
commit a74abadbc6
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/thue_morse.v
View File

@ -302,9 +302,9 @@ Proof.
intro n.
induction n.
- reflexivity.
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
reflexivity.
- rewrite <- tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
rewrite tm_step_lemma. rewrite IHn. rewrite tm_build_negb.
rewrite <- IHn. rewrite tm_step_lemma. reflexivity.
Qed.
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
@ -355,11 +355,11 @@ Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
intro n.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
rewrite tm_build. rewrite nth_error_app2.
- rewrite tm_size_power2. rewrite Nat.sub_diag.
replace (true) with (negb false). apply map_nth_error.
rewrite tm_step_head_1. reflexivity.
reflexivity. rewrite tm_size_power2. easy.
rewrite tm_step_head_1. reflexivity. reflexivity.
- rewrite tm_size_power2. apply Nat.le_refl.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),