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 2023-01-04 15:26:06 +01:00
parent 443008fbb5
commit dcfa1b363c
1 changed files with 111 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

113
thue-morse.v
View File

@ -753,6 +753,116 @@ Proof.
Qed.
Lemma tm_step_pred : forall (n k m : nat),
S (2*k) * 2^m < 2^n ->
nth_error (tm_step n) (S (2*k) * 2^m)
= nth_error (tm_step n) (pred (S (2*k) * 2^m))
<-> odd m = true.
Proof.
intros n k m.
generalize n. induction m. rewrite Nat.pow_0_r. rewrite Nat.mul_1_r.
destruct n0. rewrite Nat.pow_0_r. rewrite Nat.lt_1_r.
intro H. apply Nat.neq_succ_0 in H. contradiction H.
rewrite Nat.odd_0. rewrite Nat.pred_succ.
rewrite <- tm_step_double_index. intro H. split; intro I.
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
inversion I.
intro n0. intro I.
destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
rewrite Nat.mul_eq_0 in I. destruct I.
apply Nat.neq_succ_0 in H. contradiction H.
apply Nat.pow_nonzero in H. contradiction H. easy.
rewrite Nat.pow_succ_r'. rewrite Nat.mul_assoc.
replace (S (2*k) * 2) with (2* (S (2*k))).
rewrite <- Nat.mul_assoc. rewrite <- tm_step_double_index.
rewrite Nat.pow_succ_r' in I.
rewrite Nat.pow_succ_r' in I.
rewrite Nat.mul_assoc in I.
replace (S (2*k) * 2) with (2* (S (2*k))) in I.
rewrite <- Nat.mul_assoc in I.
rewrite <- Nat.mul_lt_mono_pos_l in I.
assert (J := I). apply IHm in J.
assert (M: 0 < 2^m). rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
assert (L: pred( S (2 * k) * 2 ^ m) < S (2 * k) * 2 ^ m).
apply Nat.lt_pred_l. apply Nat.neq_mul_0.
split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0. assumption.
assert (N: pred (2 * (S (2 * k) * 2 ^ m)) < length (tm_step (S n0))).
rewrite tm_size_power2.
rewrite <- Nat.le_succ_l. rewrite Nat.succ_pred_pos. rewrite Nat.pow_succ_r.
apply Nat.mul_le_mono_l. generalize I. apply Nat.lt_le_incl.
apply Nat.le_0_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption.
assert(T: pred (S (2 * k) * 2 ^ m) < 2 ^ n0).
generalize I. generalize L. apply Nat.lt_trans.
assert (nth_error (tm_step n0) (pred (S (2 * k) * 2 ^ m))
<> nth_error (tm_step (S n0)) (S (2 * (pred(S (2 * k) * 2 ^ m))))).
apply tm_step_succ_double_index. assumption.
replace (S (2 * (pred(S (2 * k) * 2 ^ m)))) with (pred(2 * (S (2*k) * 2^m))) in H.
rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
split. intro K. rewrite <- K in H.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (pred(S (2 * k) * 2 ^ m))).
destruct J. replace (Some b) with (Some b0) in H. contradiction H.
reflexivity. symmetry. apply H1. reflexivity.
destruct J. replace (Some b) with (None : option bool) in H.
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
destruct J. replace (None : option bool) with (Some b) in H.
contradiction H. reflexivity. symmetry. apply H1. reflexivity.
contradiction H. reflexivity.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (pred(S (2 * k) * 2 ^ m)));
intro K; simpl in K; inversion K.
rewrite nth_error_nth' with (d := false) in J.
rewrite nth_error_nth' with (d := false) in J.
rewrite nth_error_nth' with (d := false) in H.
rewrite nth_error_nth' with (d := false) in H.
rewrite nth_error_nth' with (d := false).
rewrite nth_error_nth' with (d := false).
destruct (nth (S (2 * k) * 2 ^ m) (tm_step n0) false);
destruct (nth (pred (S (2 * k) * 2 ^ m)) (tm_step n0) false);
destruct (nth (pred (2 * (S (2 * k) * 2 ^ m))) (tm_step (S n0)) false).
simpl; split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity.
simpl; split; reflexivity. contradiction H. reflexivity.
contradiction H. reflexivity.
simpl; split; reflexivity.
destruct J. rewrite H0 in H. contradiction H. reflexivity.
reflexivity.
simpl; split; reflexivity.
assumption. rewrite tm_size_power2. assumption. assumption.
rewrite tm_size_power2. assumption.
rewrite tm_size_power2. assumption.
rewrite tm_size_power2. assumption.
rewrite <- Nat.add_1_r at 4.
rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l.
rewrite <- Nat.add_1_r at 1.
rewrite Nat.mul_add_distr_r. rewrite Nat.mul_1_l.
rewrite <- Nat.add_succ_l. rewrite Nat.succ_pred_pos. rewrite <- Nat.add_pred_r.
reflexivity. apply Nat.neq_mul_0. split. apply Nat.neq_succ_0. rewrite Nat.neq_0_lt_0.
assumption. apply Nat.mul_pos_pos. apply Nat.lt_0_succ. assumption.
apply Nat.lt_0_2.
apply Nat.mul_comm. apply Nat.mul_comm.
Qed.
(* TODO: remove
Lemma tm_step_pred : forall (n k m : nat),
S (2*k) * 2^m < 2^n ->
nth_error (tm_step n) (S (2*k) * 2^m)
@ -865,7 +975,7 @@ Proof.
apply Nat.mul_comm. apply Nat.mul_comm.
Qed.
*)
(*
From a(0) to a(2n+1), there are n+1 terms equal to 0 and n+1 terms equal to 1 (see Hassan Tarfaoui link, Concours Général 1990). - Bernard Schott, Jan 21 2022
@ -1340,4 +1450,3 @@ Qed.