Update
This commit is contained in:
parent
98131965ff
commit
7fc5c18623
@ -2479,43 +2479,62 @@ Proof.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma tm_step_palindrome_8_mod8 :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
Lemma tm_step_palindromic_power2_odd_alpha :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> length a = 8
|
||||
-> length (hd ++ a) mod 8 = 0.
|
||||
-> 6 < length a
|
||||
-> length a = 2^(S (Nat.double m))
|
||||
-> length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0
|
||||
<-> (length (hd ++ a) / 4) mod (2^(S (Nat.double (pred m)))) = 0.
|
||||
Proof.
|
||||
intros n hd a tl. intros H I.
|
||||
intros m n hd a tl. intros H I J.
|
||||
|
||||
assert (J: length a mod 4 = 0). rewrite I. reflexivity.
|
||||
assert (K := J).
|
||||
rewrite tm_step_palindromic_length_12_prefix
|
||||
with (n := n) (hd := hd) (tl := tl) in K.
|
||||
assert (L: even (length hd) = true).
|
||||
rewrite <- Nat.div_exact in K. rewrite K.
|
||||
rewrite Nat.even_mul. reflexivity. easy.
|
||||
destruct m. rewrite J in I. inversion I. inversion H1. inversion H3.
|
||||
|
||||
assert (M: exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x]).
|
||||
generalize I. generalize H. apply tm_step_palindrome_8_destruct.
|
||||
destruct M as [x M].
|
||||
assert (length (hd ++ a) mod 4 = 0).
|
||||
apply tm_step_palindromic_length_12 with (n := n) (tl := tl); assumption.
|
||||
|
||||
assert (N: length (hd ++ a) mod 4 = 0).
|
||||
rewrite app_length. rewrite Nat.add_mod.
|
||||
rewrite J. rewrite K. reflexivity. easy.
|
||||
assert (length (hd ++ a) mod 8 = 0).
|
||||
apply tm_step_palindrome_mod8 with (n := n) (tl := tl); assumption.
|
||||
|
||||
split.
|
||||
- intro P.
|
||||
rewrite <- Nat.mul_cancel_l with (p := 4).
|
||||
rewrite <- Nat.mul_mod_distr_l.
|
||||
replace 4 with (2*2) at 3. rewrite <- Nat.mul_assoc.
|
||||
rewrite <- Nat.pow_succ_r. rewrite <- Nat.pow_succ_r.
|
||||
|
||||
replace (S (S (S (Nat.double (pred (S m))))))
|
||||
with (S (Nat.double (S m))).
|
||||
replace (4 * (length (hd ++ a) / 4))
|
||||
with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4).
|
||||
rewrite <- Nat.div_mod_eq. assumption.
|
||||
rewrite H0. rewrite Nat.add_0_r. reflexivity.
|
||||
|
||||
rewrite <- pred_Sn. rewrite Nat.double_S. reflexivity.
|
||||
apply le_0_n. apply le_0_n. reflexivity.
|
||||
|
||||
apply Nat.pow_nonzero. easy. easy. easy.
|
||||
- intro P.
|
||||
rewrite <- Nat.mul_cancel_l with (p := 4) in P.
|
||||
rewrite <- Nat.mul_mod_distr_l in P.
|
||||
replace 4 with (2*2) in P at 3. rewrite <- Nat.mul_assoc in P.
|
||||
rewrite <- Nat.pow_succ_r in P. rewrite <- Nat.pow_succ_r in P.
|
||||
|
||||
replace (S (S (S (Nat.double (pred (S m))))))
|
||||
with (S (Nat.double (S m))) in P.
|
||||
replace (4 * (length (hd ++ a) / 4))
|
||||
with (4 * (length (hd ++ a) / 4) + length (hd ++ a) mod 4) in P.
|
||||
rewrite <- Nat.div_mod_eq in P. assumption.
|
||||
rewrite H0. rewrite Nat.add_0_r. reflexivity.
|
||||
|
||||
rewrite <- pred_Sn. rewrite Nat.double_S. reflexivity.
|
||||
apply le_0_n. apply le_0_n. reflexivity.
|
||||
|
||||
apply Nat.pow_nonzero. easy. easy. easy.
|
||||
Qed.
|
||||
|
||||
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
Block a user