Update
This commit is contained in:
Thomas Baruchel
parent
e5e7f7f6a0
commit
2857ebad62
230
thue-morse.v
230
thue-morse.v
|
|
@ -1077,47 +1077,6 @@ Proof.
|
|||
apply H1. apply H2.
|
||||
Qed.
|
||||
|
||||
|
||||
(*
|
||||
|
||||
Lemma tm_step_enlarge_window : forall (n m k i j k': nat),
|
||||
k * 2^m < 2^n ->
|
||||
k' * 2^m < 2^(S n) -> (
|
||||
j < m -> i < 2^j ->
|
||||
nth_error (tm_step n) (k*2^m + i) = nth_error (tm_step n) (k*2^m + i + 2^j)
|
||||
<->
|
||||
nth_error (tm_step (S n)) (k'*2^m + i) = nth_error (tm_step (S n)) (k'*2^m + i + 2^j)).
|
||||
Proof.
|
||||
intros n m k i j k'. intros I J K L.
|
||||
split.
|
||||
- intros M. rewrite tm_build.
|
||||
assert (S: k' * 2^m < 2^n \/ 2^n <= k' * 2^m). apply Nat.lt_ge_cases.
|
||||
rewrite nth_error_app1. rewrite nth_error_app1. apply M.
|
||||
|
||||
|
||||
|
||||
distinguer selon k4*2^m < 2^n ou non
|
||||
|
||||
|
||||
*)
|
||||
|
||||
|
||||
|
||||
Lemma lt_even_even : forall (a b : nat),
|
||||
even a = true -> even b = true -> a < b -> S a < b.
|
||||
Proof.
|
||||
intros a b. intros H I J.
|
||||
rewrite <- Nat.le_succ_l in J. rewrite Nat.lt_eq_cases in J.
|
||||
destruct J.
|
||||
- apply H0.
|
||||
- rewrite <- H0 in I. rewrite Nat.even_succ in I.
|
||||
rewrite <- I in H. rewrite <- Nat.negb_even in H.
|
||||
destruct (even a).
|
||||
+ simpl in H. apply Bool.diff_true_false in H. contradiction H.
|
||||
+ simpl in H. symmetry in H. apply Bool.diff_true_false in H. contradiction H.
|
||||
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.
|
||||
|
|
@ -1152,77 +1111,13 @@ Proof.
|
|||
rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
(* TODO: supprimer lt_even_even après avoir réussi ce truc ??? *)
|
||||
|
||||
|
||||
|
||||
Lemma lt_split_bits : forall n m k j,
|
||||
0 < k -> j < m -> k * 2^m < 2^n -> k * 2^m +2^j < 2^n.
|
||||
Proof.
|
||||
intros n m k j. intros H I J.
|
||||
|
||||
assert (N0: 2^m < 2^n). assert (2^m <= k * 2^m).
|
||||
replace (k * 2^m) with (1*2^m + (k-1)*2^m).
|
||||
simpl. rewrite Nat.add_0_r. apply Nat.le_add_r.
|
||||
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_l.
|
||||
rewrite <- Nat.sub_succ_l. rewrite <- Nat.add_1_r. rewrite Nat.add_sub.
|
||||
reflexivity. rewrite Nat.le_succ_l. assumption.
|
||||
generalize J. generalize H0. apply Nat.le_lt_trans.
|
||||
|
||||
assert (N1: m < n). apply Nat.pow_lt_mono_r_iff in N0. assumption.
|
||||
apply Nat.lt_1_2.
|
||||
|
||||
assert (N2: 0 < m). assert (0 <= j). apply Nat.le_0_l.
|
||||
generalize I. generalize H0. apply Nat.le_lt_trans.
|
||||
|
||||
assert (N4: 0 < m-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
|
||||
replace (m-j+j) with (m). assumption. symmetry. apply Nat.sub_add.
|
||||
generalize I. apply Nat.lt_le_incl.
|
||||
|
||||
assert (N5: j < n). generalize N1. generalize I. apply Nat.lt_trans.
|
||||
|
||||
assert (N6: 0 < n-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
|
||||
replace (n-j+j) with (n). apply N5. symmetry. apply Nat.sub_add.
|
||||
generalize N5. apply Nat.lt_le_incl.
|
||||
replace (k*2^m + 2^j < 2^n) with ((k*2^(m-j)+1)*(2^j) < 2^(n-j)*2^j).
|
||||
apply Nat.mul_lt_mono_pos_r.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
rewrite Nat.add_1_r. apply lt_even_even.
|
||||
- destruct (m-j).
|
||||
+ apply Nat.lt_irrefl in N4. contradiction N4.
|
||||
+ rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_mul.
|
||||
rewrite Nat.even_2. rewrite orb_true_r. reflexivity. apply Nat.le_0_l.
|
||||
- destruct (n-j).
|
||||
+ apply Nat.lt_irrefl in N6. contradiction N6.
|
||||
+ rewrite Nat.pow_succ_r. rewrite Nat.even_mul.
|
||||
rewrite Nat.even_2. rewrite orb_true_l. reflexivity. apply Nat.le_0_l.
|
||||
- apply Nat.mul_lt_mono_pos_r with (p := 2^j).
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
rewrite <- Nat.pow_add_r.
|
||||
rewrite <- Nat.mul_assoc. rewrite <- Nat.pow_add_r.
|
||||
rewrite Nat.sub_add. rewrite Nat.sub_add. assumption.
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
- rewrite Nat.mul_add_distr_r.
|
||||
rewrite <- Nat.mul_assoc.
|
||||
rewrite <- Nat.pow_add_r. rewrite Nat.mul_1_l. rewrite Nat.sub_add.
|
||||
rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. reflexivity.
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
apply Nat.lt_le_incl. assumption.
|
||||
Qed.
|
||||
|
||||
(* TODO: truc suivant inutile ? *)
|
||||
(* TODO: réécrire en plus puissant avec i et j < 2^m et on ajoute
|
||||
désormais direcctement i et j au lieu d'ajouter 2^i et 2^j *)
|
||||
Lemma tm_step_repeating_patterns :
|
||||
forall (n m i j : nat),
|
||||
i < m -> j < m
|
||||
-> forall k, k < 2^n -> nth_error (tm_step m) (2^i)
|
||||
= nth_error (tm_step m) (2^j)
|
||||
<-> nth_error (tm_step (m+n)) (k * 2^m + (2^i))
|
||||
= nth_error (tm_step (m+n)) (k * 2^m + (2^j)).
|
||||
i < 2^m -> j < 2^m
|
||||
-> forall k, k < 2^n -> nth_error (tm_step m) i
|
||||
= nth_error (tm_step m) j
|
||||
<-> nth_error (tm_step (m+n)) (k * 2^m + i)
|
||||
= nth_error (tm_step (m+n)) (k * 2^m + j).
|
||||
Proof.
|
||||
intros n m i j. intros H I.
|
||||
induction n.
|
||||
|
|
@ -1243,19 +1138,21 @@ Proof.
|
|||
generalize H1. apply IHn.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
assert (k * 2^m + 2^j < 2^(m+n)).
|
||||
destruct k. simpl. apply Nat.log2_lt_cancel.
|
||||
rewrite Nat.log2_pow2. rewrite Nat.log2_pow2.
|
||||
apply Nat.lt_lt_add_r. assumption. apply Nat.le_0_l. apply Nat.le_0_l.
|
||||
generalize H2. apply lt_split_bits.
|
||||
apply Nat.lt_0_succ. assumption. assumption.
|
||||
assert (k * 2^m + j < 2^(m+n)).
|
||||
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
||||
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
||||
generalize H3. generalize I. apply Nat.lt_le_trans.
|
||||
apply lt_split_bits. apply Nat.lt_0_succ.
|
||||
assumption. assumption. assumption.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
destruct k. simpl. apply Nat.log2_lt_cancel.
|
||||
rewrite Nat.log2_pow2. rewrite Nat.log2_pow2.
|
||||
apply Nat.lt_lt_add_r. assumption. apply Nat.le_0_l. apply Nat.le_0_l.
|
||||
generalize H2. apply lt_split_bits.
|
||||
apply Nat.lt_0_succ. assumption.
|
||||
assert (k * 2^m + i < 2^(m+n)).
|
||||
destruct k. simpl. assert (2^m <= 2^(m+n)).
|
||||
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
|
||||
generalize H3. generalize H. apply Nat.lt_le_trans.
|
||||
apply lt_split_bits. apply Nat.lt_0_succ.
|
||||
assumption. assumption. assumption.
|
||||
|
||||
+ assert (J: 2 ^ (m + n) <= k * 2 ^ m).
|
||||
rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
|
||||
apply Nat.mul_le_mono_r. assumption.
|
||||
|
|
@ -1272,8 +1169,8 @@ Proof.
|
|||
destruct b. split. intro. inversion H2. intro. inversion H2.
|
||||
split. intro. reflexivity. intro. reflexivity.
|
||||
|
||||
replace (k * 2 ^ m + 2^i - 2^(m + n)) with ((k-2^n)*2^m + 2^i).
|
||||
replace (k * 2 ^ m + 2^j - 2^(m + n)) with ((k-2^n)*2^m + 2^j).
|
||||
replace (k * 2 ^ m + i - 2^(m + n)) with ((k-2^n)*2^m + i).
|
||||
replace (k * 2 ^ m + j - 2^(m + n)) with ((k-2^n)*2^m + j).
|
||||
rewrite nth_error_map. rewrite nth_error_map.
|
||||
|
||||
rewrite H2. apply IHn.
|
||||
|
|
@ -1292,11 +1189,11 @@ Proof.
|
|||
rewrite Nat.add_comm. reflexivity. assumption.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
assert (k*2^m <= k*2^m + 2^j). apply Nat.le_add_r.
|
||||
assert (k*2^m <= k*2^m + j). apply Nat.le_add_r.
|
||||
generalize H2. generalize J. apply Nat.le_trans.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
assert (k*2^m <= k*2^m + 2^i). apply Nat.le_add_r.
|
||||
assert (k*2^m <= k*2^m + i). apply Nat.le_add_r.
|
||||
generalize H2. generalize J. apply Nat.le_trans.
|
||||
Qed.
|
||||
|
||||
|
|
@ -1308,74 +1205,12 @@ Lemma tm_step_add_small_power2 :
|
|||
<-> nth_error (tm_step (m+n)) (k * 2^m )
|
||||
= nth_error (tm_step (m+n)) (k * 2^m + (2^j)).
|
||||
Proof.
|
||||
intros n m j. intros H.
|
||||
induction n.
|
||||
- rewrite Nat.add_0_r. intro k. intro. simpl in H0.
|
||||
assert (k = 0). generalize H0. apply Nat.lt_1_r.
|
||||
rewrite H1. easy.
|
||||
- rewrite Nat.add_succ_r. intro k. intro.
|
||||
rewrite tm_build.
|
||||
assert (S: k < 2^n \/ 2^n <= k). apply Nat.lt_ge_cases.
|
||||
destruct S.
|
||||
|
||||
assert (k*2^m < 2^(m+n)).
|
||||
destruct k.
|
||||
+ simpl. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
+ rewrite Nat.mul_lt_mono_pos_r with (p := 2^m) in H1.
|
||||
rewrite <- Nat.pow_add_r in H1. rewrite Nat.add_comm.
|
||||
assumption. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
+ rewrite nth_error_app1. rewrite nth_error_app1.
|
||||
generalize H1. apply IHn.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
assert (k * 2^m + 2^j < 2^(m+n)).
|
||||
destruct k. simpl. apply Nat.log2_lt_cancel.
|
||||
rewrite Nat.log2_pow2. rewrite Nat.log2_pow2.
|
||||
apply Nat.lt_lt_add_r. assumption. apply Nat.le_0_l. apply Nat.le_0_l.
|
||||
generalize H2. apply lt_split_bits.
|
||||
apply Nat.lt_0_succ. assumption. assumption.
|
||||
|
||||
rewrite tm_size_power2. assumption.
|
||||
+ assert (J: 2 ^ (m + n) <= k * 2 ^ m).
|
||||
rewrite Nat.pow_add_r. rewrite Nat.mul_comm.
|
||||
apply Nat.mul_le_mono_r. assumption.
|
||||
|
||||
rewrite nth_error_app2. rewrite nth_error_app2. rewrite tm_size_power2.
|
||||
|
||||
assert (forall a b, option_map negb a = option_map negb b <-> a = b).
|
||||
intros a b. destruct a. destruct b. destruct b0. destruct b.
|
||||
simpl. split. intro. reflexivity. intro. reflexivity.
|
||||
simpl. split. intro. inversion H2. intro. inversion H2.
|
||||
destruct b. simpl. split. intro. inversion H2. intro. inversion H2.
|
||||
simpl. split. intro. reflexivity. intro. reflexivity.
|
||||
split. intro. inversion H2. intro. inversion H2.
|
||||
destruct b. split. intro. inversion H2. intro. inversion H2.
|
||||
split. intro. reflexivity. intro. reflexivity.
|
||||
|
||||
replace (k * 2 ^ m - 2^(m + n)) with ((k-2^n)*2^m).
|
||||
replace (k * 2 ^ m + 2^j - 2^(m + n)) with ((k-2^n)*2^m + 2^j).
|
||||
rewrite nth_error_map. rewrite nth_error_map.
|
||||
|
||||
rewrite H2. apply IHn.
|
||||
rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
|
||||
rewrite Nat.pow_succ_r in H0. replace (2) with (1+1) in H0.
|
||||
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
|
||||
rewrite Nat.add_0_r in H0. assumption. reflexivity.
|
||||
apply Nat.le_0_l. assumption.
|
||||
|
||||
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
|
||||
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
|
||||
rewrite Nat.add_comm. reflexivity. assumption.
|
||||
|
||||
rewrite Nat.mul_sub_distr_r. rewrite <- Nat.pow_add_r.
|
||||
replace (n+m) with (m+n). reflexivity.
|
||||
rewrite Nat.add_comm. reflexivity.
|
||||
|
||||
rewrite tm_size_power2.
|
||||
assert (k*2^m <= k*2^m + 2^j). apply Nat.le_add_r.
|
||||
generalize H2. generalize J. apply Nat.le_trans.
|
||||
|
||||
rewrite tm_size_power2. assumption.
|
||||
intros n m j. intros H. intro k.
|
||||
replace (k*2^m) with (k*2^m+0) at 1.
|
||||
apply tm_step_repeating_patterns.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
|
||||
rewrite Nat.add_0_r. reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem tm_step_flip_low_bit :
|
||||
|
|
@ -1416,7 +1251,7 @@ Proof.
|
|||
apply H1 in H2. rewrite H2 at 1. easy. easy.
|
||||
rewrite nth_error_nth' with (d := false). easy.
|
||||
rewrite tm_size_power2. apply lt_split_bits.
|
||||
assumption. assumption. assumption.
|
||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
||||
replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
|
||||
rewrite tm_step_single_bit_index. reflexivity.
|
||||
apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
|
||||
|
|
@ -1427,10 +1262,11 @@ Proof.
|
|||
assumption.
|
||||
rewrite tm_step_head_1. simpl. reflexivity.
|
||||
|
||||
apply tm_step_stable.
|
||||
generalize I. generalize H. generalize G. apply lt_split_bits.
|
||||
apply tm_step_stable. apply lt_split_bits.
|
||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
||||
assert (k*2^m + 2^j < 2^n).
|
||||
generalize I. generalize H. generalize G. apply lt_split_bits.
|
||||
apply lt_split_bits.
|
||||
assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
|
||||
assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
|
||||
generalize H2. generalize H1. apply Nat.lt_le_trans.
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user