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-26 23:24:19 +01:00
parent 33619295a2
commit 30a2634ace
1 changed files with 24 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
src/thue_morse3.v
View File

@ -1493,17 +1493,19 @@ Proof.
apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
assumption. assumption.
(* proof that n <> 0 *) assert (V: 1 < n). assert (length (tm_step n) <= length (tm_step n)).
destruct n. assert (length (tm_step 0) <= length (tm_step 0)). apply Nat.le_refl. rewrite H in H0 at 1.
apply Nat.le_refl. rewrite app_length in H0. rewrite app_length in H0.
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.
rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite <- Nat.add_0_r in H0. apply Nat.le_le_add_le in H0.
apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0. rewrite tm_size_power2 in H0. destruct n. destruct a.
rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0. inversion W. destruct a. inversion W. inversion H2.
assert (K: 1 <= length a + (length tl + length hd)). destruct a. inversion W. inversion H2. inversion H4.
rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption. inversion H0. inversion H2. destruct a. inversion W.
rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0. destruct a. inversion W. inversion H2. destruct a. inversion W.
rewrite H0 in Z. inversion Z. inversion H2. inversion H4. destruct n. inversion H0. inversion H2.
inversion H4. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
apply le_0_n. destruct n. inversion V.
assert (J1: length hd mod 4 = 0). generalize J0. generalize W. assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
generalize H. apply tm_step_palindromic_length_12_prefix. generalize H. apply tm_step_palindromic_length_12_prefix.
@ -1578,26 +1580,25 @@ Proof.
rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc.
rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy. rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy.
assert (I': even (length hd') = true). assert (I': even (length hd') = true). unfold hd'. rewrite firstn_length.
unfold hd'. rewrite firstn_length_le. apply EVEN2. assumption. assert (C: Nat.div2 (length hd) <= length (tm_step n)
\/ length (tm_step n) < Nat.div2 (length hd)).
apply Nat.le_gt_cases. destruct C.
apply Nat.min_r in H6. rewrite Nat.min_comm. rewrite H6.
apply EVEN2. assumption. apply Nat.lt_le_incl in H6.
apply Nat.min_l in H6. rewrite Nat.min_comm. rewrite H6.
rewrite tm_size_power2. destruct n. inversion V. inversion H8.
rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
apply Nat.le_0_l.
assumption. easy.
rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl.
rewrite Nat.add_0_r. reflexivity.
apply Nat.le_refl.
rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
rewrite Nat.mul_comm.
rewrite Nat.div2_odd with (a := length a) at 2.
rewrite <- Nat.negb_even. rewrite J. simpl.
rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy.
Qed.