Update
This commit is contained in:
parent
bb3687969e
commit
d27fdab010
50
thue-morse.v
50
thue-morse.v
@ -1192,11 +1192,43 @@ Qed.
|
||||
|
||||
Theorem tm_step_flip_low_bit :
|
||||
forall (n m k j : nat),
|
||||
0 < k -> j < m -> k * 2^m < 2^n
|
||||
j < m -> k * 2^m < 2^n
|
||||
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
|
||||
Proof.
|
||||
intros n m k j. intros G H I.
|
||||
intros n m k j. intros H I.
|
||||
|
||||
assert (L: nth_error (tm_step m) 0 = Some false).
|
||||
rewrite tm_step_head_1. simpl. reflexivity.
|
||||
|
||||
assert (M: 2^j < 2^m).
|
||||
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
||||
|
||||
assert (N: nth_error (tm_step m) (2^j) = Some true).
|
||||
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
||||
rewrite tm_step_single_bit_index. reflexivity.
|
||||
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
||||
rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
|
||||
apply Nat.lt_1_2.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
apply Nat.le_0_l. assumption.
|
||||
|
||||
assert (G: k = 0 \/ 0 < k). apply Nat.eq_0_gt_0_cases.
|
||||
destruct G.
|
||||
|
||||
(* k = 0 *)
|
||||
rewrite H0. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
|
||||
replace (nth_error (tm_step n) 0) with (Some false).
|
||||
assert (S: n < S j \/ S j <= n). apply Nat.lt_ge_cases.
|
||||
destruct S. rewrite Nat.lt_succ_r in H1.
|
||||
apply Nat.pow_le_mono_r with (a := 2) in H1.
|
||||
rewrite <- tm_size_power2 in H1. rewrite <- nth_error_None in H1.
|
||||
rewrite H1. easy. easy.
|
||||
rewrite Nat.le_succ_l in H1. apply Nat.pow_lt_mono_r with (a := 2) in H1.
|
||||
rewrite tm_step_stable with (m := m). rewrite N. easy. assumption. assumption.
|
||||
apply Nat.lt_1_2. rewrite tm_step_head_1. simpl. reflexivity.
|
||||
|
||||
(* k < 0 *)
|
||||
rename H0 into G.
|
||||
assert ( nth_error (tm_step m) 0
|
||||
= nth_error (tm_step m) (2^j)
|
||||
<-> nth_error (tm_step (m+n)) (k * 2^m + 0)
|
||||
@ -1217,8 +1249,7 @@ Proof.
|
||||
with (nth_error (tm_step n) (k * 2 ^ m)) in H0.
|
||||
replace (nth_error (tm_step (m + n)) (k * 2 ^ m + 2^j))
|
||||
with (nth_error (tm_step n) (k * 2 ^ m + 2^j)) in H0.
|
||||
replace (nth_error (tm_step m) 0) with (Some false) in H0.
|
||||
replace (nth_error (tm_step m) (2^j)) with (Some true) in H0.
|
||||
rewrite L in H0. rewrite N in H0.
|
||||
|
||||
destruct (nth_error (tm_step n) (k * 2 ^ m)).
|
||||
destruct (nth_error (tm_step n) (k * 2 ^ m + 2^j)).
|
||||
@ -1232,15 +1263,6 @@ Proof.
|
||||
rewrite nth_error_nth' with (d := false). easy.
|
||||
rewrite tm_size_power2. apply lt_split_bits.
|
||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
||||
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
||||
rewrite tm_step_single_bit_index. reflexivity.
|
||||
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
||||
rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
|
||||
apply Nat.lt_1_2.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
apply Nat.le_0_l. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||
assumption.
|
||||
rewrite tm_step_head_1. simpl. reflexivity.
|
||||
|
||||
apply tm_step_stable. apply lt_split_bits.
|
||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
||||
@ -1255,6 +1277,8 @@ Proof.
|
||||
generalize H1. generalize I. apply Nat.lt_le_trans.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
(* vérifier si les deux sont nécessaires *)
|
||||
Require Import BinPosDef.
|
||||
Require Import BinPos.
|
||||
|
Loading…
Reference in New Issue
Block a user