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:45:40 +01:00
parent abfb4f4166
commit 64d342bbdf
1 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
thue-morse.v
View File

@ -881,7 +881,6 @@ Proof.
Qed. Qed.
(*
Lemma tm_step_next_range : Lemma tm_step_next_range :
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
@ -891,11 +890,11 @@ Proof.
assert (nth_error (tm_step n) (length l1) = Some b). assert (nth_error (tm_step n) (length l1) = Some b).
generalize H. apply list_concat_to_pos. generalize H. apply list_concat_to_pos.
rewrite tm_build. rewrite tm_build.
rewrite nth_error_app1. 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.
Qed.
Lemma tm_step_next_range2 : Lemma tm_step_next_range2 :
forall (n : nat) (l1 l2 : list bool) (b : bool), forall (n : nat) (l1 l2 : list bool) (b : bool),
@ -909,6 +908,11 @@ Proof.
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 + 2^n - 2^n) with (length l1).
apply map_nth_error. apply H0.
rewrite Nat.add_sub. reflexivity.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.