This commit is contained in:
Thomas Baruchel 2023-01-13 23:28:54 +01:00
parent 75e2fb9acd
commit eefee9f83d
2 changed files with 45 additions and 51 deletions

View File

@ -898,6 +898,51 @@ Proof.
Qed. 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), Lemma tm_step_factor4_odd_prefix : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl tm_step n = hd ++ a ++ tl
-> length a = 4 -> odd (length hd) = true -> length a = 4 -> odd (length hd) = true

View File

@ -8,57 +8,6 @@ Require Import Bool.
Import ListNotations. Import ListNotations.
(**
The following lemma, while not of truly general use, is
used in several proofs and has therefore its own dedicated
section here.
*)
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 are all related to The following lemmas and theorems are all related to
squares of odd length in the Thue-Morse sequence. squares of odd length in the Thue-Morse sequence.