Update
This commit is contained in:
parent
2600e6ca69
commit
3a48fbe5d0
70
thue-morse.v
70
thue-morse.v
@ -42,6 +42,40 @@ Proof.
|
||||
reflexivity. rewrite negb_involutive. reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma lt_split_bits : forall n m k j,
|
||||
0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
|
||||
Proof.
|
||||
intros n m k j. intros H I J.
|
||||
|
||||
assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
|
||||
apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
|
||||
|
||||
assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
|
||||
|
||||
assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
|
||||
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
|
||||
apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
|
||||
apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
|
||||
replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
|
||||
apply Nat.mul_le_mono_r with (p := 2^m) in H0.
|
||||
rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
|
||||
rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
|
||||
|
||||
rewrite Nat.add_le_mono_r with (p := j) in H0.
|
||||
assert (2^n - 2^m + j < 2^n).
|
||||
rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
|
||||
rewrite Nat.add_lt_mono_r with (p := 2^m).
|
||||
rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
|
||||
rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
|
||||
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
generalize H1. generalize H0. apply Nat.le_lt_trans.
|
||||
apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
|
||||
apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
|
||||
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
Qed.
|
||||
|
||||
Lemma tm_morphism_concat : forall (l1 l2 : list bool),
|
||||
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
||||
Proof.
|
||||
@ -423,40 +457,6 @@ Proof.
|
||||
apply H1. apply H2.
|
||||
Qed.
|
||||
|
||||
Lemma lt_split_bits : forall n m k j,
|
||||
0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
|
||||
Proof.
|
||||
intros n m k j. intros H I J.
|
||||
|
||||
assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
|
||||
apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
|
||||
|
||||
assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
|
||||
|
||||
assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
|
||||
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
|
||||
apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
|
||||
apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
|
||||
replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
|
||||
apply Nat.mul_le_mono_r with (p := 2^m) in H0.
|
||||
rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
|
||||
rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
|
||||
|
||||
rewrite Nat.add_le_mono_r with (p := j) in H0.
|
||||
assert (2^n - 2^m + j < 2^n).
|
||||
rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
|
||||
rewrite Nat.add_lt_mono_r with (p := 2^m).
|
||||
rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
|
||||
rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
|
||||
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
generalize H1. generalize H0. apply Nat.le_lt_trans.
|
||||
apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
|
||||
apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
|
||||
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_repeating_patterns :
|
||||
forall (n m i j : nat),
|
||||
i < 2^m -> j < 2^m
|
||||
@ -614,7 +614,7 @@ Proof.
|
||||
generalize P. generalize I. apply Nat.lt_le_trans.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_succ_double_index : forall (n k : nat),
|
||||
Theorem tm_step_succ_double_index : forall (n k : nat),
|
||||
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
|
||||
Proof.
|
||||
intros n k. intro H. rewrite tm_step_double_index.
|
||||
|
Loading…
Reference in New Issue
Block a user