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 17:33:35 +01:00
parent f0358d7381
commit ba5ba7b2da
1 changed files with 11 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
thue-morse.v
View File

@ -872,7 +872,7 @@ Proof.
apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
Qed.
Lemma tm_add_range : forall (n m k : nat),
Lemma tm_step_add_range : forall (n m k : nat),
k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
Proof.
intros n m k. intros H.
@ -892,14 +892,14 @@ Proof.
intros n m k. intros.
assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
apply Nat.max_spec. destruct I.
- destruct H1. replace (m) with (n + (m-n)). apply tm_add_range. apply H.
- destruct H1. replace (m) with (n + (m-n)). apply tm_step_add_range. apply H.
apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (n <= n). apply le_n. symmetry.
replace (m) with (m + (n-n)) at 1. generalize H3.
apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
reflexivity.
- destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_add_range.
- destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_step_add_range.
apply H0. replace (n) with (m + n - m) at 2. generalize H1.
apply Nat.add_sub_assoc. rewrite Nat.add_comm.
assert (m <= m). apply le_n. symmetry.
@ -939,13 +939,13 @@ Proof.
rewrite tm_size_power2. apply Nat.le_add_l.
Qed.
Lemma tm_step_next_range2_neighbor : forall (n m k : nat),
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
S k < 2^n ->
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
= eqb
(nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
Proof.
intros n m k. intros H. rewrite <- tm_size_power2 in H.
intros n k. intros H. rewrite <- tm_size_power2 in H.
assert (I := H). apply Nat.lt_succ_l in I.
assert (J : nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
generalize I. apply nth_error_nth'.
@ -970,9 +970,12 @@ Proof.
rewrite L. rewrite M. reflexivity.
Qed.
Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
S k < 2^n ->
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
= eqb
(nth (k + 2^n) (tm_step (n+m)) false) (nth (S k + 2^n) (tm_step (n+m)) false).
Proof.