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-01-03 21:16:18 +01:00
parent 4f74ecf870
commit 7ac1cd5608
1 changed files with 54 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

98
thue-morse.v
View File

@ -762,7 +762,7 @@ Proof.
symmetry in I. apply tm_step_succ_double_index in I. contradiction I.
apply Nat.lt_succ_l in H. rewrite Nat.pow_succ_r' in H.
rewrite <- Nat.mul_lt_mono_pos_l in H. assumption. apply Nat.lt_0_2.
intro I. apply diff_false_true in I. contradiction I.
intro I. inversion I.
intro n0. intro I.
destruct n0. rewrite Nat.pow_0_r in I. rewrite Nat.lt_1_r in I.
@ -822,11 +822,8 @@ Proof.
contradiction H. reflexivity.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m));
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1)).
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
intro K. simpl in K. apply diff_false_true in K. contradiction K.
destruct (nth_error (tm_step n0) (S (2 * k) * 2 ^ m - 1));
intro K; simpl in K; inversion K.
rewrite nth_error_nth' with (d := false) in J.
rewrite nth_error_nth' with (d := false) in J.
@ -1204,13 +1201,13 @@ Qed.
Lemma tm_step_cube6 : forall (n : nat) (a hd tl: list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl
-> 0 < length a
-> exists (hd2 b tl2 : list bool), tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2
/\ 0 < length b.
-> exists (hd2 b tl2 : list bool),
tm_step (Nat.pred n) = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b.
Proof.
intros n a hd tl. intros H I.
assert(J: exists (hd2 b tl2 : list bool), tm_step n = hd2 ++ b ++ b ++ b ++ tl2
/\ length a = length b
/\ even (length hd2) = true).
assert(J: exists (hd2 b tl2 : list bool),
tm_step n = hd2 ++ b ++ b ++ b ++ tl2
/\ length a = length b /\ even (length hd2) = true).
generalize I. generalize H. apply tm_step_cube5.
destruct J as [ hd2 J0]. destruct J0 as [ b J1]. destruct J1 as [ tl2 J2].
destruct J2 as [J3 J4]. destruct J4 as [J5 J6].
@ -1222,9 +1219,12 @@ Proof.
- rewrite <- tm_step_lemma in J3.
assert (L: hd2 = tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n))).
generalize J6. generalize J3. apply tm_morphism_app2.
assert (M: b ++ b ++ b ++ tl2 = tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))).
assert (M: b ++ b ++ b ++ tl2
= tm_morphism (skipn (Nat.div2 (length hd2)) (tm_step n))).
generalize J6. generalize J3. apply tm_morphism_app3.
assert (N: b = tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n)))).
assert (N: b = tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length hd2))
(tm_step n)))).
generalize J. symmetry in M. generalize M. apply tm_morphism_app2.
assert (even (length (b++b++b)) = true).
rewrite app_length. rewrite app_length.
@ -1232,17 +1232,23 @@ Proof.
apply Nat.EvenT_Even. apply Nat.even_EvenT.
rewrite Nat.even_add_even. assumption.
apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b))) (skipn (Nat.div2 (length hd2)) (tm_step n)))).
assert (O: tl2 = tm_morphism (skipn (Nat.div2 (length (b++b++b)))
(skipn (Nat.div2 (length hd2))
(tm_step n)))).
generalize H0. symmetry in M. generalize M.
replace (b++b++b++tl2) with ((b++b++b)++tl2). apply tm_morphism_app3.
rewrite app_assoc_reverse. apply app_inv_head_iff.
rewrite app_assoc_reverse. reflexivity.
assert (hd2 ++ b ++ b ++ b ++ tl2
= (tm_morphism (firstn (Nat.div2 (length hd2)) (tm_step n)))
++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))))).
++ (tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length hd2)) (tm_step n))))
++ (tm_morphism (skipn (Nat.div2 (length (b ++ b ++ b)))
(skipn (Nat.div2 (length hd2)) (tm_step n))))).
rewrite <- L. rewrite <- N. rewrite <- O. reflexivity.
rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
rewrite <- tm_morphism_app in H1. rewrite <- tm_morphism_app in H1.
@ -1250,15 +1256,19 @@ Proof.
rewrite Nat.pred_succ. rewrite <- tm_morphism_eq in H1.
exists (firstn (Nat.div2 (length hd2)) (tm_step n)).
exists (firstn (Nat.div2 (length b)) (skipn (Nat.div2 (length hd2)) (tm_step n))).
exists (skipn (Nat.div2 (length (b ++ b ++ b))) (skipn (Nat.div2 (length hd2)) (tm_step n))).
exists (firstn (Nat.div2 (length b))
(skipn (Nat.div2 (length hd2)) (tm_step n))).
exists (skipn (Nat.div2 (length (b ++ b ++ b)))
(skipn (Nat.div2 (length hd2)) (tm_step n))).
split. assumption.
assert (2 <= length b).
destruct b. simpl in J5. rewrite J5 in I. apply Nat.lt_irrefl in I. contradiction I.
destruct b0. simpl in J. inversion J.
simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
assert (length (b++b++b++tl2) = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
assert (2 <= length b). destruct b. simpl in J5. rewrite J5 in I.
apply Nat.lt_irrefl in I. contradiction I.
destruct b0. simpl in J. inversion J. simpl. rewrite <- Nat.succ_le_mono.
rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
assert (length (b++b++b++tl2)
= 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
rewrite M. apply tm_morphism_size.
assert (2 <= length (b++b++b++tl2)).
@ -1270,7 +1280,8 @@ Proof.
rewrite firstn_length. rewrite <- Nat.le_succ_l.
assert (1 <= Nat.div2 (length b)).
rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r.
replace (2 * Nat.div2 (length b)) with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))).
replace (2 * Nat.div2 (length b))
with (2 * Nat.div2 (length b) + Nat.b2n (Nat.odd (length b))).
rewrite <- Nat.div2_odd. assumption.
rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
apply Nat.lt_0_2.
@ -1290,9 +1301,11 @@ Proof.
- destruct H. destruct H. destruct H. destruct H.
exists x. exists x0. exists x1. split; assumption.
- destruct H. destruct H. destruct H. destruct H.
assert (J: exists (hd2 b2 tl2 : list bool), tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2 /\ 0 < length b2).
generalize H0. generalize H. apply tm_step_cube6. rewrite Nat.pred_succ in J.
apply IHn. apply J.
assert (J: exists (hd2 b2 tl2 : list bool),
tm_step (Nat.pred (S n)) = hd2 ++ b2 ++ b2 ++ b2 ++ tl2
/\ 0 < length b2).
generalize H0. generalize H. apply tm_step_cube6.
rewrite Nat.pred_succ in J. apply IHn. apply J.
Qed.
@ -1302,21 +1315,18 @@ Proof.
intros n hd a b tl. intros H I.
assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
destruct J. rewrite <- e in H.
assert (exists (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ a ++ tl
/\ 0 < length a).
exists hd. exists a. exists tl. split; assumption.
assert (exists (hd2 b tl2 : list bool), tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2
/\ 0 < length b).
generalize H0. apply tm_step_cube7.
destruct H1. destruct H1. destruct H1. destruct H1.
assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2.
apply Nat.lt_irrefl in H3. contradiction H3.
assumption.
destruct J.
- rewrite <- e in H.
assert (exists (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
exists hd. exists a. exists tl. split; assumption.
assert (exists (hd2 b tl2 : list bool),
tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b).
generalize H0. apply tm_step_cube7.
destruct H1. destruct H1. destruct H1. destruct H1.
assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2.
apply Nat.lt_irrefl in H3. contradiction H3.
- assumption.
Qed.