Update
This commit is contained in:
Thomas Baruchel
parent
8a73ed35ad
commit
afa6e9cdf9
|
|
@ -91,208 +91,75 @@ Qed.
|
|||
All squared factors of odd length have length 1 or 3.
|
||||
*)
|
||||
|
||||
Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ tl -> length a = 5
|
||||
-> a <> [ true; false; true; false; true].
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
||||
destruct n.
|
||||
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
||||
rewrite H in H0 at 2. simpl in H0.
|
||||
rewrite app_length in H0. rewrite app_length in H0.
|
||||
rewrite I in H0. rewrite Nat.add_shuffle3 in H0.
|
||||
apply Nat.succ_inj in H0. inversion H0.
|
||||
|
||||
assert (even (length (tm_step (S n))) = true).
|
||||
rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul.
|
||||
apply Nat.le_0_l.
|
||||
|
||||
assert (J: even (length hd) = negb (even (length tl))).
|
||||
rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
|
||||
rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0.
|
||||
destruct (even (length hd)); destruct (even (length tl)).
|
||||
inversion H0. reflexivity. reflexivity. inversion H0.
|
||||
|
||||
assert (K: {a=[true; false; true; false; true]}
|
||||
+ {~ a=[ true; false; true; false; true]}).
|
||||
apply list_eq_dec. apply bool_dec. destruct K.
|
||||
|
||||
assert ({even (length hd) = true} + {even (length hd) <> true}).
|
||||
apply bool_dec. destruct H1.
|
||||
|
||||
(* case length hd is even *)
|
||||
rewrite e0 in J. rewrite Nat.negb_even in J.
|
||||
destruct tl. inversion J.
|
||||
destruct b.
|
||||
|
||||
assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
|
||||
generalize e0. generalize H. apply tm_step_count_occ.
|
||||
|
||||
assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true
|
||||
= count_occ Bool.bool_dec (hd ++ a ++ [true]) false).
|
||||
assert (even (length (hd ++ a ++ [true])) = true).
|
||||
rewrite app_length. rewrite app_length.
|
||||
rewrite Nat.even_add. rewrite Nat.even_add.
|
||||
rewrite e0. rewrite e. reflexivity.
|
||||
replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H.
|
||||
generalize H2. generalize H. apply tm_step_count_occ.
|
||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
||||
rewrite <- app_assoc. reflexivity.
|
||||
|
||||
rewrite count_occ_app in H2. rewrite H1 in H2.
|
||||
symmetry in H2.
|
||||
rewrite count_occ_app in H2. rewrite Nat.add_cancel_l in H2.
|
||||
|
||||
rewrite count_occ_app in H2. rewrite count_occ_app in H2.
|
||||
rewrite e in H2. simpl in H2. inversion H2.
|
||||
|
||||
replace (hd ++ a ++ false::tl)
|
||||
with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
||||
simpl. apply Nat.lt_0_2.
|
||||
|
||||
rewrite e. reflexivity.
|
||||
|
||||
(* case length hd is odd *)
|
||||
apply not_true_is_false in n0.
|
||||
rewrite app_removelast_last with (l := hd) (d := true) in H.
|
||||
rewrite app_removelast_last with (l := hd) (d := true) in n0.
|
||||
rewrite app_length in n0. simpl in n0.
|
||||
rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0.
|
||||
rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0.
|
||||
|
||||
destruct (last hd true).
|
||||
rewrite <- app_assoc in H.
|
||||
assert (count_occ Bool.bool_dec (removelast hd) true
|
||||
= count_occ Bool.bool_dec (removelast hd) false).
|
||||
generalize n0. generalize H. apply tm_step_count_occ.
|
||||
replace (removelast hd ++ [true] ++ a ++ tl)
|
||||
with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H.
|
||||
assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true
|
||||
= count_occ Bool.bool_dec (removelast hd ++ [true;true]) false).
|
||||
assert (even (length (removelast hd ++ [true;true])) = true).
|
||||
rewrite app_length. rewrite Nat.even_add_even. assumption.
|
||||
apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
|
||||
generalize H2. generalize H. apply tm_step_count_occ.
|
||||
|
||||
rewrite count_occ_app in H2. rewrite count_occ_app in H2.
|
||||
rewrite H1 in H2. rewrite Nat.add_cancel_l in H2.
|
||||
simpl in H2. inversion H2.
|
||||
|
||||
rewrite e. rewrite app_assoc_reverse. reflexivity.
|
||||
|
||||
replace ((removelast hd ++ [false]) ++ a ++ tl)
|
||||
with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
||||
simpl. apply Nat.lt_0_2.
|
||||
|
||||
rewrite e. rewrite app_assoc_reverse. reflexivity.
|
||||
|
||||
assert (length hd <> 0). destruct hd. inversion n0.
|
||||
simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
|
||||
assert (length hd <> 0). destruct hd. inversion n0.
|
||||
simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
|
||||
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ tl -> length a = 5
|
||||
-> a <> [ false; true; false; true; false].
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
assert (K: {a=[false; true; false; true; false]}
|
||||
+ {~ a=[false; true; false; true; false]}).
|
||||
apply list_eq_dec. apply bool_dec. destruct K.
|
||||
assert (tm_step (S n) = hd ++ a ++ tl
|
||||
++ (map negb hd) ++ [ true; false; true; false; true ]
|
||||
++ (map negb tl)).
|
||||
rewrite tm_build. rewrite H.
|
||||
rewrite map_app. rewrite map_app.
|
||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
||||
rewrite <- app_assoc. rewrite e. reflexivity.
|
||||
rewrite app_assoc in H0. rewrite app_assoc in H0.
|
||||
rewrite app_assoc in H0. apply tm_step_factor5 in H0.
|
||||
contradiction H0. reflexivity.
|
||||
reflexivity. assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma tm_step_consecutive_identical_length :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ tl -> length a = 5
|
||||
-> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
|
||||
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. inversion I.
|
||||
|
||||
assert (a = nil). simpl in I.
|
||||
apply Nat.succ_inj in I. apply Nat.succ_inj in I.
|
||||
apply Nat.succ_inj in I. apply Nat.succ_inj in I.
|
||||
apply Nat.succ_inj in I.
|
||||
apply length_zero_iff_nil in I. assumption.
|
||||
rewrite H0. rewrite H0 in H. rewrite H0 in I.
|
||||
|
||||
destruct b; destruct b0; destruct b1; destruct b2; destruct b3.
|
||||
|
||||
exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity.
|
||||
exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity.
|
||||
|
||||
exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
|
||||
exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
|
||||
apply tm_step_factor5 in H. contradiction H. reflexivity. reflexivity.
|
||||
exists (true::false::true::nil). exists (nil). exists false. simpl. reflexivity.
|
||||
exists (true::false::false::nil). exists (nil). exists true. simpl. reflexivity.
|
||||
exists (true::nil). exists (true::false::nil). exists false. simpl. reflexivity.
|
||||
exists (true::nil). exists (false::true::nil). exists false. simpl. reflexivity.
|
||||
exists (true::false::nil). exists (false::nil). exists false. simpl. reflexivity.
|
||||
exists (false::nil). exists (true::true::nil). exists true. simpl. reflexivity.
|
||||
exists (false::nil). exists (true::false::nil). exists true. simpl. reflexivity.
|
||||
exists (false::nil). exists (false::true::nil). exists true. simpl. reflexivity.
|
||||
exists (false::nil). exists (false::false::nil). exists true. simpl. reflexivity.
|
||||
exists (false::true::false::nil). exists (nil). exists true. simpl. reflexivity.
|
||||
apply tm_step_factor5' in H. contradiction H. reflexivity. reflexivity.
|
||||
exists (false::true::nil). exists (true::nil). exists false. simpl. reflexivity.
|
||||
exists (false::true::nil). exists (false::nil). exists false. simpl. reflexivity.
|
||||
exists (false::false::nil). exists (true::nil). exists true. simpl. reflexivity.
|
||||
exists (false::false::nil). exists (false::nil). exists true. simpl. reflexivity.
|
||||
exists (nil). exists (true::false::true::nil). exists false. simpl. reflexivity.
|
||||
exists (nil). exists (true::false::false::nil). exists false. simpl. reflexivity.
|
||||
exists (nil). exists (false::true::true::nil). exists false. simpl. reflexivity.
|
||||
exists (nil). exists (false::true::false::nil). exists false. simpl. reflexivity.
|
||||
exists (nil). exists (false::false::true::nil). exists false. simpl. reflexivity.
|
||||
exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_consecutive_identical_length' :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ tl -> 4 < length a
|
||||
-> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
rewrite <- firstn_skipn with (l := a) (n := 5).
|
||||
assert (length (firstn 5 a) = 5).
|
||||
apply firstn_length_le. apply Nat.le_succ_l. apply I.
|
||||
rewrite <- firstn_skipn with (l := a) (n := 5) in H.
|
||||
rewrite <- app_assoc in H.
|
||||
assert (exists (b1 c1 : list bool) (d1 : bool),
|
||||
firstn 5 a = b1 ++ [d1; d1] ++ c1).
|
||||
generalize H0. generalize H. apply tm_step_consecutive_identical_length.
|
||||
destruct H1. destruct H1. destruct H1. rewrite H1.
|
||||
exists x. exists (x0 ++ (skipn 5 a)). exists x1.
|
||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
||||
rewrite <- app_assoc. reflexivity.
|
||||
Qed.
|
||||
assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
|
||||
apply Nat.Even_or_Odd. destruct J as [J | J].
|
||||
|
||||
(* first case *)
|
||||
replace (hd++a++tl)
|
||||
with ((hd ++ (firstn 1 a)) ++ (skipn 1 (firstn 5 a))
|
||||
++ ((skipn 5 a) ++ tl)) in H.
|
||||
|
||||
assert (length (skipn 1 (firstn 5 a)) = 4).
|
||||
rewrite skipn_length. rewrite firstn_length.
|
||||
rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
|
||||
reflexivity. assumption.
|
||||
|
||||
assert (odd (length (hd ++ firstn 1 a)) = true).
|
||||
rewrite app_length. rewrite Nat.odd_add. rewrite <- Nat.negb_even.
|
||||
apply Nat.Even_EvenT in J. apply Nat.EvenT_even in J. rewrite J.
|
||||
rewrite firstn_length. rewrite Nat.min_l. reflexivity.
|
||||
|
||||
apply Nat.lt_le_incl.
|
||||
assert (1 < 4). rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
generalize I. generalize H1. apply Nat.lt_trans.
|
||||
|
||||
assert (exists (x : bool) (u v : list bool),
|
||||
skipn 1 (firstn 5 a) = u ++ [x;x] ++ v).
|
||||
generalize H1. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
|
||||
destruct H2. destruct H2. destruct H2.
|
||||
exists ((firstn 1 a) ++ x0). exists (x1 ++ (skipn 5 a)). exists x.
|
||||
replace ((firstn 1 a ++ x0) ++ [x; x] ++ x1 ++ skipn 5 a)
|
||||
with (firstn 1 a ++ (x0 ++ [x;x] ++ x1) ++ skipn 5 a). rewrite <- H2.
|
||||
rewrite app_assoc. replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
|
||||
rewrite firstn_skipn. rewrite firstn_skipn. reflexivity.
|
||||
rewrite firstn_firstn. reflexivity.
|
||||
rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
|
||||
reflexivity.
|
||||
rewrite <- app_assoc. apply app_inv_head_iff.
|
||||
replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
|
||||
rewrite app_assoc. rewrite firstn_skipn.
|
||||
rewrite app_assoc. rewrite firstn_skipn.
|
||||
reflexivity.
|
||||
rewrite firstn_firstn. reflexivity.
|
||||
|
||||
(* second case *)
|
||||
replace (hd++a++tl) with (hd ++ (firstn 4 a) ++ ((skipn 4 a) ++ tl)) in H.
|
||||
|
||||
assert (length (firstn 4 a) = 4). rewrite firstn_length.
|
||||
rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
|
||||
reflexivity. assert (4 <= 5). apply Nat.le_succ_diag_r.
|
||||
generalize I. generalize H0. apply Nat.le_trans.
|
||||
|
||||
apply Nat.Odd_OddT in J. apply Nat.OddT_odd in J.
|
||||
|
||||
assert (exists (x : bool) (u v : list bool), firstn 4 a = u ++ [x;x] ++ v).
|
||||
generalize J. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
|
||||
destruct H1. destruct H1. destruct H1.
|
||||
exists x0. exists (x1++(skipn 4 a)). exists x.
|
||||
|
||||
replace (x0 ++ [x;x] ++ x1 ++ (skipn 4 a))
|
||||
with ((x0++[x;x]++x1) ++ (skipn 4 a)).
|
||||
rewrite <- H1. rewrite firstn_skipn. reflexivity.
|
||||
rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
|
||||
apply app_inv_head_iff.
|
||||
rewrite app_assoc. rewrite firstn_skipn. reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
|
||||
|
|
@ -301,7 +168,7 @@ Proof.
|
|||
assert (J: 4 < length a \/ length a <= 4).
|
||||
apply Nat.lt_ge_cases. destruct J.
|
||||
assert (exists b c d, a = b ++ [d;d] ++ c).
|
||||
generalize H0. generalize H. apply tm_step_consecutive_identical_length'.
|
||||
generalize H0. generalize H. apply tm_step_consecutive_identical_length.
|
||||
destruct H1. destruct H1. destruct H1. rewrite H1 in H.
|
||||
|
||||
replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
|
||||
|
|
@ -829,7 +696,3 @@ Proof.
|
|||
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
|
||||
(* TODO: la taille du facteur divise la taille du préfixe ? *)
|
||||
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user