Update
This commit is contained in:
parent
a3f15b3984
commit
ef846b4fdc
172
thue-morse.v
172
thue-morse.v
@ -1113,169 +1113,27 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
|
|||||||
- induction m.
|
- induction m.
|
||||||
+ 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_neighbor'. apply H. apply L.
|
||||||
+
|
+ intros 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 + m)).
|
||||||
|
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.pow_lt_mono_r. apply Nat.lt_1_2.
|
||||||
|
generalize H0. generalize H. apply Nat.lt_trans.
|
||||||
|
assert (H1 := H0). apply Nat.lt_succ_l in H1.
|
||||||
|
|
||||||
|
rewrite <- tm_step_next_range2_neighbor' in L.
|
||||||
Theorem tm_step_stable : forall (n m k : nat),
|
|
||||||
k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
rewrite <- Nat.add_succ_l.
|
|
||||||
replace (2^(n + S m)) with (2^(n+m) + 2^(n+m)).
|
|
||||||
rewrite Nat.add_assoc.
|
|
||||||
rewrite Nat.add_assoc.
|
|
||||||
(* rewrite Nat.add_succ_r. *)
|
|
||||||
generalize L.
|
|
||||||
apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
- assert (k < length (tm_step n)). rewrite tm_size_power2. apply I.
|
|
||||||
apply nth_error_nth' with (d :=false) in H0.
|
|
||||||
assert (S k < length (tm_step n)). rewrite tm_size_power2. apply H.
|
|
||||||
apply nth_error_nth' with (d :=false) in H1.
|
|
||||||
intros J. rewrite H0 in J. rewrite H1 in J.
|
|
||||||
apply tm_step_next_range2' in H0. apply tm_step_next_range2' in H1.
|
|
||||||
induction m.
|
|
||||||
+ rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
|
||||||
rewrite H0. rewrite H1. inversion J. rewrite H3. reflexivity.
|
|
||||||
+
|
|
||||||
|
|
||||||
assert (U: S k < 2^(S n+ m)).
|
|
||||||
assert (N: k < 2^n). apply I.
|
|
||||||
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 (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
|
|
||||||
apply nth_error_nth'. rewrite tm_size_power2. apply I.
|
|
||||||
assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
|
|
||||||
apply nth_error_nth'. rewrite tm_size_power2. apply H.
|
|
||||||
rewrite <- H2 in J. rewrite <- H3 in J.
|
|
||||||
|
|
||||||
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 + m)) k).
|
||||||
generalize K. generalize I. apply tm_step_stable.
|
generalize H1. generalize I. 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) (S k) = nth_error (tm_step (S n + m)) (S k)).
|
||||||
generalize U. generalize H. apply tm_step_stable.
|
generalize H0. generalize H. apply tm_step_stable.
|
||||||
|
rewrite <- H2 in L. rewrite <- H3 in L. apply L.
|
||||||
|
|
||||||
rewrite H4 in J. rewrite H5 in J.
|
apply H0.
|
||||||
|
Qed.
|
||||||
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 (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'.
|
|
||||||
rewrite H6 in J. rewrite H7 in J.
|
|
||||||
rewrite Nat.add_succ_comm in J. inversion J.
|
|
||||||
|
|
||||||
|
|
||||||
assert ( S k + 2^(n + S m) < 2^(S n + S m)
|
|
||||||
S k < 2^n ->
|
|
||||||
eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
|
|
||||||
= eqb
|
|
||||||
|
|
||||||
partir de H9 et appliquer :
|
|
||||||
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).
|
|
||||||
|
|
||||||
|
|
||||||
assert (nth_error (tm_step (S n + m)) (k + 2 ^ (n + m))
|
|
||||||
= nth_error (tm_step (S n + m)) (k + 2 ^ (n + m))
|
|
||||||
|
|
||||||
|
|
||||||
Theorem tm_step_stable : forall (n m k : nat),
|
|
||||||
k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
|
|
||||||
|
|
||||||
|
|
||||||
assert (U: S k < 2^(S n+ m)).
|
|
||||||
assert (N: k < 2^n). apply I.
|
|
||||||
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 (k < length (tm_step (S n + m))).
|
|
||||||
rewrite tm_size_power2. apply K.
|
|
||||||
apply nth_error_nth' with (d :=false) in H2.
|
|
||||||
assert (S k < length (tm_step (S n + m))).
|
|
||||||
rewrite tm_size_power2. apply U.
|
|
||||||
apply nth_error_nth' with (d :=false) in H3.
|
|
||||||
apply tm_step_next_range2' in H2. apply tm_step_next_range2' in H3.
|
|
||||||
|
|
||||||
rewrite Nat.add_succ_comm in H2. rewrite <- Nat.add_succ_l in H2.
|
|
||||||
rewrite Nat.add_succ_comm in H3. rewrite <- Nat.add_succ_l in H3.
|
|
||||||
|
|
||||||
rewrite H2. rewrite H3.
|
|
||||||
|
|
||||||
assert (nth_error (tm_step (n + S m)) k
|
|
||||||
= Some (nth k (tm_step (n + S m)) false)).
|
|
||||||
rewrite <- Nat.add_succ_comm. generalize K. rewrite <- tm_size_power2.
|
|
||||||
apply nth_error_nth'.
|
|
||||||
assert (nth_error (tm_step (n + S m)) (S k)
|
|
||||||
= Some (nth (S k) (tm_step (n + S m)) false)).
|
|
||||||
rewrite <- Nat.add_succ_comm. generalize U. rewrite <- tm_size_power2.
|
|
||||||
apply nth_error_nth'.
|
|
||||||
|
|
||||||
|
|
||||||
Some (negb (nth (S k) (tm_step (n + S m)) false))
|
|
||||||
|
|
||||||
Theorem tm_step_stable : forall (n m k : nat),
|
|
||||||
k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
|
|
||||||
|
|
||||||
nth_error_nth':
|
|
||||||
forall [A : Type] (l : list A) [n : nat] (d : A),
|
|
||||||
n < length l -> nth_error l n = Some (nth n l d)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
assert (V: S k < 2^(n+m)).
|
|
||||||
assert (N: k < 2^n). apply I.
|
|
||||||
assert (L: 2^n <= 2^(n + m)).
|
|
||||||
assert (M: n <= n + m). apply Nat.le_add_r.
|
|
||||||
apply Nat.pow_le_mono_r. easy. apply M.
|
|
||||||
generalize L. generalize H. apply Nat.lt_le_trans.
|
|
||||||
assert (L := V). apply Nat.lt_succ_l in L.
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
assert (k < length (tm_step (n + S m))).
|
|
||||||
rewrite tm_size_power2. apply L.
|
|
||||||
apply nth_error_nth' with (d :=false) in H2.
|
|
||||||
assert (S k < length (tm_step (n + S m))).
|
|
||||||
rewrite tm_size_power2. apply V.
|
|
||||||
apply nth_error_nth' with (d :=false) in H3.
|
|
||||||
|
|
||||||
|
|
||||||
rewrite <- Nat.add_succ_comm in V.
|
|
||||||
rewrite <- Nat.add_succ_comm in L.
|
|
||||||
|
|
||||||
|
|
||||||
assert (k < length (tm_step (S n + S m))).
|
|
||||||
rewrite tm_size_power2. apply K.
|
|
||||||
apply nth_error_nth' with (d :=false) in H2.
|
|
||||||
assert (S k < length (tm_step (S n + S m))).
|
|
||||||
rewrite tm_size_power2. apply U.
|
|
||||||
apply nth_error_nth' with (d :=false) in H3.
|
|
||||||
|
|
||||||
rewrite H2 in H3.
|
|
||||||
|
|
||||||
intros J. rewrite H0 in J. rewrite H1 in J. inversion J.
|
|
||||||
induction m. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
|
|
||||||
rewrite Bool.eqb_true_iff
|
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
Lemma tm_step_next_range2_neighbor : forall (n k : nat),
|
||||||
|
Loading…
Reference in New Issue
Block a user