Update
This commit is contained in:
parent
047ed4c527
commit
e1238e5198
@ -329,37 +329,6 @@ Qed.
|
|||||||
prefix being odd or even in front of a squared pattern.
|
prefix being odd or even in front of a squared pattern.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
Lemma tm_step_odd_prefix_square_1 : forall (n : nat) (hd a tl : list bool),
|
|
||||||
tm_step n = hd ++ a ++ a ++ tl
|
|
||||||
-> length a = 1 -> even (length hd) = false.
|
|
||||||
Proof.
|
|
||||||
intros n hd a tl. intros H I.
|
|
||||||
assert (J: Nat.even (length hd) || Nat.odd (length hd) = true).
|
|
||||||
apply Nat.orb_even_odd. apply orb_prop in J. destruct J.
|
|
||||||
- assert (K: count_occ Bool.bool_dec hd true
|
|
||||||
= count_occ Bool.bool_dec hd false).
|
|
||||||
generalize H0. generalize H. apply tm_step_count_occ.
|
|
||||||
assert (L: even (length (hd ++ a ++ a)) = true).
|
|
||||||
rewrite app_length. rewrite app_length. rewrite I.
|
|
||||||
rewrite Nat.even_add_even. assumption. rewrite Nat.add_1_r.
|
|
||||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. easy.
|
|
||||||
assert (M: count_occ Bool.bool_dec (hd ++ a ++ a) true
|
|
||||||
= count_occ Bool.bool_dec (hd ++ a ++ a) false).
|
|
||||||
generalize L. generalize H.
|
|
||||||
replace (hd ++ a ++ a ++ tl) with ((hd ++ a ++ a) ++ tl).
|
|
||||||
apply tm_step_count_occ.
|
|
||||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
|
||||||
rewrite <- app_assoc. reflexivity.
|
|
||||||
rewrite count_occ_app in M. symmetry in M.
|
|
||||||
rewrite count_occ_app in M. rewrite K in M.
|
|
||||||
rewrite Nat.add_cancel_l in M. destruct a.
|
|
||||||
+ inversion I.
|
|
||||||
+ destruct b; simpl in I; apply Nat.succ_inj in I;
|
|
||||||
rewrite length_zero_iff_nil in I; rewrite I in M;
|
|
||||||
simpl in M; inversion M.
|
|
||||||
- rewrite <- Nat.negb_odd. rewrite H0. reflexivity.
|
|
||||||
Qed.
|
|
||||||
|
|
||||||
Lemma tm_step_odd_prefix_square_3 : forall (n : nat) (hd a tl : list bool),
|
Lemma tm_step_odd_prefix_square_3 : forall (n : nat) (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ a ++ tl
|
tm_step n = hd ++ a ++ a ++ tl
|
||||||
-> length a = 3 -> even (length hd) = false.
|
-> length a = 3 -> even (length hd) = false.
|
||||||
@ -430,12 +399,10 @@ Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
|
|||||||
-> odd (length a) = true -> even (length hd) = false.
|
-> odd (length a) = true -> even (length hd) = false.
|
||||||
Proof.
|
Proof.
|
||||||
intros n hd a tl. intros H I.
|
intros n hd a tl. intros H I.
|
||||||
assert (length a < 4).
|
assert (length a < 4). generalize I. generalize H. apply tm_step_odd_square.
|
||||||
generalize I. generalize H. apply tm_step_odd_square.
|
destruct a. inversion I. destruct a.
|
||||||
destruct a. inversion I.
|
rewrite <- negb_true_iff. rewrite Nat.negb_even.
|
||||||
destruct a.
|
generalize H. apply tm_step_consecutive_identical. apply hd.
|
||||||
apply tm_step_odd_prefix_square_1 with (n := n) (a := [b]) (tl := tl).
|
|
||||||
assumption. reflexivity.
|
|
||||||
destruct a. inversion I.
|
destruct a. inversion I.
|
||||||
destruct a.
|
destruct a.
|
||||||
apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl).
|
apply tm_step_odd_prefix_square_3 with (n := n) (a := [b;b0;b1]) (tl := tl).
|
||||||
@ -549,3 +516,4 @@ Proof.
|
|||||||
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
|
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
|
||||||
(* TODO: la taille du facteur divise la taille du préfixe ? *)
|
(* TODO: la taille du facteur divise la taille du préfixe ? *)
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user