Update
This commit is contained in:
parent
c7bad77004
commit
24b8b2434d
|
@ -1357,6 +1357,30 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem tm_step_palindromic_length_12_n :
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
|
-> length a > 6
|
||||||
|
-> 1 < n.
|
||||||
|
Proof.
|
||||||
|
intros n hd a tl. intros H W.
|
||||||
|
|
||||||
|
assert (length (tm_step n) <= length (tm_step n)).
|
||||||
|
apply Nat.le_refl. rewrite H in H0 at 1.
|
||||||
|
rewrite app_length in H0. rewrite app_length in H0.
|
||||||
|
rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0.
|
||||||
|
rewrite <- Nat.add_0_r in H0. apply Nat.le_le_add_le in H0.
|
||||||
|
rewrite tm_size_power2 in H0. destruct n. destruct a.
|
||||||
|
inversion W. destruct a. inversion W. inversion H2.
|
||||||
|
destruct a. inversion W. inversion H2. inversion H4.
|
||||||
|
inversion H0. inversion H2. destruct a. inversion W.
|
||||||
|
destruct a. inversion W. inversion H2. destruct a. inversion W.
|
||||||
|
inversion H2. inversion H4. destruct n. inversion H0. inversion H2.
|
||||||
|
inversion H4. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||||
|
apply le_0_n.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem tm_step_palindromic_length_12_prefix :
|
Theorem tm_step_palindromic_length_12_prefix :
|
||||||
forall (n : nat) (hd a tl : list bool),
|
forall (n : nat) (hd a tl : list bool),
|
||||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
|
@ -1373,9 +1397,20 @@ Proof.
|
||||||
assumption. easy. assumption.
|
assumption. easy. assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Theorem tm_step_palindromic_length_12_prefix2 :
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
|
-> length a > 6
|
||||||
|
-> length a mod 4 = 0 -> length tl mod 4 = 0.
|
||||||
|
Proof.
|
||||||
|
intros n hd a tl. intros H I J.
|
||||||
|
assert (K: length hd mod 4 = 0).
|
||||||
|
generalize J. generalize I. generalize H.
|
||||||
|
apply tm_step_palindromic_length_12_prefix.
|
||||||
|
assert (L: length (hd ++ a ++ rev a ++ tl) mod 4 = 0).
|
||||||
|
rewrite <- H. rewrite tm_size_power2.
|
||||||
|
|
||||||
|
Admitted.
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_palindromic_even_morphism1 :
|
Lemma tm_step_palindromic_even_morphism1 :
|
||||||
forall (n : nat) (hd a tl : list bool),
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
@ -1484,7 +1519,9 @@ Lemma tm_step_palindromic_even_morphism2 :
|
||||||
tm_step n = hd ++ a ++ (rev a) ++ tl
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
-> length a > 6
|
-> length a > 6
|
||||||
-> (length a) mod 4 = 0
|
-> (length a) mod 4 = 0
|
||||||
-> 11 = 42.
|
-> hd = tm_morphism (tm_morphism (firstn (length hd / 4)
|
||||||
|
(tm_step (pred (pred n)))))
|
||||||
|
/\ 11 = 42.
|
||||||
Proof.
|
Proof.
|
||||||
intros n hd a tl. intros H W J0.
|
intros n hd a tl. intros H W J0.
|
||||||
|
|
||||||
|
@ -1493,19 +1530,9 @@ Proof.
|
||||||
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
|
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
|
||||||
assumption.
|
assumption.
|
||||||
|
|
||||||
assert (V: 1 < n). assert (length (tm_step n) <= length (tm_step n)).
|
assert (V: 1 < n). generalize W. generalize H.
|
||||||
apply Nat.le_refl. rewrite H in H0 at 1.
|
apply tm_step_palindromic_length_12_n.
|
||||||
rewrite app_length in H0. rewrite app_length in H0.
|
destruct n. inversion V.
|
||||||
rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0.
|
|
||||||
rewrite <- Nat.add_0_r in H0. apply Nat.le_le_add_le in H0.
|
|
||||||
rewrite tm_size_power2 in H0. destruct n. destruct a.
|
|
||||||
inversion W. destruct a. inversion W. inversion H2.
|
|
||||||
destruct a. inversion W. inversion H2. inversion H4.
|
|
||||||
inversion H0. inversion H2. destruct a. inversion W.
|
|
||||||
destruct a. inversion W. inversion H2. destruct a. inversion W.
|
|
||||||
inversion H2. inversion H4. destruct n. inversion H0. inversion H2.
|
|
||||||
inversion H4. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
|
||||||
apply le_0_n. destruct n. inversion V.
|
|
||||||
|
|
||||||
assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
|
assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
|
||||||
generalize H. apply tm_step_palindromic_length_12_prefix.
|
generalize H. apply tm_step_palindromic_length_12_prefix.
|
||||||
|
@ -1704,6 +1731,30 @@ Proof.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
split.
|
||||||
|
|
||||||
|
rewrite <- pred_Sn. rewrite <- pred_Sn.
|
||||||
|
rewrite H4 at 1. fold hd'. rewrite H4'. unfold hd'.
|
||||||
|
rewrite firstn_length_le. rewrite Nat.div2_div. rewrite Nat.div2_div.
|
||||||
|
rewrite Nat.div_div. reflexivity. easy. easy.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
assert (hd = hd). reflexivity. rewrite H4 in H12 at 2. fold hd' in H12.
|
||||||
|
rewrite H4' in H12. unfold hd' in H12.
|
||||||
|
rewrite firstn_length_le in H12.
|
||||||
|
rewrite Nat.div2_div in H12.
|
||||||
|
rewrite Nat.div2_div in H12. rewrite Nat.div_div in H12.
|
||||||
|
replace (2*2) with 4 in H12.
|
||||||
|
|
||||||
|
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue