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-21 15:14:07 +01:00
parent c1dd9ca8fb
commit bab107dd9d
2 changed files with 370 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/thue_morse.v
View File

@ -113,6 +113,23 @@ Proof.
assumption.
Qed.
Lemma odd_mod4 : forall n : nat,
odd n = true -> n mod 4 = 1 \/ n mod 4 = 3.
Proof.
intro n. intro H.
assert (K: 1 = n mod 2).
apply Nat.mod_unique with (q := Nat.div2 n). apply Nat.lt_1_2.
replace (1) with (Nat.b2n (Nat.odd n)) at 2.
apply Nat.div2_odd. rewrite H. reflexivity.
assert (L: n mod (2*2) = n mod 2 + 2 * ((n / 2) mod 2)).
apply Nat.mod_mul_r; easy. rewrite <- K in L.
replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
rewrite L.
destruct (Nat.testbit (n / 2) 0) ; [right | left] ; reflexivity.
reflexivity.
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
@ -1122,21 +1139,8 @@ Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
-> length a = 4 -> odd (length hd) = true
-> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
Proof.
intros n hd a tl. intros H I J.
assert (K: 1 = (length hd) mod 2).
apply Nat.mod_unique with (q := Nat.div2 (length hd)). apply Nat.lt_1_2.
replace (1) with (Nat.b2n (Nat.odd (length hd))) at 2.
apply Nat.div2_odd. rewrite J. reflexivity.
assert (L: (length hd) mod (2*2)
= (length hd) mod 2 + 2 * (((length hd) / 2) mod 2)).
apply Nat.mod_mul_r; easy. rewrite <- K in L.
replace (2*2) with (4) in L. rewrite <- Nat.bit0_mod in L.
assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3). rewrite L.
destruct (Nat.testbit (length hd / 2) 0) ; [right | left] ; reflexivity.
intros n hd a tl. intros H I M.
apply odd_mod4 in M.
destruct M as [M | M].
- assert (exists (x : bool), firstn 2 a = [x;x]).
generalize M. generalize I. generalize H. apply tm_step_factor4_1mod4.
@ -1146,7 +1150,6 @@ Proof.
generalize M. generalize I. generalize H. apply tm_step_factor4_3mod4.
destruct H0. exists x. exists (firstn 2 a). exists nil.
rewrite app_nil_r. rewrite <- H0. symmetry. apply firstn_skipn.
- reflexivity.
Qed.
Lemma tm_step_consecutive_identical_length :

426
src/thue_morse3.v
View File

@ -1,6 +1,8 @@
(** * The Thue-Morse sequence (part 3)
TODO
tm_step_rev
*)
Require Import thue_morse.
@ -14,6 +16,22 @@ Require Import Bool.
Import ListNotations.
Theorem tm_step_rev : forall (n : nat),
tm_step n = rev (tm_step n) \/ tm_step n = map negb (rev (tm_step n)).
Proof.
assert (Z: forall l, map (fun x : bool => negb (negb x)) l = l).
intro l. induction l. reflexivity. simpl. rewrite negb_involutive.
rewrite IHl. reflexivity.
intro n. induction n. left. reflexivity.
rewrite tm_build. destruct IHn ; [right | left];
rewrite rev_app_distr; rewrite H at 1;
rewrite H at 2; rewrite <- map_rev.
rewrite map_app. rewrite map_map. rewrite Z. reflexivity.
rewrite map_map. rewrite Z. reflexivity.
Qed.
Lemma tm_step_palindromic_odd : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> a = rev a
@ -280,78 +298,6 @@ Proof.
Qed.
Lemma tm_step_palindromic_negb_center :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ map negb (rev a) ++ tl
-> 1 < length a
-> even (length (hd ++ a)) = true.
Proof.
intros n hd a tl. intros H I.
assert (J: a = firstn (length a - 2) a ++ skipn (length a - 2) a).
symmetry. apply firstn_skipn. rewrite J in H.
rewrite rev_app_distr in H. rewrite map_app in H.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite app_assoc in H.
replace ( skipn (length a - 2) a ++
map negb (rev (skipn (length a - 2) a)) ++
map negb (rev (firstn (length a - 2) a)) ++ tl )
with ( ( skipn (length a - 2) a ++
map negb (rev (skipn (length a - 2) a)) ) ++
map negb (rev (firstn (length a - 2) a)) ++ tl ) in H.
assert (length (skipn (length a - 2) a) = 2). rewrite skipn_length.
replace (length a) with (2 + (length a - 2)) at 1. rewrite Nat.add_sub.
reflexivity. rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
rewrite Nat.sub_diag. reflexivity. easy. rewrite Nat.le_succ_l.
assumption.
assert (length
(skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a))) = 4).
rewrite app_length. rewrite map_length. rewrite rev_length.
rewrite H0. reflexivity.
assert (K: {even (length (hd ++ firstn (length a - 2) a))=true}
+ {~ even (length (hd ++ firstn (length a - 2) a))=true}).
apply bool_dec. destruct K.
rewrite J. rewrite app_assoc. rewrite app_length. rewrite Nat.even_add.
rewrite e. rewrite H0. reflexivity. apply not_true_is_false in n0.
assert (exists (x : bool) (u v : list bool),
(skipn (length a - 2) a ++ map negb (rev (skipn (length a - 2) a)))
= u ++ [x;x] ++ v).
assert (odd (length (hd ++ firstn (length a - 2) a)) = true).
rewrite <- Nat.negb_even. rewrite n0. reflexivity. generalize H2.
generalize H1. generalize H. apply tm_step_factor4_odd_prefix.
destruct H2. destruct H2. destruct H2. rewrite H2 in H1.
destruct x0.
assert (skipn (length a - 2) a = [x;x]).
assert (length (skipn (length a - 2) a) = length ([x;x])). rewrite H0.
reflexivity. generalize H3. generalize H2. rewrite app_nil_l.
apply app_eq_length_head. rewrite H3 in H.
TODO contradiction en H
Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> length a = 4 -> odd (length hd) = true
-> exists (x : bool) (u v : list bool), a = u ++ [x;x] ++ v.
pose (hd' := hd ++ firstn (length a - 2) a).
pose (tl' := map negb (rev (firstn (length a - 2) a)) ++ tl).
pose (a' := skipn (length a - 2) a).
fold hd' in H. fold tl' in H. fold a' in H.
replace (a' ++ map negb (rev a') ++ tl')
with ((a' ++ map negb (rev a')) ++ tl') in H.
assert (length pat = 4).
(**
In this notebook I call "proper palindrome" in the Thue-Morse sequence,
any palindromic subsequence such that the middle (of the palindromic
@ -360,6 +306,329 @@ Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
termes on both sides.
*)
(* palidrome 2*4 : soit centré en 4n+2 soit pas plus de 2*4 *)
(* on prouve facilement que hd != nil *)
Lemma tm_step_palindromic_length_8 :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
-> length a = 4
-> length (hd ++ a) mod 4 = 2
\/ (length (hd ++ a) mod 4 = 0 /\ last hd false <> List.hd false tl).
Proof.
intros n hd a tl. intros H I.
(* proof that length hd++a is even *)
assert (P: even (length (hd ++ a)) = true).
assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0.
generalize H. apply tm_step_palindromic_even_center.
(* proof that length hd is even *)
assert (Q: even (length hd) = true). rewrite app_length in P.
rewrite Nat.even_add_even in P. assumption. rewrite I.
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
(* construction de a *)
destruct a. inversion I. destruct a. inversion I.
destruct a. inversion I. destruct a. inversion I.
destruct a. simpl in H.
(* proof that b1 <> b2 *)
assert ({b1=b2} + {~ b1=b2}). apply bool_dec. destruct H0.
replace (hd ++ b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
with ((hd ++ b :: b0 :: nil)
++ [b1] ++ [b2] ++ [b2] ++ b1 :: b0 :: b :: tl) in H.
rewrite e in H. apply tm_step_cubefree in H. contradiction H.
reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
(* proof that n > 2 *)
assert (2 < n).
assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
<= length hd
+ length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)).
apply Nat.add_le_mono. apply le_0_n. apply Nat.le_refl.
rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J.
rewrite tm_size_power2 in J.
destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1.
destruct n. inversion J. inversion H1.
apply Nat.nle_succ_0 in H3. contradiction H3.
destruct n. inversion J. inversion H1. inversion H3. inversion H5.
inversion H7. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ.
(* proof that hd <> nil *)
destruct hd.
assert (Z: 4 < 2^n). replace 4 with (2^2).
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
assert (Some b2 = nth_error (tm_step n) 3). rewrite H. reflexivity.
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H1.
simpl in H1.
assert (Some b2 = nth_error (tm_step n) 4). rewrite H. reflexivity.
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H2.
simpl in H2.
rewrite H1 in H2. inversion H2. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
assert (3 < 4).
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
generalize Z. generalize H2. apply Nat.lt_trans.
(* proof that tl <> nil *)
destruct tl.
assert (Z: 4 < 2^n). replace 4 with (2^2).
apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
assert (Y: tm_step n = rev (tm_step n)
\/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev.
destruct Y; rewrite H in H1 at 2; rewrite rev_app_distr in H1.
assert (Some b2 = nth_error (tm_step n) 3). rewrite H1. reflexivity.
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
simpl in H2.
assert (Some b2 = nth_error (tm_step n) 4). rewrite H1. reflexivity.
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
simpl in H3.
rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
assert (3 < 4).
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
generalize Z. generalize H3. apply Nat.lt_trans.
assert (Some (negb b2) = nth_error (tm_step n) 3). rewrite H1.
rewrite nth_error_map. reflexivity.
replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
simpl in H2.
assert (Some (negb b2) = nth_error (tm_step n) 4). rewrite H1.
rewrite nth_error_map. reflexivity.
replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
simpl in H3.
rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
assert (3 < 4).
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
generalize Z. generalize H3. apply Nat.lt_trans.
(* première hypothèse b0 = b1 mais alors on construit vers la
gauche jusqu'à (lest hd) et l'on a dans l'ordre jusqu'au centre :
b1 | (negb b1) b1 | b1 (negb b1 ||
et les quatre premiers termes vont impliquer que le centre soit en 4n+2 *)
assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
rewrite e in H.
(* on a alors b = negb b1 (car dans le même bloc pair on a 01 ou 10 *)
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
rewrite e0 in H.
replace
((b3 :: hd) ++ b1 :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl)
with
((b3 :: hd) ++ [b1] ++ [b1] ++ [b1]
++ b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) in H.
apply tm_step_cubefree in H. contradiction H. reflexivity.
apply Nat.lt_0_1. reflexivity.
(* à ce stade on a F T | T F || F T T F *)
(* si on a ensuite le bloc précédent identique aux deux premiers de a
(* TODO : terminer avec une inversion sur la longueur de a ;
le dernier but vient de la destructuration initiale de a *)
F T | T F | T F ][ F T | F T T F
4n
ou F T | T F ][ F T | T F
4n ou 4n
F T F T T F F T T F T F (centre 4n+2 ET 4n : contra)
T F F T T F F T T F T F (centre : 4n+2)
F T F T T F F T T F F T (centre : 4n)
T F F T T F F T T F F T (cubes)
--> T F F T | T F ][ F T | T F F T (impossible : cubes)
--> F T F T | T F ][ F T | T F T F
Bilan : seulement deux cas possible de palindrome 8
F T | T F | T F ][ F T | F T | T F
4n+2 4n+2 (trivial)
F T | F T | T F ][ F T | T F | T F
4n (par examen des cinq premiers termes à gauche)
Lemma tm_step_proper_palindromic_center :
forall (m n k i: nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
-> length a = 2 ^ S (Nat.double m)
-> length (hd ++ a) = S (Nat.double k) * 2 ^ i
-> last hd false <> List.hd false tl
-> i = 2 ^ S (Nat.double m).
Proof.
intro m. induction m.
- intros n k i hd a tl. intros H I J K.
destruct a. inversion I. destruct a. inversion I. destruct a.
(* JUNK
Lemma xxx : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ map negb (rev a) ++ tl
-> length a = 4
-> even (length hd) = true.
Proof.
intros n hd a tl. intros H I.
destruct a. inversion I. destruct a. inversion I.
destruct a. inversion I. destruct a. inversion I.
destruct a.
replace [b;b0;b1;b2] with ([b] ++ [b0] ++ [b1] ++ [b2]) in H at 1.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite <- app_assoc in H.
replace (map negb (rev [b; b0; b1; b2]))
with ([negb b2] ++ [negb b1] ++ [negb b0] ++ [negb b]) in H.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite <- app_assoc in H.
assert (0 < length [b]). apply Nat.lt_0_1.
assert (0 < length [b0]). apply Nat.lt_0_1.
assert (0 < length [b1]). apply Nat.lt_0_1.
assert (0 < length [b2]). apply Nat.lt_0_1.
assert (J: {even (length hd) = true}
+ {~ even (length hd) = true}). apply bool_dec.
destruct b; destruct b0; destruct b1; destruct b2.
- assert ([true]<>[true]). generalize H0.
generalize H. apply tm_step_cubefree.
contradiction H4. reflexivity.
- assert ([true]<>[true]). generalize H0.
generalize H. apply tm_step_cubefree.
contradiction H4. reflexivity.
- assert([true] ++ [false] <> [true] ++ [false]). rewrite app_assoc in H.
replace ( [true] ++ [false] ++ [true] ++ [negb true]
++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
with ( ([true] ++ [false]) ++ ([true] ++ [negb true])
++ ([negb false] ++ [negb true]) ++ [negb true] ++ tl) in H.
assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
generalize H4. generalize H. apply tm_step_cubefree.
reflexivity. contradiction H4. reflexivity.
- assert (even (length (hd ++ [true] ++ [true] ++ [false] ++ [false])) = true).
replace ( [true] ++ [true] ++ [false] ++ [false] ++ [negb false]
++ [negb false] ++ [negb true] ++ [negb true] ++ tl)
with ( ([true] ++ [true] ++ [false] ++ [false]) ++ ([negb false]
++ [negb false] ++ [negb true] ++ [negb true]) ++ tl) in H.
assert (0 < length ([true] ++ [true] ++ [false] ++ [false])).
apply Nat.lt_0_succ. generalize H4. generalize H. apply tm_step_square_pos.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
rewrite app_length in H4. simpl in H4.
rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
rewrite Nat.add_succ_r in H4. rewrite Nat.add_succ_r in H4.
rewrite Nat.add_0_r in H4.
rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
rewrite Nat.even_succ in H4. rewrite Nat.odd_succ in H4.
rewrite H4. reflexivity.
- destruct J. assumption.
rewrite not_true_iff_false in n0.
assert (M: (length hd) mod 4 = 1 \/ (length hd) mod 4 = 3).
apply odd_mod4. rewrite <- Nat.negb_even. rewrite n0. reflexivity.
destruct M.
+ replace ( [true] ++ [false] ++ [true] ++ [true]
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
with ( ([true] ++ [false] ++ [true] ++ [true])
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
in H.
assert (exists (x:bool), firstn 2 [true;false;true;true] = [x;x]).
generalize H4. generalize I. generalize H.
apply tm_step_factor4_1mod4.
destruct H5. inversion H5. inversion H8.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
+ replace ( hd ++ [true] ++ [false] ++ [true] ++ [true]
++ [negb true] ++ [negb true] ++ [negb false] ++ [negb true] ++ tl )
with ( (hd ++ [true] ++ [false] ++ [true] ++ [true])
++ ([negb true] ++ [negb true] ++ [negb false] ++ [negb true]) ++ tl )
in H.
assert (exists (x:bool), skipn 2 [false;false;true;false] = [x;x]).
assert (length (hd ++ [true]++[false]++[true]++[true]) mod 4 = 3).
rewrite app_length. rewrite Nat.add_mod. rewrite H4. reflexivity.
easy. generalize H5.
assert (length [false;false;true;false]=4). reflexivity.
generalize H6. generalize H. apply tm_step_factor4_3mod4.
destruct H5. inversion H5. inversion H8.
rewrite <- app_assoc. reflexivity.
- assert([true] ++ [false] <> [true] ++ [false]).
replace ( [true] ++ [false] ++ [true] ++ [false] ++ [negb false]
++ [negb true] ++ [negb false] ++ [negb true] ++ tl)
with ( ([true] ++ [false]) ++ ([true] ++ [false])
++ ([negb false] ++ [negb true])
++ [negb false] ++ [negb true] ++ tl) in H.
assert (0 < length ([true]++[false])). apply Nat.lt_0_2.
generalize H4. generalize H. apply tm_step_cubefree.
reflexivity. contradiction H4. reflexivity.
- destruct J. assumption. rewrite not_true_iff_false in n0.
*)
(* TODO: bloqué
Lemma tm_step_proper_palindrome_center :
forall (m n k : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
@ -521,10 +790,17 @@ Proof.
assert (K': even (length a') = true). rewrite I'.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
apply le_0_n.
*)
(* montrer que length (hd'++a') est pair à l'aide de
H : tm_step n = hd' ++ a' ++ map negb (rev a') ++ tl'
(* le motif XX YY -> préfixe congru à 5 ou à 7 modulo 8
donc double du préfixe congru à 2 modulo 4
compatible avec ???
Lemma tm_step_palindromic_even_center' :
forall (n k m: nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ (rev a) ++ tl
-> 0 < length a
-> length (hd ++ a) = S (2 * k) * 2^m
-> odd m = true.
*)