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:56:36 +01:00
parent c34cd4da2e
commit dfe275c9b0
1 changed files with 12 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
thue-morse.v
View File

@ -972,14 +972,15 @@ Qed.
Lemma tm_step_add_range2_neighbor : forall (n m k : nat), Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
S k < 2^n -> S k < 2^n ->
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false) eqb (nth k (tm_step n) false)
= eqb (nth (S k) (tm_step n) false)
(nth (k + 2^(n+m)) (tm_step (S n+m)) false) (nth (S k + 2^(n+m)) (tm_step (S n+m)) false). = eqb (nth (k + 2^(n+m)) (tm_step (S n+m)) false)
(nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
Proof. Proof.
intros n m k. intros H. intros n m k. intros H.
induction m. induction m.
- rewrite Nat.add_0_r. rewrite Nat.add_0_r. apply tm_step_next_range2_neighbor. - rewrite Nat.add_0_r. rewrite Nat.add_0_r.
apply H. apply tm_step_next_range2_neighbor. apply H.
- rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. - rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
assert (I : eqb (nth k (tm_step (S n + m)) false) assert (I : eqb (nth k (tm_step (S n + m)) false)
@ -1008,7 +1009,8 @@ Proof.
assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)). assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
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_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.
@ -1016,9 +1018,11 @@ Proof.
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. inversion H6. rewrite H8. reflexivity. rewrite H3 in H6. rewrite H5 in H6. inversion H6. rewrite H8. reflexivity.
Qed. Qed.