Update
This commit is contained in:
Thomas Baruchel
parent
6ccbfa81a4
commit
24f147ebc0
|
|
@ -1191,47 +1191,57 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
|||
destruct s0. inversion H15. destruct s0. inversion H15.
|
||||
destruct s0. inversion H15. destruct s0; inversion H15.
|
||||
inversion H15. reflexivity.
|
||||
(*
|
||||
assert (b13 = b0). destruct b13; destruct b1; destruct b0.
|
||||
reflexivity. inversion H46. reflexivity. inversion H45.
|
||||
inversion H45. reflexivity. inversion H45. reflexivity.
|
||||
rewrite H17 in H15. rewrite H17 in H47. rewrite <- H47 in H15.
|
||||
rewrite <- H47 in H33. rewrite <- H33 in H15.
|
||||
rewrite <- H47 in H24. rewrite <- H24 in H15.
|
||||
rewrite <- H47 in H26. rewrite <- H26 in H15.
|
||||
rewrite <- H47 in H39. rewrite <- H39 in H15.
|
||||
rewrite <- H47 in H41. rewrite <- H41 in H15.
|
||||
rewrite <- H47 in H43. rewrite <- H43 in H15.
|
||||
rewrite negb_involutive in H15. rewrite negb_involutive in H15.
|
||||
fold s in H15.
|
||||
*)
|
||||
rewrite H17 in H.
|
||||
|
||||
(* à ce stade H est contradictoire *)
|
||||
assert (even (length h0) = false).
|
||||
replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0)
|
||||
with (h0 ++ [b0] ++ [b0] ++ ([b1; b1; b0; b0; b1; b1] ++ t0)) in H.
|
||||
assert (odd (length [b0]) = true). reflexivity. generalize H18.
|
||||
generalize H. apply tm_step_odd_prefix_square. reflexivity.
|
||||
replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0)
|
||||
with (h0 ++ [b0;b0;b1;b1] ++ [b0;b0;b1;b1] ++ t0) in H.
|
||||
assert (even (length h0) = true).
|
||||
assert (even (length (h0 ++ [b0;b0;b1;b1])) = true).
|
||||
assert (0 < length [b0;b0;b1;b1]). simpl. apply Nat.lt_0_succ.
|
||||
generalize H19. generalize H. apply tm_step_square_pos.
|
||||
rewrite app_length in H19. rewrite Nat.even_add in H19.
|
||||
rewrite H18 in H19. inversion H19. rewrite H18 in H19.
|
||||
inversion H19. reflexivity. reflexivity.
|
||||
rewrite <- length_zero_iff_nil. rewrite Y''. easy.
|
||||
|
||||
Lemma tm_morphism_app : forall (l1 l2 : list bool),
|
||||
tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
|
||||
Lemma tm_morphism_app2 : forall (l hd tl : list bool),
|
||||
tm_morphism l = hd ++ tl
|
||||
-> even (length hd) = true
|
||||
-> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
|
||||
Lemma tm_morphism_app3 : forall (l hd tl : list bool),
|
||||
tm_morphism l = hd ++ tl
|
||||
-> even (length hd) = true
|
||||
-> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
|
||||
|
||||
(* fin de la preuve, on a b8 <> b9 *)
|
||||
right. rewrite U. simpl. injection. inversion H7. rewrite H9 in n6.
|
||||
contradiction n6. reflexivity.
|
||||
|
||||
rewrite removelast_firstn_len. rewrite removelast_firstn_len. simpl.
|
||||
rewrite <- length_zero_iff_nil. easy.
|
||||
|
||||
rewrite <- length_zero_iff_nil.
|
||||
rewrite removelast_firstn_len. easy.
|
||||
|
||||
apply Nat.lt_1_2. easy.
|
||||
|
||||
|
||||
(* désormais on a b <> b1 ; il suffit de montrer que b = b0 pour
|
||||
arriver à un bloc de 2 contenant deux termes identiques *)
|
||||
assert (b = b0). destruct b; destruct b1; destruct b0.
|
||||
reflexivity. contradiction n2. reflexivity. reflexivity.
|
||||
contradiction n1. reflexivity. contradiction n1. reflexivity.
|
||||
reflexivity. contradiction n2. reflexivity. reflexivity.
|
||||
rewrite H1 in H.
|
||||
|
||||
replace (
|
||||
(b3 :: hd) ++ b0 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl)
|
||||
with (
|
||||
(b3 :: hd) ++ [b0] ++ [b0]
|
||||
++ b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl) in H.
|
||||
assert (even (length (b3 :: hd)) = false).
|
||||
assert (odd (length [b0]) = true). reflexivity. generalize H2.
|
||||
generalize H. apply tm_step_odd_prefix_square. rewrite H2 in Q.
|
||||
inversion Q. reflexivity.
|
||||
|
||||
Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> odd (length a) = true -> even (length hd) = false.
|
||||
Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ a ++ tl
|
||||
-> 0 < length a -> even (length (hd ++ a)) = true.
|
||||
(* fin de la destructuration de a, désormais trop grand
|
||||
cf. hypothèse I *)
|
||||
|
||||
|
||||
|
||||
|
|
@ -1240,66 +1250,6 @@ Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
|
|||
|
||||
|
||||
|
||||
Proof.
|
||||
|
||||
|
||||
|
||||
|
||||
False, True, True, False, True, False, False, True, True, False, False
|
||||
|
||||
Admitted.
|
||||
|
||||
|
||||
TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
|
||||
FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
|
||||
FTTFTFFT FTTFTF (pb avec le repeating_pattern de 8 ???)
|
||||
TFT TFT FF TFT TFT (si on part sur 2 mod 8)
|
||||
(idem en partant de la droite pour 6 mod 8)
|
||||
Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* si on a ensuite le bloc précédent identique aux deux premiers de a
|
||||
|
||||
|
||||
|
||||
|
||||
(* TODO : terminer avec une inversion sur la longueur de a ;
|
||||
le dernier but vient de la destructuration initiale de a *)
|
||||
|
||||
|
||||
|
||||
F T | T F | T F ][ F T | F T T F
|
||||
4n
|
||||
|
||||
ou F T | T F ][ F T | T F
|
||||
4n ou 4n
|
||||
|
||||
F T F T T F F T T F T F (centre 4n+2 ET 4n : contra)
|
||||
T F F T T F F T T F T F (centre : 4n+2)
|
||||
F T F T T F F T T F F T (centre : 4n)
|
||||
T F F T T F F T T F F T (cubes)
|
||||
|
||||
|
||||
|
||||
|
||||
--> T F F T | T F ][ F T | T F F T (impossible : cubes)
|
||||
--> F T F T | T F ][ F T | T F T F
|
||||
|
||||
Bilan : seulement deux cas possible de palindrome 8
|
||||
F T | T F | T F ][ F T | F T | T F
|
||||
4n+2 4n+2 (trivial)
|
||||
|
||||
F T | F T | T F ][ F T | T F | T F
|
||||
4n (par examen des cinq premiers termes à gauche)
|
||||
|
||||
*)
|
||||
|
||||
|
||||
Lemma tm_step_palindromic_length_12 :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
|
|
|
|||
Loading…
Reference in New Issue