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:54:17 +01:00
parent 52109dba62
commit e5c270e119
1 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
thue-morse.v
View File

@ -1300,13 +1300,12 @@ Proof.
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.
assert (2 <= length (b++b++b++tl2)).
rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
apply Nat.le_0_l. apply Nat.add_0_r.
rewrite H3 in H4. replace (2) with (2*1) 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.
@ -1314,14 +1313,16 @@ Proof.
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.
generalize H4. generalize H5. apply Nat.min_glb.
apply Nat.lt_0_2. easy.
Qed.
Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
tm_step n = hd ++ a ++ a ++ b ++ tl -> a <> b.
Proof.
intros n hd a b tl. intro H.
assert (I: a=b \/ a<>b).