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 08:43:13 +01:00
parent 787dab1159
commit 81386e67d4
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
thue-morse.v
View File

@ -1209,23 +1209,23 @@ Proof.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
assumption. assumption.
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases. destruct G. assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
destruct G as [G1|G2].
(* k = 0 *) (* k = 0 *)
rewrite H0. rewrite Nat.mul_0_l. rewrite Nat.add_0_l. rewrite G1. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
replace (nth_error (tm_step n) 0) with (Some false). replace (nth_error (tm_step n) 0) with (Some false).
assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases. assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
destruct S. rewrite Nat.lt_succ_r in H1. destruct S. rewrite Nat.lt_succ_r in H0.
apply Nat.pow_le_mono_r with (a := 2) in H1. apply Nat.pow_le_mono_r with (a := 2) in H0.
rewrite <- tm_size_power2 in H1. rewrite <- nth_error_None in H1. rewrite <- tm_size_power2 in H0. rewrite <- nth_error_None in H0.
rewrite H1. easy. easy. rewrite H0. easy. easy.
rewrite Nat.le_succ_l in H1. apply Nat.pow_lt_mono_r with (a := 2) in H1. rewrite Nat.le_succ_l in H0. apply Nat.pow_lt_mono_r with (a := 2) in H0.
rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption. rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity. apply Nat.lt_1_2. rewrite tm_step_head_1. reflexivity.
(* k < 0 *) (* k < 0 *)
rename H0 into G.
assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption. assert (O: k*2^m + 2^j < 2^n). apply lt_split_bits; assumption.
assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l. assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.