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-26 07:44:20 +01:00
parent a8cdd31830
commit e885bb3a7e
1 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
thue-morse.v
View File

@ -904,7 +904,7 @@ Proof.
Qed.
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
Proof.
intros n m k. intros.
assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
@ -1089,11 +1089,26 @@ Lemma tm_step_cancel_high_bits :
<-> odd n = true.
Proof.
intros k b n m. intros H I.
assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
<-> odd n = true).
rewrite tm_step_single_bit_index.
assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
apply tm_step_stable.
assert (2^n - 1 < 2^n).
apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
rewrite Nat.succ_lt_mono. simpl.
(*
assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
apply tm_step_repunit.
*)
Lemma tm_step_next_range :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
Theorem tm_step_stable : forall (n m k : nat),
k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.