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-11-22 18:30:05 +01:00
parent cd8f78090e
commit 1ae999e04a
1 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
thue-morse.v
View File

@ -681,6 +681,8 @@ A010060 Thue-Morse sequence: let A_k denote the first 2^k terms; then A_0 = 0 a
*)
Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import Nat.
Require Import Nat.
Require Import Bool.
@ -804,8 +806,8 @@ Proof.
- simpl tm_step. rewrite tm_morphism_rev.
replace (tm_morphism (tm_step n)) with (tm_step (S n)).
rewrite IHn. simpl tm_morphism. simpl tl.
rewrite PeanoNat.Nat.even_succ.
rewrite PeanoNat.Nat.odd_succ.
rewrite Nat.even_succ.
rewrite Nat.odd_succ.
rewrite negb_involutive.
reflexivity. reflexivity.
Qed.
@ -825,7 +827,7 @@ Proof.
destruct n.
- reflexivity.
- rewrite tm_step_end_2. simpl.
rewrite PeanoNat.Nat.odd_succ.
rewrite Nat.odd_succ.
reflexivity.
Qed.
@ -867,13 +869,18 @@ Proof.
rewrite H1. easy.
rewrite nth_error_Some in I. rewrite tm_size_power2 in I.
assert (2^k <= length l1 + 2^k).
apply PeanoNat.Nat.le_add_l.
apply Nat.le_add_l.
generalize I. generalize H3.
apply PeanoNat.Nat.le_lt_trans.
apply Nat.le_lt_trans.
}
assert (k < n). {
generalize H3. apply PeanoNat.Nat.pow_lt_mono_r_iff.
generalize H3. apply Nat.pow_lt_mono_r_iff.
BEFORE REPLACEMENT.