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 13:37:12 +01:00
parent b4940d3d78
commit 52109dba62
1 changed files with 39 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
thue-morse.v
View File

@ -160,6 +160,16 @@ Proof.
reflexivity.
Qed.
Lemma tm_morphism_size : forall l : list bool,
length (tm_morphism l) = 2 * (length l).
Proof.
intro l. induction l.
- reflexivity.
- simpl. rewrite Nat.add_0_r. rewrite IHl.
rewrite Nat.add_succ_r. replace (2) with (1+1). rewrite Nat.mul_add_distr_r.
rewrite Nat.mul_1_l. reflexivity. reflexivity.
Qed.
Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
Proof.
intro n.
@ -1234,7 +1244,8 @@ 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.
-> 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
@ -1281,9 +1292,34 @@ Proof.
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))).
assumption.
Qed.
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))).
rewrite M. apply tm_morphism_size.
assert (6 <= length (b++b++b++tl2)).
rewrite app_length. replace (6) with (2+4). apply Nat.add_le_mono. assumption.
rewrite app_length. replace (4) with (2+2). apply Nat.add_le_mono. assumption.
rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
apply Nat.le_0_l. apply Nat.add_0_r. easy. easy.
rewrite H3 in H4. replace (6) with (2*3) in H4. rewrite <- Nat.mul_le_mono_pos_l in H4.
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))).
rewrite <- Nat.div2_odd. assumption.
rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
apply Nat.lt_0_2.
assert (1 <= 3). rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
assert (1 <= length (skipn (Nat.div2 (length hd2)) (tm_step n))).
generalize H4. generalize H6. apply Nat.le_trans.
generalize H7. generalize H5. apply Nat.min_glb.
apply Nat.lt_0_2. easy.
Qed.