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-25 06:52:31 +01:00
parent 315e67aa5d
commit 7fc74784db
1 changed files with 28 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
thue-morse.v
View File

@ -939,6 +939,34 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l. rewrite tm_size_power2. apply Nat.le_add_l.
Qed. Qed.
Lemma tm_step_next_range2'' :
forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
Proof.
intros n k. intros H.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
rewrite H0.
assert (nth_error (map negb (tm_step n)) k =
Some (negb (nth k (tm_step n) false))).
generalize H0. apply map_nth_error.
rewrite H1.
destruct (nth_error (tm_step n) k). rewrite <- H0. rewrite <- H0.
Lemma tm_step_next_range2_neighbor : forall (n k : nat), Lemma tm_step_next_range2_neighbor : forall (n k : nat),
S k < 2^n -> S k < 2^n ->
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false) eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)