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-13 23:32:11 +01:00
parent eefee9f83d
commit 047ed4c527
1 changed files with 43 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
src/thue_morse.v
View File

@ -391,6 +391,49 @@ Proof.
rewrite J. apply tm_morphism_count_occ.
Qed.
Lemma tm_step_consecutive_identical :
forall (n : nat) (hd a tl : list bool) (b : bool),
tm_step n = hd ++ (b::b::nil) ++ tl
-> odd (length hd) = true.
Proof.
intros n hd a tl b. intro H.
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
apply bool_dec. destruct J.
- rewrite <- Nat.negb_even. rewrite e. reflexivity.
- apply not_false_is_true in n0.
assert (K: count_occ Bool.bool_dec hd true
= count_occ Bool.bool_dec hd false).
generalize n0. generalize H. apply tm_step_count_occ.
assert (L: count_occ Bool.bool_dec (hd ++ [b;b]) true
= count_occ Bool.bool_dec (hd ++ [b;b]) false).
assert (even (length (hd ++ [b;b])) = true).
rewrite app_length. rewrite Nat.even_add_even. assumption.
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
generalize H0. rewrite app_assoc in H. generalize H.
apply tm_step_count_occ.
rewrite count_occ_app in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b. simpl in L. inversion L. simpl in L. inversion L.
Qed.
Lemma tm_step_consecutive_identical' :
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
-> even (length a) = true.
Proof.
intros n hd a tl b1 b2. intros H.
assert (Nat.odd (length hd) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (Nat.odd (length ((hd ++ [b1;b1])++a)) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
rewrite app_length in H1. rewrite Nat.odd_add in H1.
rewrite app_length in H1. rewrite Nat.odd_add in H1. rewrite H0 in H1.
replace (Nat.odd (length a)) with (negb (Nat.even (length a))) in H1.
destruct (even (length a)). reflexivity. inversion H1.
reflexivity.
Qed.
(**
The following lemmas and theorems focus on the stability of the sequence:
@ -898,51 +941,6 @@ Proof.
Qed.
Lemma tm_step_consecutive_identical :
forall (n : nat) (hd a tl : list bool) (b : bool),
tm_step n = hd ++ (b::b::nil) ++ tl
-> odd (length hd) = true.
Proof.
intros n hd a tl b. intro H.
assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
apply bool_dec. destruct J.
- rewrite <- Nat.negb_even. rewrite e. reflexivity.
- apply not_false_is_true in n0.
assert (K: count_occ Bool.bool_dec hd true
= count_occ Bool.bool_dec hd false).
generalize n0. generalize H. apply tm_step_count_occ.
assert (L: count_occ Bool.bool_dec (hd ++ [b;b]) true
= count_occ Bool.bool_dec (hd ++ [b;b]) false).
assert (even (length (hd ++ [b;b])) = true).
rewrite app_length. rewrite Nat.even_add_even. assumption.
simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
generalize H0. rewrite app_assoc in H. generalize H.
apply tm_step_count_occ.
rewrite count_occ_app in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b. simpl in L. inversion L. simpl in L. inversion L.
Qed.
Lemma tm_step_consecutive_identical' :
forall (n : nat) (hd a tl : list bool) (b1 b2 : bool),
tm_step n = hd ++ (b1::b1::nil) ++ a ++ (b2::b2::nil) ++ tl
-> even (length a) = true.
Proof.
intros n hd a tl b1 b2. intros H.
assert (Nat.odd (length hd) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
rewrite app_assoc in H. rewrite app_assoc in H.
assert (Nat.odd (length ((hd ++ [b1;b1])++a)) = true).
generalize H. apply tm_step_consecutive_identical. apply hd.
rewrite app_length in H1. rewrite Nat.odd_add in H1.
rewrite app_length in H1. rewrite Nat.odd_add in H1. rewrite H0 in H1.
replace (Nat.odd (length a)) with (negb (Nat.even (length a))) in H1.
destruct (even (length a)). reflexivity. inversion H1.
reflexivity.
Qed.
Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl
-> length a = 4 -> odd (length hd) = true