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:31:44 +01:00
parent ba491a33d3
commit 8604cc2d27
1 changed files with 7 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
thue-morse.v
View File

@ -628,10 +628,10 @@ Qed.
Lemma tm_step_pred : forall (n k m : nat),
S (2*k) * 2^m < 2^n -> (
S (2*k) * 2^m < 2^n ->
nth_error (tm_step n) (S (2*k) * 2^m)
= nth_error (tm_step n) (S (2*k) * 2^m - 1)
<-> odd m = true).
<-> odd m = true.
Proof.
intros n k m.
@ -730,26 +730,20 @@ Proof.
reflexivity.
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.
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 Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.
rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. reflexivity.
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity.
replace (2) with (2*1) at 1.
apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2.
apply Nat.le_succ_l. apply Nat.mul_pos_pos.
apply Nat.lt_0_succ. assumption. apply Nat.mul_1_r.
apply Nat.lt_0_2.
apply Nat.mul_comm.
apply Nat.mul_comm.
apply Nat.mul_comm. apply Nat.mul_comm.
Qed.