Update
This commit is contained in:
Thomas Baruchel
parent
7c83761f32
commit
be18d6fa0d
|
|
@ -2096,6 +2096,134 @@ Proof.
|
|||
Qed.
|
||||
|
||||
|
||||
Lemma tm_step_palindrome_7_destruct :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> length a = 7
|
||||
-> exists x, a = [negb x; negb x; x; negb x; x; x; negb x].
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
||||
assert (J: 6 < length a). rewrite I. apply Nat.lt_succ_diag_r.
|
||||
assert (K: length (hd ++ a) mod 4 = 0). generalize J. generalize H.
|
||||
apply tm_step_palindromic_length_12.
|
||||
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I.
|
||||
|
||||
destruct a.
|
||||
replace (rev [b; b0; b1; b2; b3; b4; b5])
|
||||
with ([b5; b4; b3; b2; b1; b0; b]) in H.
|
||||
|
||||
assert (even (length (hd ++ [b; b0; b1; b2; b3; b4; b5])) = true).
|
||||
rewrite <- Nat.div_exact in K. rewrite K. rewrite Nat.even_mul.
|
||||
reflexivity. easy.
|
||||
assert (odd (length hd) = true). rewrite app_length in H0.
|
||||
rewrite Nat.even_add in H0. simpl in H0. apply eqb_prop in H0.
|
||||
rewrite <- Nat.negb_even. rewrite H0. reflexivity.
|
||||
assert (length hd mod 4 = 1 \/ length hd mod 4 = 3).
|
||||
apply odd_mod4. assumption.
|
||||
destruct H2.
|
||||
|
||||
assert (b3 = b4).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b4; b5]
|
||||
++ [b5; b4; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0]) ++ [b1; b2; b3; b4]
|
||||
++ [b5; b5; b4; b3; b2; b1; b0; b] ++ tl) in H.
|
||||
assert (length (hd ++ [b; b0]) mod 4 = 3).
|
||||
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2.
|
||||
reflexivity. easy.
|
||||
assert (exists x, skipn 2 [b1; b2; b3; b4] = [x; x]).
|
||||
generalize H3.
|
||||
apply tm_step_factor4_3mod4 with (n' := n)
|
||||
(y := [b5; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption.
|
||||
reflexivity. destruct H4. inversion H4. reflexivity.
|
||||
rewrite <- app_assoc. reflexivity. rewrite H3 in H.
|
||||
|
||||
assert (b4 <> b5).
|
||||
replace (hd ++ [b; b0; b1; b2; b4; b4; b5]
|
||||
++ [b5; b4; b4; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1; b2]) ++ [b4] ++ [b4] ++ [b5]
|
||||
++ [b5; b4; b4; b2;b1;b0;b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b4; destruct b5.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b4 <> b2).
|
||||
replace (hd ++ [b; b0; b1; b2; b4; b4; b5]
|
||||
++ [b5; b4; b4; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1; b2; b4; b4; b5; b5])
|
||||
++ [b4] ++ [b4] ++ [b2] ++ [b1;b0;b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b4; destruct b2.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b2 = b5). destruct b2; destruct b4; destruct b5.
|
||||
contradiction H4. reflexivity. contradiction H5. reflexivity.
|
||||
reflexivity. contradiction H4. reflexivity.
|
||||
contradiction H4. reflexivity. reflexivity.
|
||||
contradiction H5. reflexivity. contradiction H4. reflexivity.
|
||||
rewrite H6 in H.
|
||||
|
||||
assert (b = b0).
|
||||
replace (hd ++ [b; b0; b1; b5; b4; b4; b5]
|
||||
++ [b5; b4; b4; b5; b1; b0; b] ++ tl)
|
||||
with (hd ++ [b; b0; b1; b5]
|
||||
++ [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl) in H.
|
||||
assert (exists x, firstn 2 [b; b0; b1; b5] = [x; x]).
|
||||
generalize H2.
|
||||
apply tm_step_factor4_1mod4 with (n' := n)
|
||||
(y := [b4; b4; b5; b5; b4; b4; b5; b1; b0; b] ++ tl). assumption.
|
||||
reflexivity. destruct H7. inversion H7. reflexivity. reflexivity.
|
||||
rewrite H7 in H.
|
||||
|
||||
assert ({b1=b5} + {~ b1=b5}). apply bool_dec. destruct H8. rewrite e in H.
|
||||
replace (hd ++ [b0; b0; b5; b5; b4; b4; b5]
|
||||
++ [b5; b4; b4; b5; b5; b0; b0] ++ tl)
|
||||
with ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4]
|
||||
++ [b5; b5; b4; b4] ++ [b5; b5; b0; b0] ++ tl) in H.
|
||||
assert (even (length ((hd ++ [b0; b0]) ++ [b5; b5; b4; b4])) = true).
|
||||
assert (0 < length ([b5; b5; b4; b4])). apply Nat.lt_0_succ.
|
||||
generalize H8. generalize H. apply tm_step_square_pos.
|
||||
rewrite app_length in H8. rewrite app_length in H8.
|
||||
rewrite <- Nat.add_assoc in H8. rewrite Nat.even_add in H8.
|
||||
rewrite <- Nat.negb_odd in H8.
|
||||
rewrite H1 in H8. inversion H8. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b1 = b4). destruct b1; destruct b4; destruct b5.
|
||||
reflexivity. reflexivity. contradiction n0. reflexivity.
|
||||
contradiction H4. reflexivity. contradiction H4. reflexivity.
|
||||
contradiction n0. reflexivity. reflexivity. reflexivity.
|
||||
rewrite H8 in H.
|
||||
|
||||
assert (b0 <> b4).
|
||||
replace (hd ++ [b0; b0; b4; b5; b4; b4; b5]
|
||||
++ [b5; b4; b4; b5; b4; b0; b0] ++ tl)
|
||||
with (hd ++ [b0] ++ [b0] ++ [b4]
|
||||
++ [b5;b4;b4;b5;b5; b4; b4; b5; b4; b0; b0] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b0; destruct b4.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. reflexivity.
|
||||
|
||||
assert (b0 = b5). destruct b0; destruct b4; destruct b5.
|
||||
reflexivity. contradiction H9. reflexivity. reflexivity.
|
||||
contradiction H4. reflexivity. contradiction H4. reflexivity.
|
||||
reflexivity. contradiction H9. reflexivity. reflexivity.
|
||||
rewrite H10 in H.
|
||||
|
||||
assert (b5 = negb b4). destruct b4; destruct b5.
|
||||
contradiction H4. reflexivity. reflexivity. reflexivity.
|
||||
contradiction H4. reflexivity. rewrite H11 in H.
|
||||
|
||||
exists b4. rewrite H3. rewrite H6. rewrite H7. rewrite H8. rewrite H10.
|
||||
rewrite H11. reflexivity.
|
||||
rewrite app_length in K. rewrite <- Nat.add_mod_idemp_l in K.
|
||||
rewrite H2 in K. inversion K. easy. reflexivity.
|
||||
inversion I.
|
||||
Qed.
|
||||
|
||||
Lemma tm_step_palindrome_8_destruct :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
|
|
@ -2104,6 +2232,8 @@ Lemma tm_step_palindrome_8_destruct :
|
|||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
|
||||
|
||||
(*
|
||||
assert (J: length a mod 4 = 0). rewrite I. reflexivity.
|
||||
assert (K := J).
|
||||
rewrite tm_step_palindromic_length_12_prefix
|
||||
|
|
@ -2111,6 +2241,7 @@ Proof.
|
|||
assert (L: even (length hd) = true).
|
||||
rewrite <- Nat.div_exact in K. rewrite K.
|
||||
rewrite Nat.even_mul. reflexivity. easy.
|
||||
*)
|
||||
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
destruct a. inversion I. destruct a. inversion I.
|
||||
|
|
@ -2121,116 +2252,31 @@ Proof.
|
|||
replace (rev [b; b0; b1; b2; b3; b4; b5; b6])
|
||||
with ([b6; b5; b4; b3; b2; b1; b0; b]) in H.
|
||||
|
||||
assert (b4 = b5).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b4; b5; b6]
|
||||
++ [b6; b5; b4; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1]) ++ [b2; b3; b4; b5]
|
||||
++ [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl) in H.
|
||||
assert (length (hd ++ [b; b0; b1]) mod 4 = 3).
|
||||
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K.
|
||||
reflexivity. easy.
|
||||
assert (exists x, skipn 2 [b2; b3; b4; b5] = [x; x]).
|
||||
generalize H0.
|
||||
apply tm_step_factor4_3mod4 with (n' := n)
|
||||
(y := [b6; b6; b5; b4; b3; b2; b1; b0; b] ++ tl). assumption.
|
||||
reflexivity. destruct H1. inversion H1. reflexivity.
|
||||
rewrite <- app_assoc. reflexivity. rewrite H0 in H.
|
||||
assert (exists x, [b0; b1; b2; b3; b4; b5; b6]
|
||||
= [negb x; negb x; x; negb x; x; x; negb x]).
|
||||
apply tm_step_palindrome_7_destruct
|
||||
with (n := n) (hd := hd ++ [b]) (tl := [b] ++ tl).
|
||||
rewrite <- app_assoc. assumption. reflexivity.
|
||||
|
||||
assert (b5 <> b6).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
|
||||
++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1; b2; b3]) ++ [b5] ++ [b5] ++ [b6]
|
||||
++ [b6; b5; b5; b3; b2;b1;b0;b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b5; destruct b6.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
||||
destruct H0. inversion H0. rewrite H2 in H. rewrite H3 in H.
|
||||
rewrite H4 in H. rewrite H5 in H. rewrite H6 in H. rewrite H7 in H.
|
||||
rewrite H8 in H.
|
||||
|
||||
assert (b5 <> b3).
|
||||
replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
|
||||
++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6])
|
||||
++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b5; destruct b3.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b3 = b6). destruct b3; destruct b5; destruct b6.
|
||||
contradiction H1. reflexivity. contradiction H2. reflexivity.
|
||||
reflexivity. contradiction H1. reflexivity.
|
||||
contradiction H1. reflexivity. reflexivity.
|
||||
contradiction H2. reflexivity. contradiction H1. reflexivity.
|
||||
rewrite H3 in H.
|
||||
|
||||
assert (b0 = b1).
|
||||
replace (hd ++ [b; b0; b1; b2; b6; b5; b5; b6]
|
||||
++ [b6; b5; b5; b6; b2; b1; b0; b] ++ tl)
|
||||
with ((hd ++ [b]) ++ [b0; b1; b2; b6]
|
||||
++ [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl) in H.
|
||||
assert (length (hd ++ [b]) mod 4 = 1).
|
||||
rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K.
|
||||
reflexivity. easy.
|
||||
assert (exists x, firstn 2 [b0; b1; b2; b6] = [x; x]).
|
||||
generalize H4.
|
||||
apply tm_step_factor4_1mod4 with (n' := n)
|
||||
(y := [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl). assumption.
|
||||
reflexivity. destruct H5. inversion H5. reflexivity.
|
||||
rewrite <- app_assoc. reflexivity. rewrite H4 in H.
|
||||
|
||||
assert ({b2=b6} + {~ b2=b6}). apply bool_dec. destruct H5. rewrite e in H.
|
||||
replace (hd ++ [b; b1; b1; b6; b6; b5; b5; b6]
|
||||
++ [b6; b5; b5; b6; b6; b1; b1; b] ++ tl)
|
||||
with ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5]
|
||||
++ [b6; b6; b5; b5] ++ [b6; b6; b1; b1; b] ++ tl) in H.
|
||||
assert (even (length ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5])) = true).
|
||||
assert (0 < length ([b6; b6; b5; b5])). apply Nat.lt_0_succ.
|
||||
generalize H5. generalize H. apply tm_step_square_pos.
|
||||
rewrite app_length in H5. rewrite app_length in H5.
|
||||
rewrite <- Nat.add_assoc in H5. rewrite Nat.even_add in H5.
|
||||
rewrite L in H5. inversion H5. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b2 = b5). destruct b2; destruct b6; destruct b5.
|
||||
reflexivity. contradiction n0. reflexivity. reflexivity.
|
||||
contradiction H1. reflexivity. contradiction H1. reflexivity.
|
||||
reflexivity. contradiction n0. reflexivity. reflexivity.
|
||||
rewrite H5 in H.
|
||||
|
||||
assert (b1 <> b5).
|
||||
replace (hd ++ [b; b1; b1; b5; b6; b5; b5; b6]
|
||||
++ [b6; b5; b5; b6; b5; b1; b1; b] ++ tl)
|
||||
with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b5]
|
||||
++ [b6;b5;b5;b6;b6; b5; b5; b6; b5; b1; b1; b] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. destruct b1; destruct b5.
|
||||
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
|
||||
|
||||
assert (b1 = b6). destruct b1; destruct b5; destruct b6.
|
||||
reflexivity. contradiction H6. reflexivity. reflexivity.
|
||||
contradiction H1. reflexivity. contradiction H1. reflexivity.
|
||||
reflexivity. contradiction H6. reflexivity. reflexivity.
|
||||
rewrite H7 in H.
|
||||
|
||||
assert ({b=b6} + {~ b=b6}). apply bool_dec. destruct H8. rewrite e in H.
|
||||
replace (hd ++ [b6; b6; b6; b5; b6; b5; b5; b6]
|
||||
++ [b6; b5; b5; b6; b5; b6; b6; b6] ++ tl)
|
||||
with (hd ++ [b6] ++ [b6] ++ [b6]
|
||||
++ [b5; b6;b5;b5;b6;b6; b5; b5; b6; b5; b6; b6; b6] ++ tl) in H.
|
||||
assert ({b=x} + {~ b=x}). apply bool_dec. destruct H1.
|
||||
exists x. rewrite e. reflexivity.
|
||||
assert (b = negb x). destruct b; destruct x.
|
||||
contradiction n0. reflexivity. reflexivity. reflexivity.
|
||||
contradiction n0. reflexivity.
|
||||
rewrite H1 in H.
|
||||
replace (hd ++ [negb x; negb x; negb x; x; negb x; x; x; negb x] ++
|
||||
[negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl)
|
||||
with (hd ++ [negb x] ++ [negb x] ++ [negb x]
|
||||
++ [x; negb x; x; x; negb x;
|
||||
negb x; x; x; negb x; x; negb x; negb x; negb x] ++ tl) in H.
|
||||
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
||||
apply Nat.lt_0_1. reflexivity.
|
||||
|
||||
assert (b = b5). destruct b; destruct b5; destruct b6.
|
||||
reflexivity. reflexivity. contradiction n1. reflexivity.
|
||||
contradiction H1. reflexivity. contradiction H1. reflexivity.
|
||||
contradiction n1. reflexivity. reflexivity. reflexivity.
|
||||
rewrite H8 in H.
|
||||
|
||||
assert (b6 = negb b5). destruct b5; destruct b6.
|
||||
contradiction H1. reflexivity. reflexivity. reflexivity.
|
||||
contradiction H1. reflexivity. rewrite H9 in H.
|
||||
|
||||
exists b5. rewrite H4. rewrite H3. rewrite H8. rewrite H7. rewrite H5.
|
||||
rewrite H0. rewrite H9. reflexivity.
|
||||
reflexivity. inversion I. assumption. rewrite I.
|
||||
rewrite <- Nat.le_succ_l. apply Nat.le_succ_diag_r.
|
||||
reflexivity. inversion I.
|
||||
Qed.
|
||||
|
||||
|
||||
|
|
@ -2254,6 +2300,21 @@ Proof.
|
|||
generalize I. generalize H. apply tm_step_palindrome_8_destruct.
|
||||
destruct M as [x M].
|
||||
|
||||
assert (N: length (hd ++ a) mod 4 = 0).
|
||||
rewrite app_length. rewrite Nat.add_mod.
|
||||
rewrite J. rewrite K. reflexivity. easy.
|
||||
|
||||
assert (O: length (hd++a) mod 8 = 0 \/ length (hd++a) mod 8 = 4).
|
||||
assert (length (hd ++ a) mod (4*2)
|
||||
= (length (hd ++ a) mod 4 + 4 * (length (hd ++ a) / 4 mod 2))).
|
||||
apply Nat.mod_mul_r. easy. easy.
|
||||
rewrite N in H0. rewrite <- Nat.bit0_mod in H0.
|
||||
replace (4*2) with 8 in H0. rewrite Nat.add_0_l in H0.
|
||||
destruct (Nat.testbit (length (hd ++ a) / 4)).
|
||||
right. apply H0. left. apply H0. reflexivity.
|
||||
|
||||
destruct O as [O | O]. assumption.
|
||||
|
||||
|
||||
|
||||
(*
|
||||
|
|
|
|||
Loading…
Reference in New Issue