Update
This commit is contained in:
parent
ab50cd2b28
commit
a59cfa8944
|
@ -2,7 +2,10 @@
|
||||||
|
|
||||||
TODO
|
TODO
|
||||||
|
|
||||||
tm_step_rev
|
Theorem tm_step_rev : forall (n : nat),
|
||||||
|
Theorem tm_step_palindromic_full : forall (n : nat),
|
||||||
|
Theorem tm_step_palindromic_full_even : forall (n : nat),
|
||||||
|
Theorem tm_step_palindromic_length_12 :
|
||||||
*)
|
*)
|
||||||
|
|
||||||
Require Import thue_morse.
|
Require Import thue_morse.
|
||||||
|
@ -1248,7 +1251,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Lemma tm_step_palindromic_length_12 :
|
Theorem tm_step_palindromic_length_12 :
|
||||||
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
|
||||||
-> 6 < length a
|
-> 6 < length a
|
||||||
|
@ -1354,6 +1357,61 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem tm_step_palindromic_length_12_prefix :
|
||||||
|
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 hd mod 4 = 0.
|
||||||
|
Proof.
|
||||||
|
intros n hd a tl. intros H I. split; intro J;
|
||||||
|
apply tm_step_palindromic_length_12 with (n := n) (hd := hd) (tl := tl) in I.
|
||||||
|
rewrite app_length in I.
|
||||||
|
rewrite <- Nat.add_mod_idemp_r in I. rewrite J in I. rewrite Nat.add_0_r in I.
|
||||||
|
assumption. easy. assumption.
|
||||||
|
rewrite app_length in I.
|
||||||
|
rewrite <- Nat.add_mod_idemp_l in I. rewrite J in I. rewrite Nat.add_0_l in I.
|
||||||
|
assumption. easy. assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Lemma tm_step_palindromic_even_morphism1 :
|
||||||
|
forall (n : nat) (hd a tl : list bool),
|
||||||
|
tm_step n = hd ++ a ++ (rev a) ++ tl
|
||||||
|
-> 0 < length a
|
||||||
|
-> even (length a) = true
|
||||||
|
-> 11= 42.
|
||||||
|
Proof.
|
||||||
|
intros n hd a tl. intros H I J.
|
||||||
|
destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
|
||||||
|
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. simpl in H0.
|
||||||
|
apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0.
|
||||||
|
rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0.
|
||||||
|
assert (K: 1 <= length a + (length tl + length hd)).
|
||||||
|
rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption.
|
||||||
|
rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0.
|
||||||
|
rewrite H0 in I. inversion I.
|
||||||
|
|
||||||
|
assert (even (length (hd ++ a)) = true). generalize I. generalize H.
|
||||||
|
apply tm_step_palindromic_even_center.
|
||||||
|
|
||||||
|
assert (even (length hd) = true). rewrite app_length in H0.
|
||||||
|
rewrite Nat.even_add in H0. rewrite J in H0.
|
||||||
|
destruct (even (length hd)). reflexivity. inversion H0.
|
||||||
|
|
||||||
|
rewrite <- tm_step_lemma in H.
|
||||||
|
assert (hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
|
||||||
|
generalize H1. generalize H. apply tm_morphism_app2.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue