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-24 07:56:21 +01:00
parent 0bad6482ea
commit ab50cd2b28
1 changed files with 44 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
src/thue_morse3.v
View File

@ -1248,12 +1248,6 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
Qed.
Lemma tm_step_palindromic_length_12 :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ rev a ++ tl
@ -1310,15 +1304,54 @@ Proof.
rewrite Nat.add_sub_swap in H2. rewrite Nat.add_sub in H2.
assert (K: forall m (u : list bool),
nth_error u m = nth_error (rev u) (length u - S m)).
intros. induction u. destruct m. reflexivity.
rewrite nth_error_None. apply Nat.le_0_l.
induction m. simpl. rewrite nth_error_app2. rewrite rev_length.
m < length u -> nth_error u m = nth_error (rev u) (length u - S m)).
intros m u. intro V.
assert (V' := V). apply nth_error_nth' with (d := false) in V'.
assert (exists l1 l2, u = l1 ++ (nth m u false)::l2 /\ length l1 = m).
apply nth_error_split. assumption. destruct H3. destruct H3. destruct H3.
rewrite V'.
assert (length u = length u). reflexivity. rewrite H3 in H5 at 2.
rewrite app_length in H5. rewrite H4 in H5.
rewrite H3 at 2. rewrite rev_app_distr. rewrite nth_error_app1.
replace (nth m u false :: x0) with ([nth m u false] ++ x0).
rewrite rev_app_distr. rewrite H5.
rewrite Nat.add_comm. replace (S m) with (m + 1).
rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc.
rewrite Nat.sub_diag. rewrite Nat.add_0_r.
rewrite nth_error_app2. rewrite rev_length. simpl.
rewrite Nat.sub_0_r. rewrite Nat.sub_diag. reflexivity.
rewrite rev_length. rewrite Nat.sub_0_r. apply Nat.le_refl.
rewrite rev_length. simpl. rewrite Nat.sub_0_r. apply Nat.le_refl.
apply Nat.le_refl. rewrite Nat.add_1_r. reflexivity. reflexivity.
rewrite rev_length. rewrite Nat.add_lt_mono_r with (p := m).
replace (S m) with (m + 1). rewrite <- Nat.add_sub_swap.
rewrite Nat.sub_add_distr. rewrite <- Nat.add_sub_assoc.
rewrite Nat.sub_diag. rewrite Nat.add_0_r. rewrite Nat.add_comm.
rewrite <- H5. apply Nat.sub_lt. rewrite H5. simpl.
rewrite Nat.add_succ_r. apply le_n_S. apply Nat.le_0_l.
apply Nat.lt_0_1. apply Nat.le_refl.
rewrite Nat.add_succ_r. rewrite Nat.add_0_r. rewrite Nat.le_succ_l.
assumption. apply Nat.add_1_r.
rewrite K with (u := rev (b::b0::b1::l)) in H2.
rewrite rev_involutive in H2. rewrite rev_length in H2.
contradiction H2. reflexivity.
rewrite rev_length. simpl. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
simpl. apply le_n_S. apply le_n_S. apply le_n_S.
apply Nat.le_0_l.
rewrite rev_length. simpl. rewrite <- Nat.succ_lt_mono.
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
rewrite app_length. simpl.
replace (S (S (S (length l)))) with (length l + 3).
rewrite <- Nat.add_sub_assoc. rewrite <- Nat.add_sub_assoc.
rewrite Nat.sub_diag. rewrite Nat.add_0_r.
apply Nat.le_add_r. apply Nat.le_refl.
apply Nat.le_add_l. rewrite Nat.add_comm. simpl. reflexivity.
Qed.