Update
This commit is contained in:
Thomas Baruchel
parent
29890ef332
commit
099a6a85e9
145
thue-morse.v
145
thue-morse.v
|
|
@ -839,29 +839,6 @@ Proof.
|
|||
apply Nat.lt_0_succ.
|
||||
Qed.
|
||||
|
||||
Lemma list_concat_to_pos : forall (l l1 l2 : list bool) (b : bool),
|
||||
l = l1 ++ b :: l2 -> nth_error l (length l1) = Some b.
|
||||
Proof.
|
||||
intros l l1 l2 b. intros H.
|
||||
assert (I: length l1 < length l). generalize H. apply list_app_length_lt.
|
||||
assert (L: nth_error l (length l1) = Some (nth (length l1) l false)).
|
||||
{ apply nth_error_nth'. apply I. }
|
||||
replace (nth (length l1) l false) with (nth (length l1) (l1++b::l2) false) in L.
|
||||
rewrite nth_middle in L. apply L. rewrite H. reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range :
|
||||
forall (n : nat) (l1 l2 : list bool) (b : bool),
|
||||
tm_step n = l1 ++ b :: l2
|
||||
-> nth_error (tm_step (S n)) (length l1) = Some b.
|
||||
Proof.
|
||||
intros n l1 l2 b. intros H.
|
||||
assert (I: nth_error (tm_step n) (length l1) = Some b).
|
||||
generalize H. apply list_concat_to_pos.
|
||||
rewrite tm_build. rewrite nth_error_app1. apply I.
|
||||
generalize H. apply list_app_length_lt.
|
||||
Qed.
|
||||
|
||||
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.
|
||||
|
|
@ -908,37 +885,6 @@ Proof.
|
|||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range2 :
|
||||
forall (n : nat) (l1 l2 : list bool) (b : bool),
|
||||
tm_step n = l1 ++ b :: l2
|
||||
-> nth_error (tm_step (S n)) (length l1 + 2^n) = Some (negb b).
|
||||
Proof.
|
||||
intros n l1 l2 b. intros H.
|
||||
assert (nth_error (tm_step n) (length l1) = Some b).
|
||||
generalize H. apply list_concat_to_pos.
|
||||
rewrite tm_build.
|
||||
assert (I: length l1 < 2^n).
|
||||
rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
|
||||
rewrite nth_error_app2. rewrite tm_size_power2.
|
||||
rewrite Nat.add_sub. apply map_nth_error. apply H0.
|
||||
rewrite tm_size_power2. apply Nat.le_add_l.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range2' :
|
||||
forall (n k : nat) (b : bool),
|
||||
nth_error (tm_step n) k = Some b
|
||||
-> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
|
||||
Proof.
|
||||
intros n k b. intros H. assert (I := H).
|
||||
apply nth_error_split in H. destruct H. destruct H. inversion H.
|
||||
rewrite tm_build.
|
||||
assert (J: k < 2^n).
|
||||
rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt.
|
||||
rewrite nth_error_app2. rewrite tm_size_power2.
|
||||
rewrite Nat.add_sub. apply map_nth_error. apply I.
|
||||
rewrite tm_size_power2. apply Nat.le_add_l.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range2'' :
|
||||
forall (n k : nat),
|
||||
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
|
||||
|
|
@ -956,37 +902,6 @@ Proof.
|
|||
rewrite tm_size_power2. apply Nat.le_add_l.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
||||
S k < 2^n ->
|
||||
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
|
||||
= eqb
|
||||
(nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
|
||||
Proof.
|
||||
intros n k. intros H. rewrite <- tm_size_power2 in H.
|
||||
assert (I := H). apply Nat.lt_succ_l in I.
|
||||
assert (J : nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
||||
generalize I. apply nth_error_nth'.
|
||||
assert (K : nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
|
||||
generalize H. apply nth_error_nth'.
|
||||
assert (L := J). apply tm_step_next_range2' in L.
|
||||
assert (M := K). apply tm_step_next_range2' in M.
|
||||
destruct (nth k (tm_step n) false).
|
||||
destruct (nth (S k) (tm_step n) false).
|
||||
apply nth_error_nth with (d :=false) in L.
|
||||
apply nth_error_nth with (d :=false) in M.
|
||||
rewrite L. rewrite M. reflexivity.
|
||||
apply nth_error_nth with (d :=false) in L.
|
||||
apply nth_error_nth with (d :=false) in M.
|
||||
rewrite L. rewrite M. reflexivity.
|
||||
destruct (nth (S k) (tm_step n) false).
|
||||
apply nth_error_nth with (d :=false) in L.
|
||||
apply nth_error_nth with (d :=false) in M.
|
||||
rewrite L. rewrite M. reflexivity.
|
||||
apply nth_error_nth with (d :=false) in L.
|
||||
apply nth_error_nth with (d :=false) in M.
|
||||
rewrite L. rewrite M. reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
|
||||
S k < 2^n ->
|
||||
nth_error (tm_step n) k = nth_error (tm_step n) (S k)
|
||||
|
|
@ -1132,66 +1047,6 @@ Qed.
|
|||
|
||||
|
||||
|
||||
Lemma tm_step_add_range2_neighbor0 : forall (n m k : nat),
|
||||
S k < 2^n ->
|
||||
eqb (nth k (tm_step n) false)
|
||||
(nth (S k) (tm_step n) false)
|
||||
= eqb (nth (k + 2^(n+m)) (tm_step (S n+m)) false)
|
||||
(nth (S k + 2^(n+m)) (tm_step (S n+m)) false).
|
||||
Proof.
|
||||
intros n m k. intros H.
|
||||
induction m.
|
||||
- rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
||||
apply tm_step_next_range2_neighbor. apply H.
|
||||
- rewrite IHm. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
|
||||
|
||||
assert (I : eqb (nth k (tm_step (S n + m)) false)
|
||||
(nth (S k) (tm_step (S n + m)) false)
|
||||
= eqb (nth (k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)
|
||||
(nth (S k + 2 ^ S (n + m)) (tm_step (S (S n + m))) false)).
|
||||
apply tm_step_next_range2_neighbor. induction m.
|
||||
+ rewrite Nat.add_0_r. simpl. generalize H. apply Nat.lt_lt_add_r.
|
||||
+ assert (2^n < 2^(S n + S m)).
|
||||
assert (n < S n + S m). rewrite Nat.add_succ_comm.
|
||||
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
|
||||
generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
|
||||
apply Nat.pow_lt_mono_r. generalize H0. generalize H. apply Nat.lt_trans.
|
||||
+ rewrite <- I. rewrite <- IHm.
|
||||
|
||||
assert (U: S k < 2^(S n+m)).
|
||||
assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
|
||||
assert (L: 2^n < 2^(S n + m)).
|
||||
assert (M: n < S n + m). rewrite Nat.add_succ_comm.
|
||||
apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
|
||||
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
|
||||
generalize L. generalize H. apply Nat.lt_trans.
|
||||
assert (K := U). apply Nat.lt_succ_l in K.
|
||||
|
||||
assert (J: k < 2^n). apply Nat.lt_succ_l. apply H.
|
||||
|
||||
assert (nth_error (tm_step n) k = Some(nth k (tm_step n) false)).
|
||||
generalize J. rewrite <- tm_size_power2. apply nth_error_nth'.
|
||||
assert (nth_error (tm_step (S n + m)) k
|
||||
= Some(nth k (tm_step (S n + m)) false)).
|
||||
generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
|
||||
assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
|
||||
generalize K. generalize J. apply tm_step_stable.
|
||||
rewrite <- H2 in H1. rewrite H0 in H1. inversion H1. rewrite H4.
|
||||
|
||||
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 + m)) (S k)
|
||||
= Some(nth (S k) (tm_step (S n + m)) false)).
|
||||
generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
|
||||
assert (nth_error (tm_step n) (S k)
|
||||
= nth_error (tm_step (S n + m)) (S k)).
|
||||
generalize U. generalize H. apply tm_step_stable.
|
||||
rewrite H3 in H6. rewrite H5 in H6. inversion H6. rewrite H8. reflexivity.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma tm_step_consecutive_power2 :
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user