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-02 22:17:33 +01:00
parent 258bfc5251
commit 33746ab603
1 changed files with 124 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
thue-morse.v
View File

@ -1032,24 +1032,137 @@ Proof.
Qed.
Lemma tm_step_cube2 : forall (n : nat) (a hd tl: list bool),
Lemma tm_step_cube3 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length hd) = false
-> 0 < length a
-> hd_error a = hd_error tl.
Proof.
intros n a hd tl. intros H I J.
assert (even (length hd) = even (length tl)).
generalize J. generalize H. apply tm_step_cube2.
assert (even (length a) = true). generalize H. apply tm_step_cube1.
rewrite I in H0.
destruct a.
- simpl in J. apply Nat.lt_irrefl in J. contradiction J.
- destruct tl. simpl in H0. inversion H0.
simpl. replace (b::a) with ((b::nil) ++ a) in H.
replace (hd ++ ([b] ++ a) ++ ([b] ++ a) ++ ([b] ++ a) ++ (b0::tl))
with ((hd ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b::nil)) ++ (a ++ (b0::nil)) ++ tl) in H.
assert (even (length (hd ++ (b::nil))) = true).
rewrite last_length.
rewrite Nat.even_succ. rewrite <- Nat.negb_even. rewrite I. reflexivity.
assert (count_occ Bool.bool_dec (hd ++ (b::nil)) true
= count_occ Bool.bool_dec (hd ++ (b::nil)) false).
generalize H2. generalize H. apply tm_step_count_occ.
assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)))) = true).
rewrite app_length. rewrite Nat.even_add. rewrite H2.
rewrite last_length.
replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
reflexivity.
assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) true
= count_occ Bool.bool_dec ((hd ++ [b]) ++ a ++ [b]) false).
generalize H4. rewrite app_assoc in H. generalize H. apply tm_step_count_occ.
assert (K := H5).
rewrite count_occ_app in H5. symmetry in H5. rewrite count_occ_app in H5.
rewrite H3 in H5. rewrite Nat.add_cancel_l in H5.
assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)))) = true).
rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
rewrite last_length.
replace (length (b::a)) with (S (length a)) in H1. rewrite H1. reflexivity.
reflexivity.
assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) true
= count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b])) false).
generalize H6.
rewrite app_assoc in H. rewrite app_assoc in H.
replace (((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b])
with ((hd ++ [b]) ++ (a ++ [b]) ++ a ++ [b]) in H.
generalize H. apply tm_step_count_occ.
rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
assert (even (length ((hd ++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b::nil)) ++ (a++ (b0::nil)))) = true).
rewrite app_assoc. rewrite app_length. rewrite Nat.even_add. rewrite H4.
rewrite app_length. rewrite last_length.
replace (length (b::a)) with (S (length a)) in H1. rewrite Nat.even_add. rewrite H1.
rewrite last_length. rewrite H1. reflexivity. reflexivity.
assert (count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) true
= count_occ Bool.bool_dec ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) false).
generalize H8.
rewrite app_assoc in H. rewrite app_assoc in H. rewrite app_assoc in H.
replace ((((hd ++ [b]) ++ a ++ [b]) ++ a ++ [b]) ++ a ++ [b0])
with ((hd ++ [b]) ++ (a ++ [b]) ++ (a ++ [b]) ++ (a ++ [b0])) in H.
generalize H. apply tm_step_count_occ.
rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
rewrite app_assoc_reverse. rewrite app_assoc_reverse. rewrite app_assoc_reverse.
apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc_reverse. apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
rewrite H3 in H9. rewrite Nat.add_cancel_l in H9.
rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
rewrite count_occ_app in H9. symmetry in H9. rewrite count_occ_app in H9.
rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
destruct b; destruct b0.
reflexivity.
rewrite count_occ_app in H9. rewrite count_occ_app in H9.
rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
rewrite H5 in H9.
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
rewrite Nat.add_cancel_l in H9. inversion H9.
reflexivity. easy. easy. reflexivity.
rewrite count_occ_app in H9. rewrite count_occ_app in H9.
rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
rewrite count_occ_app in H5. rewrite count_occ_app in H5.
rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
rewrite <- H5 in H9.
rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
rewrite Nat.add_cancel_l in H9. inversion H9.
easy. reflexivity. reflexivity. easy.
reflexivity.
rewrite app_assoc_reverse. apply app_inv_head_iff.
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
rewrite app_assoc_reverse. rewrite app_assoc_reverse.
apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc_reverse.
apply app_inv_head_iff. apply app_inv_head_iff.
rewrite app_assoc_reverse.
reflexivity.
reflexivity.
Qed.
(hd + [a] + [a] + [a])
-> prouver que le premier caractère qui suit hd suit aussi le troisième a
quand hd est de taille impaire
[hd + false] + /a+false/
Prouver que si un cube existe de taille k, il existe aussi un cube