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-12-10 18:16:27 +01:00
parent 2857ebad62
commit a4b2592b01
1 changed files with 6 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
thue-morse.v
View File

@ -1197,22 +1197,6 @@ Proof.
generalize H2. generalize J. apply Nat.le_trans. generalize H2. generalize J. apply Nat.le_trans.
Qed. Qed.
Lemma tm_step_add_small_power2 :
forall (n m j : nat),
j < m
-> forall k, k < 2^n -> nth_error (tm_step m) 0
= nth_error (tm_step m) (2^j)
<-> nth_error (tm_step (m+n)) (k * 2^m )
= nth_error (tm_step (m+n)) (k * 2^m + (2^j)).
Proof.
intros n m j. intros H. intro k.
replace (k*2^m) with (k*2^m+0) at 1.
apply tm_step_repeating_patterns.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
rewrite Nat.add_0_r. reflexivity.
Qed.
Theorem tm_step_flip_low_bit : Theorem tm_step_flip_low_bit :
forall (n m k j : nat), forall (n m k j : nat),
0 < k -> j < m -> k * 2^m < 2^n 0 < k -> j < m -> k * 2^m < 2^n
@ -1222,16 +1206,19 @@ Proof.
assert ( nth_error (tm_step m) 0 assert ( nth_error (tm_step m) 0
= nth_error (tm_step m) (2^j) = nth_error (tm_step m) (2^j)
<-> nth_error (tm_step (m+n)) (k * 2^m) <-> nth_error (tm_step (m+n)) (k * 2^m + 0)
= nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ). = nth_error (tm_step (m+n)) (k * 2^m + (2^j)) ).
apply tm_step_add_small_power2. apply tm_step_repeating_patterns.
assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg. assert (1 * k <= (2^m) * k). apply Nat.mul_le_mono_nonneg.
apply Nat.le_0_1. rewrite Nat.le_succ_l. apply Nat.le_0_1. rewrite Nat.le_succ_l.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0. apply Nat.le_0_l. apply Nat.le_refl. rewrite Nat.mul_1_l in H0.
rewrite Nat.mul_comm in H0. rewrite Nat.mul_comm in H0.
generalize I. generalize H0. apply Nat.le_lt_trans. generalize I. generalize H0. apply Nat.le_lt_trans.
rewrite Nat.add_0_r in H0.
replace (nth_error (tm_step (m + n)) (k * 2 ^ m)) replace (nth_error (tm_step (m + n)) (k * 2 ^ m))
with (nth_error (tm_step n) (k * 2 ^ m)) in H0. with (nth_error (tm_step n) (k * 2 ^ m)) in H0.
@ -1280,10 +1267,6 @@ Qed.
Require Import BinNat. Require Import BinNat.
Require Import BinPosDef. Require Import BinPosDef.
Require Import BinPos. Require Import BinPos.