diff --git a/thue-morse.v b/thue-morse.v index 6060bb1..aabd0bc 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -1113,169 +1113,27 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat), - induction m. + 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. - + + + 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. - -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. + rewrite <- tm_step_next_range2_neighbor' in L. 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)). - 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. - - 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 + apply H0. +Qed. Lemma tm_step_next_range2_neighbor : forall (n k : nat),