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 21:46:41 +01:00
parent 326c44e2c6
commit 8fd8fbf561
1 changed files with 3 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
thue-morse.v
View File

@ -993,8 +993,7 @@ Proof.
assert (n < S n + S m). rewrite Nat.add_succ_comm. assert (n < S n + S m). rewrite Nat.add_succ_comm.
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ. apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1. generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
apply Nat.pow_lt_mono_r. generalize H0. generalize H. apply Nat.pow_lt_mono_r. generalize H0. generalize H. apply Nat.lt_trans.
apply Nat.lt_trans.
+ rewrite <- I. rewrite <- IHm. + rewrite <- I. rewrite <- IHm.
assert (U: S k < 2^(S n+m)). assert (U: S k < 2^(S n+m)).
@ -1012,26 +1011,17 @@ Proof.
generalize J. rewrite <- tm_size_power2. apply nth_error_nth'. generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)). assert (nth_error (tm_step (S n + m)) k = Some(nth k (tm_step (S n + m)) false)).
generalize K. rewrite <- tm_size_power2. apply nth_error_nth'. generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
(* assert (nth k (tm_step n) false = nth k (tm_step (S n + m)) false). *)
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k). assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
generalize K. generalize J. apply tm_step_stable. generalize K. generalize J. apply tm_step_stable.
rewrite <- H2 in H1. rewrite H0 in H1. inversion H1. rewrite H4.
rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
rewrite H4.
assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)). assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'. generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)). assert (nth_error (tm_step (S n + m)) (S k) = Some(nth (S k) (tm_step (S n + m)) false)).
generalize U. rewrite <- tm_size_power2. apply nth_error_nth'. generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)). assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
generalize U. generalize H. apply tm_step_stable. generalize U. generalize H. apply tm_step_stable.
rewrite H3 in H6. rewrite H5 in H6. rewrite H3 in H6. rewrite H5 in H6. inversion H6. rewrite H8. reflexivity.
inversion H6. rewrite H8.
reflexivity.
Qed. Qed.