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 2023-01-06 17:36:17 +01:00
parent d3bc94288a
commit 8a6141073c
1 changed files with 15 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/thue_morse.v
View File

@ -347,19 +347,18 @@ Proof.
destruct k.
- rewrite Nat.mul_0_r. rewrite tm_step_head_1. simpl.
rewrite tm_step_head_1. reflexivity.
- rewrite <- tm_step_lemma.
rewrite tm_morphism_double_index. reflexivity.
- rewrite <- tm_step_lemma. apply tm_morphism_double_index.
Qed.
Lemma tm_step_single_bit_index : forall (n : nat),
nth_error (tm_step (S n)) (2^n) = Some true.
Proof.
intro n.
rewrite tm_build. rewrite nth_error_app2.
- rewrite tm_size_power2. rewrite Nat.sub_diag.
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. reflexivity. reflexivity.
- rewrite tm_size_power2. apply Nat.le_refl.
- apply Nat.le_refl.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
@ -414,7 +413,7 @@ Lemma tm_step_add_range : forall (n m k : nat),
Proof.
intros n m k. intro H.
induction m.
- rewrite Nat.add_comm. reflexivity.
- rewrite Nat.add_0_r. reflexivity.
- rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize H. apply nth_error_nth'.
@ -434,15 +433,13 @@ Proof.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (n <= n). apply le_n. symmetry.
replace (m) with (m + (n-n)) at 1. generalize H3.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
reflexivity.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. apply Nat.add_0_r.
- destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
apply H0. replace (n) with (m + n - m) at 2. generalize H1.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (m <= m). apply le_n. symmetry.
replace (n) with (n + (m-m)) at 1. generalize H3.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
reflexivity.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. apply Nat.add_0_r.
Qed.
(**
@ -512,11 +509,11 @@ Proof.
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
rewrite Nat.add_comm. reflexivity. assumption.
apply Nat.add_comm. assumption.
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
rewrite Nat.add_comm. reflexivity. assumption.
apply Nat.add_comm. assumption.
rewrite tm_size_power2.
assert (k*2^m <= k*2^m + j). apply Nat.le_add_r.
@ -709,7 +706,7 @@ Proof.
assert (N: nth_error (tm_step m) (2^j) = Some true).
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
rewrite tm_step_single_bit_index. reflexivity.
apply tm_step_single_bit_index.
apply tm_step_stable.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
assumption.
@ -948,7 +945,7 @@ Proof.
rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
apply app_assoc_reverse.
assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I.
assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false).
@ -978,11 +975,11 @@ Proof.
rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3.
rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3.
assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l.
rewrite app_assoc_reverse. reflexivity.
apply app_assoc_reverse.
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
rewrite app_assoc_reverse. rewrite app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity.
apply app_assoc_reverse.
apply app_assoc_reverse.
Qed.
@ -1262,7 +1259,7 @@ Proof.
generalize H0. symmetry in M. generalize M.
replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3.
rewrite app_assoc_reverse. apply app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
apply app_assoc_reverse.
assert (hd2 ++ b ++ b ++ b ++ tl2
= (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n)))
++ (tm_morphism (firstn (Nat.div2 (length b))