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 2022-11-26 06:45:16 +01:00
parent 7c0b8de103
commit b0e15fc10a
1 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
thue-morse.v
View File

@ -830,7 +830,21 @@ Proof.
reflexivity.
Qed.
Lemma tm_step_repunit : forall (n : nat),
Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
intros n.
induction n.
- simpl. reflexivity.
- 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. simpl. reflexivity.
reflexivity. rewrite tm_size_power2. easy.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intros n.