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-23 10:39:39 +01:00
parent 0c970f9666
commit 9f6dc417be
1 changed files with 14 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
thue-morse.v
View File

@ -890,10 +890,20 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Lemma tm_step_next_range2' :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b
-> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
Proof.
intros n k b. intros H. assert (I := H).
apply nth_error_split in H. destruct H. destruct H. inversion H.
rewrite tm_build.
assert (J: k < 2^n).
rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt.
rewrite nth_error_app2. rewrite tm_size_power2.
rewrite Nat.add_sub. apply map_nth_error. apply I.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Lemma tm_step_consecutive_power2 :