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-12-15 15:41:36 +01:00
parent 2786ad33bd
commit 8065518a98
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
thue-morse.v
View File

@ -202,21 +202,20 @@ Proof.
reflexivity. rewrite tm_size_power2. easy.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
Proof.
intro n.
assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
rewrite nth_error_nth' with (d := false).
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag.
rewrite tm_step_end_1. reflexivity.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
apply rev_involutive. rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
rewrite rev_length. assumption. apply rev_involutive. assumption.
Qed.
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),