Update
This commit is contained in:
Thomas Baruchel
parent
6aa1efe86c
commit
f55b756129
|
|
@ -739,10 +739,220 @@ Proof.
|
|||
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 *)
|
||||
destruct tl. rewrite app_nil_r in H.
|
||||
assert (length (tm_step n) = length (tm_step n)). reflexivity.
|
||||
rewrite H in H2 at 2.
|
||||
assert (even (length (tm_step n)) = even (length (tm_step n))). reflexivity.
|
||||
rewrite H in H3 at 2. rewrite app_length in H3. rewrite app_length in H3.
|
||||
rewrite Nat.even_add in H3.
|
||||
rewrite Nat.even_add in H3.
|
||||
rewrite H0 in H3. symmetry in H3.
|
||||
rewrite <- Nat.negb_odd in H3. rewrite H1 in H3. simpl in H3.
|
||||
rewrite tm_size_power2 in H3. destruct n.
|
||||
assert (1 < length (hd ++ a ++ a)). rewrite app_length.
|
||||
apply Nat.lt_lt_add_l. rewrite app_length.
|
||||
rewrite <- Nat.le_succ_l in I. rewrite <- Nat.le_succ_l.
|
||||
rewrite <- Nat.add_1_r. apply Nat.add_le_mono; assumption.
|
||||
rewrite <- H2 in H4. apply Nat.lt_irrefl in H4. contradiction H4.
|
||||
rewrite Nat.pow_succ_r' in H3. rewrite Nat.even_mul in H3.
|
||||
simpl in H3. inversion H3.
|
||||
|
||||
(* 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 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 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 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.
|
||||
|
||||
|
||||
|
||||
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
|
||||
(* TODO: la taille du facteur divise la taille du préfixe ? *)
|
||||
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
Lemma xxx : 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.
|
||||
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.
|
||||
|
||||
assert (forall (n' : nat) (w z y : list bool),
|
||||
tm_step n' = w ++ z ++ y
|
||||
-> length z = 4 -> length w mod 4 = 1
|
||||
-> exists (x : bool), firstn 2 z = [x;x]).
|
||||
intros n' w z y. intros G0 G1 G2.
|
||||
assert (U: 4 * (length w / 4) <= length w).
|
||||
apply Nat.mul_div_le. easy.
|
||||
assert (W: length w < length (tm_step n')). rewrite G0.
|
||||
rewrite app_length. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_lt_mono_l.
|
||||
rewrite app_length. rewrite G1. apply Nat.lt_0_succ.
|
||||
assert (Q: length z <= length (tm_step n')). rewrite G0.
|
||||
rewrite app_length. rewrite app_length.
|
||||
rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
|
||||
apply Nat.le_add_l. rewrite tm_size_power2 in Q. rewrite G1 in Q.
|
||||
replace (4) with (2^2) in Q. rewrite <- Nat.pow_le_mono_r_iff in Q.
|
||||
assert (O: nth_error (tm_step 2) 1 = nth_error (tm_step 2) 2
|
||||
<-> nth_error (tm_step (2+(n'-2))) (length w / 4 * 2 ^ 2 + 1)
|
||||
= nth_error (tm_step (2+(n'-2))) (length w / 4 * 2 ^ 2 + 2)).
|
||||
apply tm_step_repeating_patterns.
|
||||
simpl. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
|
||||
apply Nat.lt_0_succ.
|
||||
rewrite Nat.mul_lt_mono_pos_l with (p := 2^2). rewrite <- Nat.pow_add_r.
|
||||
rewrite Nat.add_comm. rewrite Nat.sub_add.
|
||||
replace (2^2) with 4.
|
||||
rewrite tm_size_power2 in W. generalize W. generalize U.
|
||||
apply Nat.le_lt_trans. reflexivity.
|
||||
assumption.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
rewrite Nat.mul_comm in O. replace (2^2) with 4 in O.
|
||||
rewrite <- G2 in O at 9. rewrite <- G2 in O at 14.
|
||||
replace (4 * (length w / 4) + S (length w mod 4))
|
||||
with (S (length w)) in O. rewrite <- Nat.div_mod_eq in O.
|
||||
replace (2+(n'-2)) with n' in O. rewrite G0 in O.
|
||||
rewrite nth_error_app2 in O. rewrite Nat.sub_diag in O.
|
||||
rewrite nth_error_app1 in O. rewrite nth_error_app2 in O.
|
||||
rewrite Nat.sub_succ_l in O. rewrite Nat.sub_diag in O.
|
||||
rewrite nth_error_app1 in O. destruct O.
|
||||
assert (nth_error z 0 = nth_error z 1). apply H0. reflexivity.
|
||||
rewrite nth_error_nth' with (d := false) in H2.
|
||||
rewrite nth_error_nth' with (d := false) in H2.
|
||||
exists (nth 0 z false). inversion H2.
|
||||
rewrite H4 at 2.
|
||||
destruct z. inversion G1. destruct z. inversion G1. reflexivity.
|
||||
rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
rewrite G1. apply Nat.lt_0_succ.
|
||||
rewrite G1. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||
apply Nat.le_refl. apply Nat.le_succ_diag_r.
|
||||
rewrite G1. apply Nat.lt_0_succ. apply Nat.le_refl.
|
||||
rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
|
||||
reflexivity. easy. assumption.
|
||||
rewrite Nat.add_succ_r. rewrite <- Nat.div_mod_eq. reflexivity.
|
||||
reflexivity. apply Nat.lt_1_2. reflexivity.
|
||||
|
||||
destruct M as [M | M].
|
||||
- assert (exists (x : bool), firstn 2 a = [x;x]).
|
||||
generalize M. generalize I. generalize H. apply H0.
|
||||
destruct H1. exists x. exists nil. exists (skipn 2 a).
|
||||
rewrite app_nil_l. rewrite <- H1. symmetry. apply firstn_skipn.
|
||||
- assert ((length (hd ++ (firstn 2 a))) mod 4 = 1).
|
||||
rewrite app_length. rewrite firstn_length. rewrite I.
|
||||
rewrite <- Nat.add_mod_idemp_l. rewrite M. reflexivity. easy.
|
||||
assert (tm_step (S n) = tm_step n ++ map negb (tm_step n)).
|
||||
apply tm_build. rewrite H in H2.
|
||||
assert (length ((skipn 2 a)
|
||||
++ (firstn 2 (tl ++ (map negb (hd ++ a ++ tl))))) = 4).
|
||||
rewrite app_length. rewrite skipn_length. rewrite I.
|
||||
rewrite firstn_length. rewrite app_length. rewrite <- H.
|
||||
rewrite map_length.
|
||||
assert (4 <= length tl + length (tm_step n)).
|
||||
assert (Q: length a <= length (tm_step n)). rewrite H.
|
||||
rewrite app_length. rewrite app_length.
|
||||
rewrite Nat.add_assoc. rewrite Nat.add_shuffle0.
|
||||
apply Nat.le_add_l. rewrite I in Q.
|
||||
rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
|
||||
apply Nat.le_0_l. assumption. rewrite Nat.min_l. reflexivity.
|
||||
assert (2 <= 4). apply le_n_S. apply le_n_S. apply Nat.le_0_l.
|
||||
generalize H3. generalize H4. apply Nat.le_trans.
|
||||
replace ((hd ++ a ++ tl) ++ map negb (hd ++ a ++ tl))
|
||||
with ((hd ++ firstn 2 a)
|
||||
++ (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
|
||||
++ (skipn 2 (tl ++ map negb (hd ++ a ++ tl)))) in H2.
|
||||
assert (exists (x : bool),
|
||||
firstn 2 (skipn 2 a ++ firstn 2 (tl ++ map negb (hd ++ a ++ tl)))
|
||||
= [x;x]).
|
||||
generalize H1. generalize H3. generalize H2. apply H0.
|
||||
destruct H4. exists x. exists (firstn 2 a). exists nil.
|
||||
rewrite <- H4. rewrite firstn_app. rewrite skipn_length. rewrite I.
|
||||
replace (2 - (4 - 2)) with 0. rewrite firstn_O.
|
||||
rewrite app_nil_r. rewrite app_nil_r.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. reflexivity. inversion I.
|
||||
reflexivity.
|
||||
rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
|
||||
apply app_inv_head_iff.
|
||||
rewrite <- app_assoc. symmetry. rewrite <- app_assoc.
|
||||
rewrite firstn_skipn.
|
||||
rewrite <- firstn_skipn with (n := 2) (l := a) at 4.
|
||||
rewrite <- app_assoc. reflexivity.
|
||||
- reflexivity.
|
||||
Qed.
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user