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 16:12:03 +01:00
parent dce599bcb3
commit 44ae80ab27
1 changed files with 127 additions and 212 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

339
thue-morse.v → thue_morse.v
View File

@ -1,7 +1,8 @@
(*
(**
Some proofs related to the Thue-Morse sequence.
See https://oeis.org/A010060
https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
See:
- https://oeis.org/A010060
- https://en.wikipedia.org/wiki/Thue%E2%80%93Morse_sequence
*)
Require Import Coq.Lists.List.
@ -12,9 +13,9 @@ Require Import Bool.
Import ListNotations.
(*
(**
This whole notebook contains proofs related to the following two functions.
Nothing else is defined afterwards.
Nothing else is defined afterwards in the current notebook.
*)
Fixpoint tm_morphism (l:list bool) : list bool :=
@ -30,7 +31,7 @@ Fixpoint tm_step (n: nat) : list bool :=
end.
(*
(**
More or less "general" lemmas, which are not directly related to
the previous functions are proved below.
*)
@ -96,7 +97,7 @@ Proof.
Qed.
(*
(**
Some lemmas related to the first function (tm_morphism) are proved here.
They have a wider scope than the following ones since they don't focus on
the Thue-Morse sequence by itself.
@ -281,7 +282,7 @@ Proof.
Qed.
(*
(**
Lemmas and theorems below are related to the second function defined initially.
They focus on the Thue-Morse sequence.
*)
@ -369,22 +370,25 @@ Proof.
Qed.
Lemma tm_step_repunit_index : forall (n : nat),
nth_error (tm_step n) (2^n - 1) = Some (odd n).
nth_error (tm_step n) (pred (2^n)) = Some (odd n).
Proof.
intro n.
assert (H: 2 ^ n - 1 < length (tm_step n)). rewrite tm_size_power2.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l. apply Nat.pow_nonzero. easy.
rewrite <- Nat.sub_1_r. rewrite <- tm_size_power2.
rewrite nth_error_nth' with (d := false).
replace (tm_step n) with (rev (rev (tm_step n))).
rewrite rev_nth. rewrite rev_length. rewrite tm_size_power2.
rewrite Nat.sub_1_r. rewrite Nat.succ_pred_pos. rewrite Nat.sub_diag.
rewrite tm_step_end_1. reflexivity.
rewrite <- rev_nth. rewrite tm_step_end_1. simpl.
reflexivity.
rewrite tm_size_power2.
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
rewrite rev_length. assumption. apply rev_involutive. assumption.
rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
Qed.
(**
The following lemmas and theorems focus on the stability of the sequence:
while lists in the sequence get longer and longer, the beginning of a
longer list contain the same elements as the previous shorter lists.
*)
Lemma tm_step_next_range :
forall (n k : nat) (b : bool),
nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
@ -432,6 +436,94 @@ Proof.
reflexivity.
Qed.
(**
The following lemma states that a block of terms in the Thue-Morse
sequence having a size being a power of 2 is repeated, either
as an identical version or with all values together flipped.
*)
Lemma tm_step_repeating_patterns :
forall (n m i j : nat),
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.
- rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro.
rewrite H0. simpl. 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.
+ assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))).
intro l. intro M. rewrite tm_size_power2.
destruct k. simpl. assert (2^m <= 2^(m+n)).
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
generalize H3. generalize M. apply Nat.lt_le_trans.
apply lt_split_bits. apply Nat.lt_0_succ. assumption.
assumption.
rewrite nth_error_app1. rewrite nth_error_app1.
generalize H1. apply IHn.
apply L. assumption. apply L. 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. split; intro; inversion H2.
split; intro; inversion H2. split; intro; reflexivity.
split; intro; inversion H2.
destruct b. split; intro; inversion H2. split; intro; reflexivity.
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.
rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
rewrite Nat.pow_succ_r in H0. rewrite <- Nat.add_1_r in H0 at 1.
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
rewrite Nat.add_0_r in H0. assumption.
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.
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
rewrite Nat.add_comm. reflexivity. assumption.
rewrite tm_size_power2.
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 + i). apply Nat.le_add_r.
generalize H2. generalize J. apply Nat.le_trans.
Qed.
(**
The following lemmas and theorems are related to flipping the
most significant bit in the numerical value of indices (of terms
in the lists).
*)
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).
@ -583,81 +675,12 @@ Proof.
apply H1. apply H2.
Qed.
Lemma tm_step_repeating_patterns :
forall (n m i j : nat),
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.
- rewrite Nat.add_0_r. intro k. simpl. rewrite Nat.lt_1_r. intro.
rewrite H0. simpl. 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.
(**
The following lemmas and theorems are related to flipping the
least significant bit in the numerical value of indices (of terms
in the lists).
*)
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.
+ assert (L: forall l, l < 2^m -> k*2^m + l < length (tm_step (m+n))).
intro l. intro M. rewrite tm_size_power2.
destruct k. simpl. assert (2^m <= 2^(m+n)).
apply Nat.pow_le_mono_r. easy. apply Nat.le_add_r.
generalize H3. generalize M. apply Nat.lt_le_trans.
apply lt_split_bits. apply Nat.lt_0_succ. assumption.
assumption.
rewrite nth_error_app1. rewrite nth_error_app1.
generalize H1. apply IHn.
apply L. assumption. apply L. 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. split; intro; inversion H2.
split; intro; inversion H2. split; intro; reflexivity.
split; intro; inversion H2.
destruct b. split; intro; inversion H2. split; intro; reflexivity.
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.
rewrite Nat.add_lt_mono_r with (p := 2^n). rewrite Nat.sub_add.
rewrite Nat.pow_succ_r in H0. rewrite <- Nat.add_1_r in H0 at 1.
rewrite Nat.mul_add_distr_r in H0. simpl in H0.
rewrite Nat.add_0_r in H0. assumption.
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.
rewrite Nat.add_sub_swap. replace (n+m) with (m+n). reflexivity.
rewrite Nat.add_comm. reflexivity. assumption.
rewrite tm_size_power2.
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 + i). apply Nat.le_add_r.
generalize H2. generalize J. apply Nat.le_trans.
Qed.
(* Note: a first version included the 0 < k hypothesis but in the very
unorthodox case where k=0 it happens to be true anyway, and the hypothesis
@ -739,6 +762,13 @@ Proof.
generalize P. generalize I. apply Nat.lt_le_trans.
Qed.
(**
The following lemmas and theorems are of general interest; they
come here because they use more specific previously defined
lemmas and theorems.
*)
Theorem tm_step_succ_double_index : forall (n k : nat),
k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
Proof.
@ -862,125 +892,13 @@ Proof.
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)
= nth_error (tm_step n) (S (2*k) * 2^m - 1)
<-> 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.sub_succ. rewrite Nat.sub_0_r.
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.
intro I. 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: S (2 * k) * 2 ^ m - 1 < S (2 * k) * 2 ^ m).
replace (S (2 * k) * 2 ^ m) with (S (S (2 * k) * 2 ^ m - 1)) at 2.
apply Nat.lt_succ_diag_r.
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_1_r. rewrite pred_Sn.
reflexivity. rewrite Nat.le_succ_l. apply Nat.mul_pos_pos.
apply Nat.lt_0_succ. assumption.
assert (N: 2 * (S (2 * k) * 2 ^ m) - 1 < length (tm_step (S n0))).
rewrite tm_size_power2.
rewrite <- Nat.le_succ_l. rewrite <- Nat.add_1_r.
rewrite Nat.sub_add. rewrite Nat.pow_succ_r'.
rewrite <- Nat.mul_le_mono_pos_l.
apply Nat.lt_le_incl. assumption. apply Nat.lt_0_2.
apply Nat.le_succ_l. apply Nat.mul_pos_pos. apply Nat.lt_0_2.
apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
assumption.
assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0).
generalize I. generalize L. apply Nat.lt_trans.
assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
<> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
apply tm_step_succ_double_index. assumption.
replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) 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) (S (2 * k) * 2 ^ m - 1)).
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) (S (2 * k) * 2 ^ m - 1));
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 (S (2 * k) * 2 ^ m - 1) (tm_step n0) false);
destruct (nth (2 * (S (2 * k) * 2 ^ m) - 1) (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.mul_sub_distr_l. rewrite Nat.mul_1_r.
rewrite <- Nat.sub_succ_l. rewrite Nat.sub_succ. reflexivity.
rewrite <- Nat.mul_1_r at 1.
apply Nat.mul_le_mono_pos_l. apply Nat.lt_0_2.
apply Nat.le_succ_l. 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.
*)
(*
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
TODO Search "count_occ"
*)
(**
The following lemmas and theorems are related to the sequence being
cubefree. Only the final theorem is of general interest; all other
lemmas are defined for the very specific purpose of being used in the
final proof.
*)
Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
tm_step n = hd ++ tl -> even (length hd) = true
-> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
@ -1447,6 +1365,3 @@ Proof.
Qed.