Update
This commit is contained in:
parent
54cdff7f66
commit
4fcaba8c73
@ -1650,3 +1650,54 @@ Proof.
|
|||||||
generalize H1. generalize H0. apply IHn.
|
generalize H1. generalize H0. apply IHn.
|
||||||
- assumption.
|
- assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
(*
|
||||||
|
Theorem tm_step_repeating_patterns_no_square :
|
||||||
|
forall (n m : nat) (hd a b tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ b ++ tl -> length a = 2^m
|
||||||
|
-> (forall k, length hd = k * 2 ^ S m -> a <> b).
|
||||||
|
Proof.
|
||||||
|
intros n m hd a b tl. intros H I.
|
||||||
|
induction n.
|
||||||
|
- assert (m = 0).
|
||||||
|
destruct m. reflexivity.
|
||||||
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
||||||
|
rewrite H in H0 at 2. rewrite app_length in H0. rewrite Nat.add_comm in H0.
|
||||||
|
rewrite app_length in H0. rewrite <- Nat.add_assoc in H0.
|
||||||
|
rewrite I in H0. rewrite Nat.pow_succ_r in H0. symmetry in H0.
|
||||||
|
apply Nat.eq_add_1 in H0. destruct H0; destruct H0.
|
||||||
|
apply Nat.mul_eq_1 in H0. destruct H0. inversion H0.
|
||||||
|
apply Nat.mul_eq_0 in H0. destruct H0. inversion H0.
|
||||||
|
apply Nat.pow_nonzero in H0. contradiction H0. easy. apply le_0_n.
|
||||||
|
intro k. intro J. rewrite H0 in J. rewrite Nat.pow_1_r in J.
|
||||||
|
assert (k = 0).
|
||||||
|
assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
|
||||||
|
rewrite H in H1 at 2. rewrite app_length in H1. rewrite J in H1.
|
||||||
|
symmetry in H1. apply Nat.eq_add_1 in H1. destruct H1; destruct H1.
|
||||||
|
apply Nat.mul_eq_1 in H1. destruct H1. inversion H3.
|
||||||
|
apply Nat.mul_eq_0 in H1. destruct H1. assumption. inversion H1.
|
||||||
|
rewrite H1 in J. rewrite Nat.mul_0_l in J. rewrite length_zero_iff_nil in J.
|
||||||
|
assert ({a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
|
||||||
|
destruct H2. rewrite <- e in H.
|
||||||
|
|
||||||
|
assert (0 < length a). rewrite I. rewrite H0. apply Nat.lt_0_1.
|
||||||
|
|
||||||
|
assert (hd <> nil). generalize H2. generalize H.
|
||||||
|
apply tm_step_square_prefix_not_nil. rewrite J in H3.
|
||||||
|
contradiction H3. reflexivity. assumption.
|
||||||
|
-
|
||||||
|
|
||||||
|
Reformulation:
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ a ++ tl
|
||||||
|
-> 0 < length a
|
||||||
|
-> (length hd) mod (length (a ++ a)) <> 0.
|
||||||
|
PB : manque l'idée d'une puissance de 2 !
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Theorem tm_step_square_prefix_not_nil :
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil.
|
||||||
|
*)
|
||||||
|
@ -1819,6 +1819,80 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_step_palindromic_power2_even :
|
||||||
|
forall (m n k : 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 k 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.
|
||||||
|
|
||||||
|
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 (length (hd ++ a) mod 4 = 0).
|
||||||
|
assert (W' := W).
|
||||||
|
rewrite tm_step_palindromic_length_12_prefix
|
||||||
|
with (hd := hd) (n := n) (tl := tl) in W'.
|
||||||
|
rewrite app_length. rewrite Nat.add_mod.
|
||||||
|
rewrite W. rewrite W'. reflexivity. easy. assumption. 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 (pred (Nat.double (pred (S (S m)))))))
|
||||||
|
with (pred (Nat.double (S (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.
|
||||||
|
rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity.
|
||||||
|
rewrite Nat.neq_0_lt_0. rewrite Nat.double_S.
|
||||||
|
apply Nat.lt_0_succ. 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 (pred (Nat.double (pred (S (S m)))))))
|
||||||
|
with (pred (Nat.double (S (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.
|
||||||
|
rewrite <- pred_Sn. rewrite Nat.succ_pred. reflexivity.
|
||||||
|
rewrite Nat.neq_0_lt_0. rewrite Nat.double_S.
|
||||||
|
apply Nat.lt_0_succ. apply le_0_n. apply le_0_n.
|
||||||
|
reflexivity.
|
||||||
|
|
||||||
|
apply Nat.pow_nonzero. easy. easy. easy.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Lemma xxx :
|
Lemma xxx :
|
||||||
forall (m n k : nat) (hd a tl : list bool),
|
forall (m n k : nat) (hd a tl : list bool),
|
||||||
@ -1912,33 +1986,64 @@ Proof.
|
|||||||
with (S (S (pred (Nat.double (S (S m)))))).
|
with (S (S (pred (Nat.double (S (S m)))))).
|
||||||
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
|
||||||
rewrite Nat.mul_assoc. replace (2*2) with 4.
|
rewrite Nat.mul_assoc. replace (2*2) with 4.
|
||||||
|
|
||||||
|
rewrite Nat.mod_mul_r.
|
||||||
|
assert (length (hd ++ a) mod 4 = 0).
|
||||||
|
assert (length hd mod 4 = 0). rewrite O. rewrite Nat.mul_comm.
|
||||||
|
rewrite Nat.mod_mul. reflexivity. easy.
|
||||||
|
rewrite app_length. rewrite Nat.add_mod.
|
||||||
|
rewrite H0. rewrite W. reflexivity. easy. rewrite H0.
|
||||||
|
rewrite Nat.add_0_l. rewrite Nat.mul_eq_0. right.
|
||||||
|
|
||||||
|
|
||||||
|
Nat.mod_mul_r:
|
||||||
|
forall a b c : nat,
|
||||||
|
b <> 0 -> c <> 0 -> a mod (b * c) = a mod b + b * ((a / b) mod c)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
rewrite Nat.mod_mul_r.
|
||||||
|
assert (length (hd ++ a) mod 4 = 0).
|
||||||
|
assert (length hd mod 4 = 0). rewrite O. rewrite Nat.mul_comm.
|
||||||
|
rewrite Nat.mod_mul. reflexivity. easy.
|
||||||
|
rewrite app_length. rewrite Nat.add_mod.
|
||||||
|
rewrite H0. rewrite W. reflexivity. easy. rewrite H0.
|
||||||
|
rewrite Nat.add_0_l. rewrite Nat.mul_eq_0. right.
|
||||||
|
|
||||||
|
|
||||||
|
Nat.mod_mul_r:
|
||||||
|
forall a b c : nat,
|
||||||
|
b <> 0 -> c <> 0 -> a mod (b * c) = a mod b + b * ((a / b) mod c)
|
||||||
|
|
||||||
|
Theorem tm_step_palindromic_length_12_prefix :
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
|
-> 6 < length a
|
||||||
|
-> length a mod 4 = 0 <-> length hd mod 4 = 0.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
rewrite app_length. rewrite N. rewrite O.
|
rewrite app_length. rewrite N. rewrite O.
|
||||||
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
rewrite <- Nat.mul_add_distr_l. rewrite Nat.mul_mod_distr_l.
|
||||||
apply Nat.mul_eq_0. right. rewrite <- app_length.
|
apply Nat.mul_eq_0. right. rewrite <- app_length.
|
||||||
|
apply IHm with (tl := tl').
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
m, n, k : nat
|
Theorem tm_step_palindromic_length_12_prefix :
|
||||||
hd, a, tl : list bool
|
forall (n : nat) (hd a tl : list bool),
|
||||||
hd' := firstn (length hd / 4) (tm_step n) : list bool
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
a' := firstn (length a / 4) (skipn (length hd / 4) (tm_step n)) : list bool
|
-> 6 < length a
|
||||||
tl' := skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n) : list bool
|
-> length a mod 4 = 0 <-> length hd mod 4 = 0.
|
||||||
H : tm_step n = hd' ++ a' ++ rev a' ++ tl'
|
|
||||||
I : 6 < length a
|
|
||||||
J : length a = 2 ^ Nat.double (S (S m))
|
|
||||||
W : length a mod 4 = 0
|
|
||||||
K : hd = tm_morphism (tm_morphism hd')
|
unfold hd' at 2.
|
||||||
L : a = tm_morphism (tm_morphism a')
|
|
||||||
M : tl =
|
|
||||||
tm_morphism
|
|
||||||
(tm_morphism
|
|
||||||
(skipn (length hd / 4 + Nat.div2 (length a))
|
|
||||||
(tm_step (pred (pred (S (S n)))))))
|
|
||||||
V : 3 < S (S n)
|
|
||||||
N : length a = 4 * length a'
|
|
||||||
O : length hd = 4 * length hd'
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user