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 10:19:48 +01:00
parent 84a71a9e9d
commit 0c970f9666
1 changed files with 7 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
thue-morse.v
View File

@ -863,16 +863,14 @@ Proof.
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.
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = 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.
intros n k b. intros H. assert (I := H).
apply nth_error_split in H. destruct H. destruct H. inversion H.
rewrite tm_build. rewrite nth_error_app1. apply I.
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
Qed.