Update
This commit is contained in:
Thomas Baruchel
parent
36b7d26757
commit
837884e808
|
|
@ -1893,6 +1893,292 @@ Qed.
|
|||
|
||||
|
||||
|
||||
Lemma xxx :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> length a = 2^(Nat.double m)
|
||||
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
||||
\/ 64 <= length a.
|
||||
Proof.
|
||||
intros m n hd a tl. intros H I J.
|
||||
|
||||
destruct m. rewrite J in I. inversion I. inversion H1.
|
||||
destruct m. rewrite J in I. inversion I. inversion H1.
|
||||
inversion H3. inversion H5. inversion H7.
|
||||
|
||||
destruct m. left.
|
||||
|
||||
assert (W: length a mod 4 = 0). rewrite J. reflexivity.
|
||||
|
||||
assert (
|
||||
hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
||||
(tm_step (pred (pred n)))))
|
||||
/\ a = tm_morphism (tm_morphism
|
||||
(firstn (length a / 4) (skipn (length hd / 4)
|
||||
(tm_step (pred (pred n))))))
|
||||
/\ tl = tm_morphism (tm_morphism
|
||||
(skipn (length hd / 4 + Nat.div2 (length a))
|
||||
(tm_step (pred (pred n)))))).
|
||||
generalize W. generalize I. generalize H.
|
||||
apply tm_step_palindromic_even_morphism2.
|
||||
destruct H0 as [K H0]. destruct H0 as [L M].
|
||||
|
||||
assert (V: 3 < n). generalize I. generalize H.
|
||||
apply tm_step_palindromic_length_12_n.
|
||||
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
||||
|
||||
rewrite K in H. rewrite L in H. rewrite M in H.
|
||||
rewrite tm_morphism_twice_rev in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H.
|
||||
rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
|
||||
rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
|
||||
|
||||
pose (hd' := (firstn (length hd / 4) (tm_step n))).
|
||||
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
|
||||
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
|
||||
fold hd' in H. fold a' in H. fold tl' in H.
|
||||
|
||||
rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K.
|
||||
rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
|
||||
fold hd' in K. fold a' in L.
|
||||
assert (N: length a = length a). reflexivity. rewrite L in N at 2.
|
||||
rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
|
||||
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
||||
assert (O: length hd = length hd). reflexivity. rewrite K in O at 2.
|
||||
rewrite tm_morphism_length in O. rewrite tm_morphism_length in O.
|
||||
rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O.
|
||||
|
||||
replace (2^ pred (Nat.double 2)) with (4*2).
|
||||
rewrite app_length. rewrite N. rewrite O.
|
||||
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
||||
rewrite Nat.mul_eq_0. right. rewrite <- app_length.
|
||||
|
||||
assert (U: even (length (hd' ++ a')) = true).
|
||||
assert (0 < length a').
|
||||
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
||||
rewrite N in I.
|
||||
rewrite <- Nat.mul_1_r in I at 1.
|
||||
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
||||
apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ.
|
||||
generalize H0. generalize H. apply tm_step_palindromic_even_center.
|
||||
|
||||
replace (length (hd' ++ a'))
|
||||
with (2 * Nat.div2 (length (hd' ++ a'))
|
||||
+ Nat.b2n (Nat.odd (length (hd' ++ a')))).
|
||||
rewrite <- Nat.negb_even. rewrite U. rewrite Nat.add_0_r.
|
||||
rewrite Nat.mul_mod. reflexivity. easy. symmetry. apply Nat.div2_odd.
|
||||
easy. easy. reflexivity. reflexivity. reflexivity.
|
||||
|
||||
right. rewrite J. rewrite Nat.double_S. rewrite Nat.double_S.
|
||||
rewrite Nat.double_S. rewrite Nat.pow_succ_r.
|
||||
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
||||
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
||||
rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc.
|
||||
rewrite Nat.mul_assoc. rewrite Nat.mul_assoc.
|
||||
rewrite Nat.mul_assoc. rewrite Nat.mul_assoc.
|
||||
|
||||
replace (2*2*2*2*2*2) with 64. rewrite <- Nat.mul_1_r at 1.
|
||||
rewrite <- Nat.mul_le_mono_pos_l. rewrite Nat.le_succ_l.
|
||||
rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
|
||||
apply Nat.lt_0_succ. reflexivity.
|
||||
apply le_0_n. apply le_0_n. apply le_0_n.
|
||||
apply le_0_n. apply le_0_n. apply le_0_n.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
destruct m. left.
|
||||
|
||||
assert (K: length a mod 4 = 0). rewrite J. reflexivity.
|
||||
assert (L: length hd mod 4 = 0).
|
||||
generalize K. generalize I. generalize H.
|
||||
apply tm_step_palindromic_length_12_prefix.
|
||||
|
||||
assert (M: hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
||||
(tm_step (pred (pred n)))))
|
||||
/\ a = tm_morphism (tm_morphism
|
||||
(firstn (length a / 4) (skipn (length hd / 4)
|
||||
(tm_step (pred (pred n))))))
|
||||
/\ tl = tm_morphism (tm_morphism
|
||||
(skipn (length hd / 4 + Nat.div2 (length a))
|
||||
(tm_step (pred (pred n)))))).
|
||||
generalize K. generalize I. generalize H.
|
||||
apply tm_step_palindromic_even_morphism2.
|
||||
|
||||
destruct M as [N O]. destruct O as [O P].
|
||||
rewrite N in H. rewrite O in H. rewrite P in H.
|
||||
(*
|
||||
rewrite tm_morphism_twice_rev in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
*)
|
||||
|
||||
pose (hd' := (firstn (length hd / 4) (tm_step (pred (pred n))))).
|
||||
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step (pred (pred n)))))).
|
||||
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step (pred (pred n))))).
|
||||
fold hd' in H. fold a' in H. fold tl' in H.
|
||||
|
||||
|
||||
Lemma tm_step_palindromic_power2_even :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> length a = 2^(Nat.double m)
|
||||
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
||||
<-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0.
|
||||
Proof.
|
||||
intros m n hd a tl. intros H I J.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma xxx :
|
||||
forall m : nat,
|
||||
(forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> length a = 2^(Nat.double m)
|
||||
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0)
|
||||
-> (forall (n' : nat) (hd' a' tl' : list bool),
|
||||
tm_step n' = hd' ++ a' ++ (rev a') ++ tl'
|
||||
-> 6 < length a'
|
||||
-> length a' = 2^(Nat.double (S m))
|
||||
-> length (hd' ++ a') mod (2 ^ (pred (Nat.double (S m)))) = 0).
|
||||
Proof.
|
||||
intro m. intro IH.
|
||||
intros n hd a tl. intros H I J.
|
||||
rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl).
|
||||
rewrite <- pred_Sn.
|
||||
|
||||
destruct m. rewrite J in I. inversion I. inversion H1.
|
||||
inversion H3. inversion H5. inversion H7.
|
||||
|
||||
assert (W: (length a) mod 4 = 0).
|
||||
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
||||
rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
|
||||
rewrite Nat.mul_assoc in J.
|
||||
replace (2*2) with 4 in J. rewrite J.
|
||||
rewrite <- Nat.mul_mod_idemp_l. reflexivity.
|
||||
easy. reflexivity. apply le_0_n. apply le_0_n.
|
||||
|
||||
assert (
|
||||
hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
||||
(tm_step (pred (pred n)))))
|
||||
/\ a = tm_morphism (tm_morphism
|
||||
(firstn (length a / 4) (skipn (length hd / 4)
|
||||
(tm_step (pred (pred n))))))
|
||||
/\ tl = tm_morphism (tm_morphism
|
||||
(skipn (length hd / 4 + Nat.div2 (length a))
|
||||
(tm_step (pred (pred n)))))).
|
||||
generalize W. generalize I. generalize H.
|
||||
apply tm_step_palindromic_even_morphism2.
|
||||
destruct H0 as [K H0]. destruct H0 as [L M].
|
||||
|
||||
assert (V: 3 < n). generalize I. generalize H.
|
||||
apply tm_step_palindromic_length_12_n.
|
||||
destruct n. inversion V. destruct n. inversion V. inversion H1.
|
||||
|
||||
rewrite K in H. rewrite L in H. rewrite M in H.
|
||||
rewrite tm_morphism_twice_rev in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
|
||||
rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H.
|
||||
rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
|
||||
rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
|
||||
|
||||
pose (hd' := (firstn (length hd / 4) (tm_step n))).
|
||||
pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
|
||||
pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
|
||||
fold hd' in H. fold a' in H. fold tl' in H.
|
||||
|
||||
rewrite Nat.pred_succ in K. rewrite Nat.pred_succ in K.
|
||||
rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
|
||||
fold hd' in K. fold a' in L.
|
||||
assert (N: length a = length a). reflexivity. rewrite L in N at 2.
|
||||
rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
|
||||
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
|
||||
assert (O: length hd = length hd). reflexivity. rewrite K in O at 2.
|
||||
rewrite tm_morphism_length in O. rewrite tm_morphism_length in O.
|
||||
rewrite Nat.mul_assoc in O. replace (2*2) with 4 in O.
|
||||
|
||||
rewrite app_length. rewrite N. rewrite O.
|
||||
rewrite <- Nat.mul_add_distr_l. rewrite <- app_length.
|
||||
rewrite Nat.mul_comm. rewrite Nat.div_mul.
|
||||
apply IH with (n := n) (tl := tl'). assumption.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
replace (2^ pred (Nat.double 2)) with (4*2).
|
||||
rewrite app_length. rewrite N. rewrite O.
|
||||
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
||||
rewrite Nat.mul_eq_0. right. rewrite <- app_length.
|
||||
|
||||
assert (U: even (length (hd' ++ a')) = true).
|
||||
assert (0 < length a').
|
||||
apply Nat.lt_succ_l in I. apply Nat.lt_succ_l in I.
|
||||
rewrite N in I.
|
||||
rewrite <- Nat.mul_1_r in I at 1.
|
||||
rewrite <- Nat.mul_lt_mono_pos_l in I.
|
||||
apply Nat.lt_succ_l in I. assumption. apply Nat.lt_0_succ.
|
||||
generalize H0. generalize H. apply tm_step_palindromic_even_center.
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma tm_step_palindromic_even_morphism2 :
|
||||
forall (n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> (length a) mod 4 = 0
|
||||
-> hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
||||
(tm_step (pred (pred n)))))
|
||||
/\ a = tm_morphism (tm_morphism
|
||||
(firstn (length a / 4) (skipn (length hd / 4)
|
||||
(tm_step (pred (pred n))))))
|
||||
/\ tl = tm_morphism (tm_morphism
|
||||
(skipn (length hd / 4 + Nat.div2 (length a))
|
||||
(tm_step (pred (pred n))))).
|
||||
|
||||
|
||||
rewrite Nat.double_S.
|
||||
replace (pred (S (S (Nat.double m)))) with (S (S (pred (Nat.double m)))).
|
||||
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc.
|
||||
replace (2*2) with 4.
|
||||
|
||||
Lemma tm_step_palindromic_power2_even :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> length a = 2^(Nat.double m)
|
||||
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
||||
<-> (length (hd ++ a) / 4) mod (2^(pred (Nat.double (pred m)))) = 0.
|
||||
|
||||
|
||||
|
||||
Lemma tm_step_palindromic_power2_even :
|
||||
forall (m n : nat) (hd a tl : list bool),
|
||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||
-> 6 < length a
|
||||
-> length a = 2^(Nat.double m)
|
||||
-> length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Lemma xxx :
|
||||
forall (m n k : nat) (hd a tl : list bool),
|
||||
|
|
@ -2048,6 +2334,7 @@ Proof.
|
|||
rewrite app_length. rewrite N. rewrite O.
|
||||
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
||||
rewrite Nat.mul_eq_0. right. rewrite <- app_length.
|
||||
apply IHm.
|
||||
|
||||
|
||||
Lemma tm_step_palindromic_power2_even :
|
||||
|
|
|
|||
Loading…
Reference in New Issue