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:12:13 +01:00
parent 85418e959b
commit 2600e6ca69
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
thue-morse.v
View File

@ -615,19 +615,16 @@ Proof.
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)).
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S 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.
simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k).
apply Nat.add_lt_mono; assumption.
rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
simpl. rewrite Nat.add_1_r. reflexivity. reflexivity.
Qed.