Update
This commit is contained in:
parent
272abb67cf
commit
00fd7e39f1
157
thue-morse.v
157
thue-morse.v
@ -1012,145 +1012,78 @@ Proof.
|
|||||||
easy.
|
easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
Lemma tm_step_add_range2_flip_two : forall (n m j k : nat),
|
||||||
S k < 2^n ->
|
k < 2^n -> m < 2^n ->
|
||||||
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
nth_error (tm_step n) k = nth_error (tm_step n) m
|
||||||
<->
|
<->
|
||||||
nth_error (tm_step (S n)) (k + 2^n)
|
nth_error (tm_step (S n+j)) (k + 2^(n+j))
|
||||||
= nth_error (tm_step (S n)) (S k + 2^n).
|
= nth_error (tm_step (S n+j)) (m + 2^(n+j)).
|
||||||
Proof.
|
Proof.
|
||||||
intros n k. intros H.
|
intros n m j k. intros H I.
|
||||||
(* Part 1: preamble *)
|
assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
|
||||||
assert (I := H). apply Nat.lt_succ_l in I.
|
generalize H. apply Nat.add_lt_mono_r.
|
||||||
assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
|
assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
|
||||||
generalize I. apply tm_step_next_range2.
|
generalize I. apply Nat.add_lt_mono_r.
|
||||||
assert (nth_error (tm_step n) (S k) <> nth_error (tm_step (S n)) (S k + 2^n)).
|
|
||||||
generalize H. apply tm_step_next_range2.
|
|
||||||
assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
|
|
||||||
rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
|
|
||||||
assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
|
|
||||||
|
|
||||||
(* Part 2 *)
|
|
||||||
assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
|
||||||
generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
|
|
||||||
assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
|
|
||||||
generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
|
|
||||||
assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
|
|
||||||
Some (nth (k + 2^n) (tm_step (S n)) false)).
|
|
||||||
generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
|
|
||||||
apply nth_error_nth'.
|
|
||||||
assert (nth_error (tm_step (S n)) (S k + 2 ^ n) =
|
|
||||||
Some (nth (S k + 2^n) (tm_step (S n)) false)).
|
|
||||||
generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
|
|
||||||
apply nth_error_nth'.
|
|
||||||
rewrite H2. rewrite H3. rewrite H4. rewrite H5.
|
|
||||||
|
|
||||||
(* Part 3 *)
|
|
||||||
destruct (nth k (tm_step n) false).
|
|
||||||
destruct (nth (S k) (tm_step n) false).
|
|
||||||
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
easy.
|
|
||||||
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
|
|
||||||
easy.
|
|
||||||
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
|
|
||||||
easy.
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
easy.
|
|
||||||
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
|
|
||||||
destruct (nth (S k) (tm_step n) false).
|
|
||||||
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
|
|
||||||
easy.
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
easy.
|
|
||||||
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
|
|
||||||
destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
easy.
|
|
||||||
rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
|
|
||||||
destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
|
|
||||||
rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
|
|
||||||
easy.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
|
|
||||||
S k < 2^n ->
|
|
||||||
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
|
||||||
<->
|
|
||||||
nth_error (tm_step (S n+m)) (k + 2^(n+m))
|
|
||||||
= nth_error (tm_step (S n+m)) (S k + 2^(n+m)).
|
|
||||||
Proof.
|
|
||||||
intros n m k. intros H.
|
|
||||||
assert (I := H). apply Nat.lt_succ_l in I.
|
|
||||||
assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
|
|
||||||
rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
|
|
||||||
assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
|
|
||||||
|
|
||||||
split.
|
split.
|
||||||
- induction m.
|
- induction j.
|
||||||
+ intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
+ intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
||||||
apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
|
rewrite <- tm_step_next_range2_flip_two. apply L. apply H. apply I.
|
||||||
apply K.
|
|
||||||
rewrite <- tm_step_next_range2_neighbor.
|
|
||||||
apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
|
|
||||||
apply K.
|
|
||||||
rewrite <- tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
|
|
||||||
rewrite <- tm_step_next_range2_neighbor. apply L.
|
|
||||||
apply H. rewrite <- Nat.add_succ_l. apply K.
|
|
||||||
rewrite <- Nat.add_succ_l. apply K.
|
|
||||||
+ intros L.
|
+ intros L.
|
||||||
|
|
||||||
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
|
rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
|
||||||
|
|
||||||
assert (S k < 2^(S n + m)).
|
assert (2^n < 2^(S n + j)).
|
||||||
assert (2^n < 2^(S n + m)).
|
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
|
||||||
assert (n < S n + m). assert (n < S n). apply Nat.lt_succ_diag_r.
|
|
||||||
generalize H0. apply Nat.lt_lt_add_r.
|
generalize H0. apply Nat.lt_lt_add_r.
|
||||||
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||||
|
assert (k < 2^(S n + j)).
|
||||||
generalize H0. generalize H. apply Nat.lt_trans.
|
generalize H0. generalize H. apply Nat.lt_trans.
|
||||||
assert (H1 := H0). apply Nat.lt_succ_l in H1.
|
assert (m < 2^(S n + j)).
|
||||||
|
generalize H0. generalize I. apply Nat.lt_trans.
|
||||||
|
|
||||||
rewrite <- tm_step_next_range2_neighbor.
|
rewrite <- tm_step_next_range2_flip_two.
|
||||||
|
|
||||||
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
|
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
|
||||||
generalize H1. generalize I. apply tm_step_stable.
|
generalize H1. generalize H. apply tm_step_stable.
|
||||||
assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
|
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
|
||||||
generalize H0. generalize H. apply tm_step_stable.
|
generalize H2. generalize I. apply tm_step_stable.
|
||||||
rewrite <- H2. rewrite <- H3. apply L.
|
rewrite <- H3. rewrite <- H4. apply L.
|
||||||
|
|
||||||
apply H0.
|
apply H1. apply H2.
|
||||||
- induction m.
|
- induction j.
|
||||||
+ intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
|
+ intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
|
||||||
apply tm_step_next_range2_neighbor. apply H. apply L.
|
apply tm_step_next_range2_flip_two. apply H. apply I. apply L.
|
||||||
+ intros L.
|
+ intros L.
|
||||||
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
|
rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
|
||||||
|
|
||||||
assert (S k < 2^(S n + m)).
|
assert (2^n < 2^(S n + j)).
|
||||||
assert (2^n < 2^(S n + m)).
|
assert (n < S n + j). assert (n < S n). apply Nat.lt_succ_diag_r.
|
||||||
assert (n < S n + m). assert (n < S n). apply Nat.lt_succ_diag_r.
|
|
||||||
generalize H0. apply Nat.lt_lt_add_r.
|
generalize H0. apply Nat.lt_lt_add_r.
|
||||||
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
generalize H0. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||||
|
assert (k < 2^(S n + j)).
|
||||||
generalize H0. generalize H. apply Nat.lt_trans.
|
generalize H0. generalize H. apply Nat.lt_trans.
|
||||||
assert (H1 := H0). apply Nat.lt_succ_l in H1.
|
assert (m < 2^(S n + j)).
|
||||||
|
generalize H0. generalize I. apply Nat.lt_trans.
|
||||||
|
|
||||||
rewrite <- tm_step_next_range2_neighbor in L.
|
rewrite <- tm_step_next_range2_flip_two in L.
|
||||||
|
|
||||||
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
|
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + j)) k).
|
||||||
generalize H1. generalize I. apply tm_step_stable.
|
generalize H1. generalize H. apply tm_step_stable.
|
||||||
assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
|
assert (nth_error (tm_step n) m = nth_error (tm_step (S n + j)) m).
|
||||||
generalize H0. generalize H. apply tm_step_stable.
|
generalize H2. generalize I. apply tm_step_stable.
|
||||||
rewrite <- H2 in L. rewrite <- H3 in L. apply L.
|
rewrite <- H3 in L. rewrite <- H4 in L. apply L.
|
||||||
|
|
||||||
apply H0.
|
apply H1. apply H2.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_cancel_high_bits :
|
Lemma tm_step_cancel_high_bits :
|
||||||
forall (k b n m : nat),
|
forall (k b n m : nat),
|
||||||
(* every natral number k can be written according to the following form *)
|
(* every natral number k can be written according to the following form *)
|
||||||
|
Loading…
Reference in New Issue
Block a user