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-10 22:39:37 +01:00
parent 39b4aa0626
commit e4e0052d90
1 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
thue-morse.v
View File

@ -1231,6 +1231,10 @@ Proof.
(* k < 0 *)
rename H0 into G.
assert (O: k*2^m + 2^j < 2^n).
apply lt_split_bits. assumption. assumption. assumption.
assert ( nth_error (tm_step m) 0
= nth_error (tm_step m) (2^j)
<-> nth_error (tm_step (m+n)) (k * 2^m + 0)
@ -1263,16 +1267,11 @@ Proof.
assert (Some false = Some false). reflexivity.
apply H1 in H2. rewrite H2 at 1. easy. easy.
rewrite nth_error_nth' with (d := false). easy.
rewrite tm_size_power2. apply lt_split_bits.
assumption. assumption. assumption.
rewrite tm_size_power2. assumption.
apply tm_step_stable. assumption.
apply tm_step_stable. apply lt_split_bits.
assumption. assumption. assumption.
assert (k*2^m + 2^j < 2^n).
apply lt_split_bits.
assumption. assumption. assumption.
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
generalize H2. generalize H1. apply Nat.lt_le_trans.
generalize H1. generalize O. apply Nat.lt_le_trans.
apply tm_step_stable. assumption.
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.