baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-02-01 18:41:16 +01:00
parent 837884e808
commit 9031f3b839
1 changed files with 119 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
src/thue_morse3.v
View File

@ -1892,14 +1892,13 @@ Proof.
Qed.
Lemma xxx :
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
\/ 64 <= length a.
\/ 2^6 <= length a.
Proof.
intros m n hd a tl. intros H I J.
@ -1974,23 +1973,127 @@ Proof.
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.
rewrite Nat.double_S. apply Nat.pow_le_mono_r. easy.
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
apply le_0_n.
Qed.
Theorem 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.
Proof.
intros m n hd a tl. intros H I J.
assert (E: length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
\/ 2^6 <= length a).
generalize J. generalize I. generalize H.
apply tm_step_palindromic_power2_even'.
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.
generalize dependent hd.
generalize dependent a.
generalize dependent tl.
generalize dependent n.
induction m.
- intros n tl a I J hd H E. destruct E. assumption.
rewrite J in H0. rewrite <- Nat.pow_le_mono_r_iff in H0.
inversion H0. inversion H2. inversion H4.
inversion H6. apply Nat.nle_succ_0 in H8.
contradiction H8. apply Nat.lt_1_2.
- intros n tl a I J hd H E. assert (E' := E).
destruct E as [E0 | E1]. assumption.
rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl).
rewrite <- pred_Sn.
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 Nat.mul_comm. rewrite Nat.div_mul. rewrite <- app_length.
assert (Y: length a' = 2 ^ Nat.double (S (S m))).
rewrite J in N. rewrite Nat.double_S in N.
rewrite Nat.pow_succ_r in N. rewrite Nat.pow_succ_r in N.
rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
rewrite Nat.mul_cancel_l in N. rewrite N. reflexivity. easy. reflexivity.
apply le_0_n. apply le_0_n.
assert (Y': 6 < length a').
rewrite N in E1.
rewrite Nat.pow_succ_r in E1. rewrite Nat.pow_succ_r in E1.
rewrite Nat.mul_assoc in E1. replace (2*2) with 4 in E1.
rewrite <- Nat.mul_le_mono_pos_l in E1.
assert (6 < 2^4). simpl.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
apply Nat.lt_0_succ. generalize E1. generalize H0.
apply Nat.lt_le_trans. apply Nat.lt_0_succ. reflexivity.
apply le_0_n. apply le_0_n.
apply IHm with (n := n) (tl := tl').
assumption. assumption. assumption.
generalize Y. generalize Y'. generalize H.
apply tm_step_palindromic_power2_even'.
easy. reflexivity. reflexivity.
assumption. assumption. assumption.
Qed.