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:30:53 +01:00
parent e0754cb433
commit 84a71a9e9d
1 changed files with 5 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
thue-morse.v
View File

@ -834,18 +834,9 @@ Qed.
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
l = l1 ++ b :: l2 -> length l1 < length l.
Proof.
intros l l1 l2 b. intros H.
assert (I: l = (l1 ++ b::nil) ++ l2).
{ rewrite H. rewrite <- app_assoc. reflexivity. }
assert (J: length (l1 ++ b::nil) <= length l).
{ rewrite I.
replace (length ((l1 ++ [b]) ++ l2)) with
(length (l1 ++ [b]) + length l2).
apply Nat.le_add_r.
symmetry. apply app_length. }
rewrite last_length in J. assert (L: length l1 < S (length l1)).
apply Nat.lt_succ_diag_r. generalize J. generalize L.
apply Nat.lt_le_trans.
intros l l1 l2 b. intros H. rewrite H.
rewrite app_length. simpl. apply Nat.lt_add_pos_r.
apply Nat.lt_0_succ.
Qed.
Lemma list_concat_to_pos : forall (l l1 l2 : list bool) (b : bool),
@ -865,9 +856,9 @@ Lemma tm_step_next_range :
-> nth_error (tm_step (S n)) (length l1) = Some b.
Proof.
intros n l1 l2 b. intros H.
assert (nth_error (tm_step n) (length l1) = Some b).
assert (I: nth_error (tm_step n) (length l1) = Some b).
generalize H. apply list_concat_to_pos.
rewrite tm_build. rewrite nth_error_app1. apply H0.
rewrite tm_build. rewrite nth_error_app1. apply I.
generalize H. apply list_app_length_lt.
Qed.