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-29 10:45:51 +01:00
parent 0e43274f90
commit ea8e07d20d
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
thue-morse.v
View File

@ -681,11 +681,14 @@ Proof.
apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
assumption.
assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0).
generalize I. generalize L. apply Nat.lt_trans.
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
apply tm_step_succ_double_index.
generalize I. generalize L. apply Nat.lt_trans.
assumption.
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
@ -728,8 +731,8 @@ Proof.
simpl; split; reflexivity.
assumption. rewrite tm_size_power2. assumption. assumption.
rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans.
rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans.
rewrite tm_size_power2. assumption.
rewrite tm_size_power2. assumption.
rewrite tm_size_power2. assumption.
rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.