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-15 08:29:10 +01:00
parent 22b6ec0a63
commit f34f5d3afd
2 changed files with 243 additions and 125 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/thue_morse.v
View File

@ -434,6 +434,52 @@ Proof.
reflexivity.
Qed.
Theorem tm_step_length_even : forall (n : nat),
0 < n -> even (length (tm_step n)) = true.
Proof.
intro n. intro H.
rewrite tm_size_power2. destruct n. inversion H.
rewrite Nat.pow_succ_r'. rewrite Nat.even_mul. reflexivity.
Qed.
Theorem tm_step_not_nil_factor_even : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> even (length a) = true
-> 0 < n.
Proof.
intros n hd a tl. intros H I J.
assert (M: 1 < length (tm_step n)). rewrite H.
rewrite app_length. rewrite app_length.
assert (0 <= length hd). apply le_0_n.
assert (2 <= length a + length tl). rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. destruct a. inversion I.
destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply le_0_n.
apply le_0_n. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l.
rewrite plus_n_Sm. apply Nat.add_le_mono; assumption.
rewrite tm_size_power2 in M.
rewrite Nat.pow_lt_mono_r_iff with (a := 2). simpl. assumption.
apply Nat.lt_1_2.
Qed.
Theorem tm_step_tail_not_nil_prefix_odd : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> odd (length hd) = true
-> even (length a) = true
-> nil <> tl.
Proof.
intros n hd a tl. intros H I J K.
assert (L: 0 < n). generalize K. generalize I. generalize H.
apply tm_step_not_nil_factor_even.
assert (M: even (length (tm_step n)) = true). generalize L.
apply tm_step_length_even.
destruct tl. rewrite app_nil_r in H.
rewrite H in M. rewrite app_length in M.
rewrite Nat.even_add in M. rewrite K in M. rewrite <- Nat.negb_odd in M.
rewrite J in M. inversion M. apply nil_cons.
Qed.
(**
The following lemmas and theorems focus on the stability of the sequence:

322
src/thue_morse2.v
View File

@ -392,53 +392,6 @@ Proof.
Qed.
Theorem tm_step_length_even : forall (n : nat),
0 < n -> even (length (tm_step n)) = true.
Proof.
intro n. intro H.
rewrite tm_size_power2. destruct n. inversion H.
rewrite Nat.pow_succ_r'. rewrite Nat.even_mul. reflexivity.
Qed.
Theorem tm_step_not_nil_factor_even : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> even (length a) = true
-> 0 < n.
Proof.
intros n hd a tl. intros H I J.
assert (M: 1 < length (tm_step n)). rewrite H.
rewrite app_length. rewrite app_length.
assert (0 <= length hd). apply le_0_n.
assert (2 <= length a + length tl). rewrite <- Nat.add_0_r at 1.
apply Nat.add_le_mono. destruct a. inversion I.
destruct a. inversion J. simpl. apply le_n_S. apply le_n_S. apply le_0_n.
apply le_0_n. rewrite <- Nat.add_0_l at 1. rewrite <- Nat.le_succ_l.
rewrite plus_n_Sm. apply Nat.add_le_mono; assumption.
rewrite tm_size_power2 in M.
rewrite Nat.pow_lt_mono_r_iff with (a := 2). simpl. assumption.
apply Nat.lt_1_2.
Qed.
Theorem tm_step_tail_not_nil_prefix_odd : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> 0 < length a
-> odd (length hd) = true
-> even (length a) = true
-> nil <> tl.
Proof.
intros n hd a tl. intros H I J K.
assert (L: 0 < n). generalize K. generalize I. generalize H.
apply tm_step_not_nil_factor_even.
assert (M: even (length (tm_step n)) = true). generalize L.
apply tm_step_length_even.
destruct tl. rewrite app_nil_r in H.
rewrite H in M. rewrite app_length in M.
rewrite Nat.even_add in M. rewrite K in M. rewrite <- Nat.negb_odd in M.
rewrite J in M. inversion M. apply nil_cons.
Qed.
@ -448,97 +401,216 @@ Qed.
Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a -> even (length (hd ++ a)) = true.
-> 0 < length a
-> odd (length hd) = true
-> even (length a) = true
-> exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = S (length hd)
/\ length a' = length a.
Proof.
intros n hd a tl. intros H I.
intros n hd a tl. intros H I J K.
rewrite app_length. rewrite Nat.even_add.
assert (J: Nat.even (length a) || Nat.odd (length a) = true).
apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
- rewrite H0.
assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
rewrite H1. reflexivity.
(* proof that tl is not nil *)
assert (W: nil <> tl).
assert (even (length (a++a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite K. reflexivity.
assert (0 < length (a ++ a)). rewrite <- Nat.add_0_r at 1.
rewrite app_length. apply Nat.add_lt_mono; assumption.
generalize H0. generalize J. generalize H1.
replace (hd++a++a++tl) with (hd++(a++a)++tl) in H. generalize H.
apply tm_step_tail_not_nil_prefix_odd. rewrite <- app_assoc. reflexivity.
destruct tl. contradiction W. reflexivity.
(* proof that tl is not nil *)
assert (W: nil <> tl).
assert (even (length (a++a)) = true). rewrite app_length.
rewrite Nat.even_add. rewrite H0. reflexivity.
assert (0 < length (a ++ a)). rewrite <- Nat.add_0_r at 1.
rewrite app_length. apply Nat.add_lt_mono; assumption.
generalize H2. generalize H1. generalize H3.
replace (hd++a++a++tl) with (hd++(a++a)++tl) in H. generalize H.
apply tm_step_tail_not_nil_prefix_odd. rewrite <- app_assoc. reflexivity.
destruct tl. contradiction W. reflexivity.
(* proof that a is not nil *)
destruct a. inversion I.
(* proof that a is not nil *)
destruct a. inversion I.
replace (hd ++ (b0 :: a) ++ (b0 :: a) ++ b :: tl)
with ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl) in H.
assert (even (length (hd ++ [b0])) = true).
rewrite app_length. rewrite Nat.add_1_r. rewrite Nat.even_succ.
assumption.
assert (L: count_occ Bool.bool_dec (hd ++ [b0]) true
= count_occ Bool.bool_dec (hd ++ [b0]) false).
generalize H0. generalize H. apply tm_step_count_occ.
replace (hd ++ (b0 :: a) ++ (b0 :: a) ++ b :: tl)
with ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl) in H.
assert (even (length (hd ++ [b0])) = true).
rewrite app_length. rewrite Nat.add_1_r. rewrite Nat.even_succ.
assumption.
assert (L: count_occ Bool.bool_dec (hd ++ [b0]) true
= count_occ Bool.bool_dec (hd ++ [b0]) false).
generalize H2. generalize H. apply tm_step_count_occ.
replace ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl)
with ((hd ++ [b0] ++ a ++ [b0] ++ a ++ [b]) ++ tl) in H.
assert (even (length (hd ++ [b0] ++ a ++ [b0] ++ a ++ [b])) = true).
rewrite <- app_assoc_reverse. rewrite app_length.
rewrite Nat.even_add. rewrite H0.
rewrite app_length. rewrite app_length. rewrite app_length.
rewrite Nat.add_1_r. rewrite <- Nat.add_succ_comm.
rewrite Nat.even_add.
destruct (even (S (length a))); reflexivity.
assert (M: count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) true
= count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) false).
generalize H1. generalize H. apply tm_step_count_occ.
rewrite app_assoc in M. rewrite count_occ_app in M.
symmetry in M. rewrite count_occ_app in M. rewrite L in M.
rewrite Nat.add_cancel_l in M.
replace ((hd ++ [b0]) ++ a ++ (b0::a) ++ b::tl)
with ((hd ++ [b0] ++ a ++ [b0] ++ a ++ [b]) ++ tl) in H.
assert (even (length (hd ++ [b0] ++ a ++ [b0] ++ a ++ [b])) = true).
rewrite <- app_assoc_reverse. rewrite app_length.
rewrite Nat.even_add. rewrite H2.
rewrite app_length. rewrite app_length. rewrite app_length.
rewrite Nat.add_1_r. rewrite <- Nat.add_succ_comm.
rewrite Nat.even_add.
destruct (even (S (length a))); reflexivity.
assert (M: count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) true
= count_occ Bool.bool_dec (hd ++ [b0]++a++[b0]++a++[b]) false).
generalize H3. generalize H. apply tm_step_count_occ.
rewrite app_assoc in M. rewrite count_occ_app in M.
symmetry in M. rewrite count_occ_app in M. rewrite L in M.
rewrite Nat.add_cancel_l in M.
assert (forall x , x + x = 2*x).
intro x. rewrite <- Nat.mul_1_l with (n := x).
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
rewrite Nat.mul_1_l. reflexivity.
Opaque even. simpl in K. Transparent even.
assert (b = b0). destruct b0; destruct b.
- reflexivity.
- rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H2 in H4. rewrite H2 in H4.
rewrite Nat.mul_cancel_l in H4.
apply count_occ_bool_list2 in H4.
rewrite <- K in H4. rewrite Nat.even_succ in H4.
rewrite <- Nat.negb_even in H4.
destruct (even (length a)); inversion H4. easy.
- rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H2 in H4. rewrite H2 in H4.
rewrite Nat.mul_cancel_l in H4.
apply count_occ_bool_list2 in H4.
rewrite <- K in H4. rewrite Nat.even_succ in H4.
rewrite <- Nat.negb_even in H4.
destruct (even (length a)); inversion H4. easy.
- reflexivity.
- rewrite H3 in H.
exists (hd ++ [b0]). exists (a ++ [b0]). exists tl.
split. rewrite H. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
split. apply last_length. apply last_length.
- rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
- rewrite <- app_assoc. reflexivity.
Qed.
assert (forall x , x + x = 2*x).
intro x. rewrite <- Nat.mul_1_l with (n := x).
rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r.
rewrite Nat.mul_1_l. reflexivity.
Opaque even. simpl in H0. Transparent even.
assert (b = b0). destruct b0; destruct b.
+ reflexivity.
+ rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H4 in H6. rewrite H4 in H6.
rewrite Nat.mul_cancel_l in H6.
apply count_occ_bool_list2 in H6.
rewrite <- H0 in H6. rewrite Nat.even_succ in H6.
rewrite <- Nat.negb_even in H6.
destruct (even (length a)); inversion H6. easy.
+ rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
rewrite count_occ_app in M. rewrite count_occ_app in M.
simpl in M. rewrite Nat.add_1_r in M. rewrite Nat.add_0_r in M.
rewrite Nat.add_succ_r in M. rewrite Nat.add_succ_r in M.
inversion M.
rewrite H4 in H6. rewrite H4 in H6.
rewrite Nat.mul_cancel_l in H6.
apply count_occ_bool_list2 in H6.
rewrite <- H0 in H6. rewrite Nat.even_succ in H6.
rewrite <- Nat.negb_even in H6.
destruct (even (length a)); inversion H6. easy.
+ reflexivity.
+ rewrite H5 in H.
Theorem tm_step_square_pos_even' : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
-> odd (length hd) = true
-> even (length a) = true
-> exists (hd' a' tl' : list bool),
tm_step n = hd' ++ a' ++ a' ++ tl'
/\ length hd' = Nat.pred (length hd)
/\ length a' = length a.
Proof.
intros n hd a tl. intros H I J K.
assert (L: hd = removelast hd ++ last hd false :: nil).
apply app_removelast_last. destruct hd. inversion J. easy.
rewrite L in H.
assert (M: a = removelast a ++ last a false :: nil).
apply app_removelast_last. destruct a. inversion I. easy.
rewrite M in H.
rewrite <- app_assoc in H. rewrite <- app_assoc in H.
rewrite <- app_assoc in H.
assert (U: even (length (removelast hd)) = true).
rewrite L in J. rewrite app_length in J.
rewrite Nat.add_1_r in J. rewrite Nat.odd_succ in J.
assumption.
assert (N: count_occ Bool.bool_dec (removelast hd) true
= count_occ Bool.bool_dec (removelast hd) false).
generalize U. generalize H. apply tm_step_count_occ.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (V: even (length ((removelast hd ++ [last hd false])
++ removelast a)) = true).
rewrite app_length. rewrite <- L. rewrite Nat.even_add.
rewrite <- Nat.negb_odd. rewrite J. rewrite M in K.
rewrite app_length in K. rewrite Nat.add_1_r in K.
rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd.
rewrite K. reflexivity.
assert (O: count_occ Bool.bool_dec
((removelast hd ++ [last hd false]) ++ removelast a) true
= count_occ Bool.bool_dec
((removelast hd ++ [last hd false]) ++ removelast a) false).
generalize V. generalize H. apply tm_step_count_occ.
replace ((removelast hd ++ [last hd false]) ++ removelast a)
with (removelast hd ++ ([last hd false] ++ removelast a)) in O.
rewrite count_occ_app in O. symmetry in O. rewrite count_occ_app in O.
rewrite N in O. rewrite Nat.add_cancel_l in O.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (W: even (length ((((removelast hd ++ [last hd false])
++ removelast a) ++ [last a false])
++ removelast a)) = true).
rewrite app_length. rewrite app_length. rewrite Nat.even_add.
rewrite Nat.even_add. rewrite V.
assert (even (length (removelast a)) = false).
rewrite M in K. rewrite app_length in K. rewrite Nat.add_1_r in K.
rewrite Nat.even_succ in K. rewrite <- Nat.negb_odd. rewrite K.
reflexivity. rewrite H0. reflexivity.
assert (P: count_occ Bool.bool_dec
((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) true
= count_occ Bool.bool_dec
((((removelast hd ++ [last hd false]) ++ removelast a) ++ [last a false]) ++ removelast a) false).
generalize W. generalize H. apply tm_step_count_occ.
rewrite <- app_assoc in P. rewrite <- app_assoc in P.
rewrite <- app_assoc in P.
rewrite count_occ_app in P. symmetry in P. rewrite count_occ_app in P.
rewrite N in P. rewrite Nat.add_cancel_l in P.
rewrite app_assoc in P. rewrite count_occ_app in P. symmetry in P.
rewrite count_occ_app in P. rewrite O in P. rewrite Nat.add_cancel_l in P.
assert (last hd false = last a false).
destruct (last hd false); destruct (last a false).
reflexivity.
simpl in O. simpl in P. rewrite O in P.
rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
inversion P.
simpl in O. simpl in P. rewrite <- O in P. symmetry in P.
rewrite <- Nat.add_1_l in P. rewrite <- Nat.add_succ_comm in P.
rewrite <- Nat.add_0_l in P at 1. rewrite Nat.add_cancel_r in P.
inversion P.
reflexivity.
rewrite H0 in H.
exists (removelast hd). exists ([last a false] ++ removelast a).
exists ([last a false] ++ tl).
split. rewrite H.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
reflexivity.
split.
assert (X: length hd = length hd). reflexivity.
rewrite app_removelast_last with (l := hd) (d := false) in X at 2.
rewrite app_length in X. rewrite Nat.add_1_r in X.
rewrite <- Nat.succ_pred_pos with (n := length hd) in X.
apply Nat.succ_inj. rewrite X. reflexivity.
destruct (length hd). inversion J. apply Nat.lt_0_succ.
destruct hd. inversion J. easy.
rewrite app_length. rewrite Nat.add_comm. rewrite <- app_length.
rewrite <- M. reflexivity.
rewrite <- app_assoc. reflexivity.
Qed.
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
(* TODO: la taille du facteur divise la taille du préfixe ? *)
(* TODO : le cas de la taille 2 est un cas pair facile
grâce à tm_step_factor4_odd_prefix *)
Admitted.
(* TODO: revoir tm_step_cube4 *)