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-12-15 16:03:55 +01:00
parent 8065518a98
commit 85418e959b
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

@ -614,7 +614,21 @@ Proof.
generalize P. generalize I. apply Nat.lt_le_trans. generalize P. generalize I. apply Nat.lt_le_trans.
Qed. Qed.
Lemma tm_step_succ_double_index : forall (n k : nat),
2 * k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step n) (S (2*k)).
Proof.
intros n k. intro H. rewrite tm_step_double_index.
replace (nth_error (tm_step (S n)) (2*k)) with (nth_error (tm_step n) (2*k)).
rewrite Nat.mul_comm. replace (2) with (2^1).
replace (S (k*2^1)) with (k*2^1 + 2^0).
apply tm_step_flip_low_bit. apply Nat.lt_0_1.
simpl. rewrite Nat.mul_comm. assumption.
rewrite Nat.add_1_r. reflexivity. easy.
apply tm_step_stable. assumption.
assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r.
apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
generalize H0. generalize H. apply Nat.lt_trans.
Qed.