baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-12-10 14:47:50 +01:00
parent 3f9b64f4ab
commit d938efe215
1 changed files with 1 additions and 452 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

453
thue-morse.v
View File

@ -1172,6 +1172,7 @@ Proof.
apply Nat.lt_le_incl. assumption.
Qed.
(* TODO: truc suivant inutile ? *)
Lemma tm_step_repeating_patterns :
forall (n m i j : nat),
i < m -> j < m
@ -1404,458 +1405,6 @@ Qed.
Lemma tm_step_add_small_power2 :
forall (n m j : nat),
j < m
-> forall k, k < 2^n -> nth_error (tm_step m) 0
= nth_error (tm_step m) (2^j)
<-> nth_error (tm_step (m+n)) (k * 2^m )
= nth_error (tm_step (m+n)) (k * 2^m + (2^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. apply G.
generalize H. generalize H0. apply Nat.le_lt_trans.
assert (N1: m < n). apply Nat.pow_lt_mono_r_iff in N0. apply N0.
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 (N3: 0 < n). destruct k. apply Nat.lt_irrefl in G. contradiction G.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
assert (2^m <= 2^m + k*2^m). apply Nat.le_add_r.
generalize H1. generalize H0. apply Nat.le_trans.
assert (2^0 < 2^n). generalize H. generalize H0.
apply Nat.le_lt_trans.
rewrite <- Nat.pow_lt_mono_r_iff in H1.
apply H1. apply Nat.lt_1_2.
assert (N4: 0 < m-j). rewrite Nat.add_lt_mono_r with (p := j). simpl.
replace (m-j+j) with (m). apply I. 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.
assert (O: k * 2^m + 2^j < 2^n).
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. apply H.
apply Nat.lt_le_incl. apply N5.
apply Nat.lt_le_incl. apply I.
- 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. apply N5.
apply Nat.lt_le_incl. apply I.
- assert ((S k)*2^m + 2^j < 2^(S n)). rewrite Nat.add_comm.
apply Nat.add_lt_mono with (p := 2^m) (q := 2^n) in O.
rewrite <- Nat.add_assoc in O. rewrite Nat.add_shuffle3 in O.
replace (2^m) with (1 * 2^m) in O at 2. rewrite <- Nat.mul_add_distr_r in O.
rewrite Nat.add_1_r in O. rewrite Nat.pow_succ_r'.
replace (2^n) with (1*2^n) in O. rewrite <- Nat.mul_add_distr_r in O.
rewrite Nat.add_1_r in O. apply O.
rewrite Nat.mul_1_l. reflexivity. rewrite Nat.mul_1_l. reflexivity.
apply N0.
TODO
Lemma tm_step_add_small_power :
forall (n m k j : nat),
1 < k -> k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros J H I.
assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (m-j+j) with (m). apply I. symmetry. apply Nat.sub_add.
generalize I. apply Nat.lt_le_incl.
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
- rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
+
(* m < n *)
assert (N: m < n). apply Nat.lt_le_incl in H0.
apply Nat.log2_le_mono in H0.
rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
generalize H0. assert (m < m + Nat.log2 k).
apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
generalize H1. apply Nat.lt_le_trans.
apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
apply Nat.le_0_l.
assert (0 < n-m).
rewrite Nat.add_lt_mono_l with (p := m).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (n-m+m) with (n). apply N. symmetry. apply Nat.sub_add.
generalize N. apply Nat.lt_le_incl.
assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Nat.add_0_r. rewrite Nat.add_comm.
replace (n-j+j) with (n). generalize N. generalize I. apply Nat.lt_trans.
symmetry. apply Nat.sub_add.
assert (j < n). generalize N. generalize I. apply Nat.lt_trans.
generalize H2. apply Nat.lt_le_incl.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
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.
assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
generalize I. generalize H3. apply Nat.le_lt_trans.
assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
assert (2^m <= 2^m + k*2^m). apply Nat.le_add_r.
generalize H5. generalize H4. apply Nat.le_trans.
assert (2^0 < 2^n). generalize H0. generalize H4.
apply Nat.le_lt_trans.
rewrite <- Nat.pow_lt_mono_r_iff in H5.
apply H5. apply Nat.lt_1_2.
assert (S (k*2^m) < 2^n). apply lt_even_even.
rewrite Nat.even_mul.
assert (Nat.even (2^m) = true). destruct m.
* apply Nat.lt_irrefl in H3. contradiction H3.
* rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
destruct n.
apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* apply H0.
* rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
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.
apply H0.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite <- Nat.pow_add_r.
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.sub_add.
reflexivity.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite tm_size_power2. apply H0.
+
rewrite nth_error_app2. rewrite nth_error_app2.
rewrite tm_size_power2.
rewrite nth_error_nth' with (d := false).
rewrite nth_error_nth' with (d := false).
(*
Lemma tm_step_add_small_power :
forall (n m k j : nat),
1 < k -> k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros J H I.
assert (M: 0 < m-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply I.
generalize I. apply Nat.lt_le_incl.
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
- rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
+
(* m < n *)
assert (N: m < n). apply Nat.lt_le_incl in H0.
apply Nat.log2_le_mono in H0.
rewrite Nat.log2_mul_pow2 in H0. rewrite Nat.log2_pow2 in H0.
generalize H0. assert (m < m + Nat.log2 k).
apply Nat.lt_add_pos_r. apply Nat.log2_pos. apply J.
generalize H1. apply Nat.lt_le_trans.
apply Nat.le_0_l. apply Nat.lt_succ_l in J. apply J.
apply Nat.le_0_l.
assert (0 < n-m).
rewrite Nat.add_lt_mono_l with (p := m).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r. apply N.
generalize N. apply Nat.lt_le_incl.
assert (0 < n-j). rewrite Nat.add_lt_mono_l with (p := j).
rewrite Arith_prebase.le_plus_minus_r_stt. rewrite Nat.add_0_r.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. generalize N. generalize I. apply Nat.lt_trans.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
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.
assert (0 < m). assert (0 <= j). apply Nat.le_0_l.
generalize I. generalize H3. apply Nat.le_lt_trans.
assert (0 < n). destruct k. apply Nat.nlt_succ_diag_l in J. contradiction J.
assert (2^0 <= (S k) * (2^m)). simpl. assert (1 <= 2^m).
replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r. easy.
apply Nat.le_0_l. reflexivity.
generalize H4. apply Arith_prebase.le_plus_trans_stt.
assert (2^0 < 2^n). generalize H0. generalize H4.
apply Nat.le_lt_trans. rewrite <- Nat.pow_lt_mono_r_iff in H5.
apply H5. apply Nat.lt_1_2.
assert (S (k*2^m) < 2^n). apply lt_even_even.
rewrite Nat.even_mul.
assert (Nat.even (2^m) = true). destruct m.
* apply Nat.lt_irrefl in H3. contradiction H3.
* rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
* destruct m. apply Nat.lt_irrefl in H3. contradiction H3.
destruct n.
apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
reflexivity. apply Nat.le_0_l.
* apply H0.
* rewrite Nat.add_1_r. apply lt_even_even. rewrite Nat.even_mul.
destruct (m-j). apply Nat.lt_irrefl in M. contradiction M.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
simpl. rewrite Bool.orb_true_r. reflexivity. apply Nat.le_0_l.
destruct (n-j). apply Nat.lt_irrefl in H2. contradiction H2.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. rewrite Nat.even_2.
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.
apply H0.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite <- Nat.pow_add_r.
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.sub_add.
reflexivity.
apply Nat.lt_le_incl.
generalize N. generalize I. apply Nat.lt_trans.
apply Nat.lt_le_incl. apply I.
* rewrite tm_size_power2. apply H0.
+
rewrite nth_error_app2. rewrite nth_error_app2.
rewrite tm_size_power2.
rewrite nth_error_map.
rewrite nth_error_map.
Lemma tm_step_add_small_power :
forall (n m k j : nat),
k * 2^m < 2^n -> j < m
-> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).
Proof.
intros n m k j. intros H I.
(*
assert(J: nth_error (tm_step (S j)) 0 <> nth_error (tm_step (S j)) (2 ^ j)).
rewrite tm_build. rewrite nth_error_app1. rewrite nth_error_app2.
rewrite tm_size_power2. rewrite Nat.sub_diag.
rewrite tm_step_head_1. simpl. easy.
rewrite tm_size_power2. easy.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
replace (nth_error (tm_step (S j)) 0) with (nth_error (tm_step m) 0) in J.
replace (nth_error (tm_step (S j)) (2^j)) with (nth_error (tm_step m) (2^j)) in J.
*)
(* à raccourcir avec tm_step build ! *)
assert (J: nth_error (tm_step j) 0 <> nth_error (tm_step (S j)) (2^j)).
replace (2^j) with (0 + 2^j).
apply tm_step_next_range2 with (k := 0).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. reflexivity.
assert (K: nth_error (tm_step j) 0 = nth_error (tm_step m) 0).
apply tm_step_stable.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (L: nth_error (tm_step (S j)) (2^j) = nth_error (tm_step m) (2^j)).
apply tm_step_stable. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
apply Nat.lt_succ_diag_r.
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply I.
rewrite K in J. rewrite L in J. clear K. clear L.
(* fin du à raccourcir *)
induction n.
- simpl. destruct k.
+ (* hypothèse vraie : k = 0 *)
simpl. assert (0 < 2^j).
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (nth_error [false] (2^j) = None).
apply nth_error_None. simpl. rewrite Nat.le_succ_l. apply H0.
rewrite H1. easy.
+ (* hypothèse fausse : contradiction en H *)
assert ((S k) * (2^m) <> 0).
rewrite <- Nat.neq_mul_0.
split. easy. apply Nat.pow_nonzero. easy.
rewrite Nat.pow_0_r in H. apply Nat.lt_1_r in H.
rewrite H in H0. contradiction H0. reflexivity.
-
rewrite tm_build.
assert (S: k * 2^m < 2^n \/ 2^n <= k * 2^m). apply Nat.lt_ge_cases.
destruct S.
rewrite nth_error_app1. rewrite nth_error_app1.
apply IHn. apply H0. rewrite tm_size_power2.
rewrite <- tm_size_power2 in H0.
rewrite <- nth_error_None in H0.
(*
induction k. rewrite Nat.mul_0_l. rewrite Nat.add_0_l.
assert(K: nth_error (tm_step n) 0 = nth_error (tm_step m) 0).
replace (nth_error (tm_step n) 0) with (Some false).
rewrite tm_step_head_1. simpl. reflexivity.
rewrite tm_step_head_1. simpl. reflexivity.
assert(L: nth_error (tm_step n) (2^j) = nth_error (tm_step m) (2^j)).
apply tm_step_stable.
*)
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).
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.
*)
Lemma greedy_power2 : forall (n m : nat),