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-23 09:08:09 +01:00
parent 3195f3eb4e
commit 4b36fa4531
1 changed files with 17 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
thue-morse.v
View File

@ -859,7 +859,6 @@ Proof.
rewrite nth_middle in L. apply L. rewrite H. reflexivity.
Qed.
Lemma tm_step_next_range :
forall (n : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2
@ -869,12 +868,25 @@ Proof.
assert (nth_error (tm_step n) (length l1) = Some b).
generalize H. apply list_concat_to_pos.
rewrite tm_build.
assert (I: length l1 < 2^n).
rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
rewrite nth_error_app1. apply H0.
rewrite tm_size_power2. apply I.
assert (length l1 < length (tm_step n)).
generalize H. apply list_app_length_lt.
rewrite nth_error_app1. apply H0. apply H1.
Qed.
Lemma tm_step_next_range' :
forall (n k : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2
-> nth_error (tm_step (n + k)) (length l1) = Some b.
Proof.
intros n k l1 l2 b. intros H.
induction k.
- rewrite Nat.add_0_r. generalize H. apply list_concat_to_pos.
- rewrite Nat.add_succ_r.
simpl.
apply nth_error_split in IHk.
Lemma tm_step_next_range2 :
forall (n : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2