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 22:22:50 +01:00
parent 47a1c275cc
commit abfb4f4166
1 changed files with 13 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
thue-morse.v
View File

@ -882,17 +882,22 @@ Qed.
(* (*
Lemma nth_error_app : forall (l1 l2 : list bool) (k : nat), Lemma tm_step_next_range :
nth_error (l1 ++ l2) (k + length l1) = nth_error l2 k. forall (n : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2
-> nth_error (tm_step (S n)) (length l1) = Some b.
Proof. Proof.
intros n l1 l2 b. intros H.
nth_error_app2: assert (nth_error (tm_step n) (length l1) = Some b).
forall [A : Type] (l l' : list A) [n : nat], generalize H. apply list_concat_to_pos.
length l <= n -> nth_error (l ++ l') n = nth_error l' (n - length l) rewrite tm_build.
rewrite nth_error_app1.
*) *)
Lemma tm_step_next_range :
Lemma tm_step_next_range2 :
forall (n : nat) (l1 l2 : list bool) (b : bool), forall (n : nat) (l1 l2 : list bool) (b : bool),
tm_step n = l1 ++ b :: l2 tm_step n = l1 ++ b :: l2
-> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b). -> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b).
@ -903,8 +908,7 @@ Proof.
rewrite tm_build. rewrite tm_build.
assert (I: length l1 < 2^n). assert (I: length l1 < 2^n).
rewrite <- tm_size_power2. generalize H. apply list_app_length_lt. rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
rewrite nth_error_app2. rewrite <- tm_size_power2. rewrite nth_error_app2. rewrite tm_size_power2.
replace (length l1 + length (tm_step n) - length (tm_step n)) with (length l1).