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 23:10:30 +01:00
parent 5f373c7859
commit 27cdbf88b2
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
thue-morse.v
View File

@ -786,8 +786,7 @@ Proof.
induction n.
- reflexivity.
- simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
rewrite IHn. simpl. reflexivity.
simpl. reflexivity.
rewrite IHn. reflexivity. reflexivity.
Qed.
Lemma tm_step_end_2 : forall (n : nat),
@ -831,7 +830,7 @@ Proof.
rewrite tm_build.
rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
replace (true) with (negb false). apply map_nth_error.
rewrite tm_step_head_1. simpl. reflexivity.
rewrite tm_step_head_1. reflexivity.
reflexivity. rewrite tm_size_power2. easy.
Qed.
@ -845,7 +844,7 @@ Proof.
rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
rewrite Nat.sub_diag. rewrite tm_step_end_1.
simpl. reflexivity.
reflexivity.
rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
@ -1201,7 +1200,7 @@ Proof.
intros n m k j. intros H I.
assert (L: nth_error (tm_step m) 0 = Some false).
rewrite tm_step_head_1. simpl. reflexivity.
rewrite tm_step_head_1. reflexivity.
assert (M: 2^j < 2^m).
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.