From 773caecd3caa2996ce6e1db864fd277242232f1c Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 2 Jan 2023 18:13:52 +0100 Subject: [PATCH] Update --- thue-morse.v | 97 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 97 insertions(+) diff --git a/thue-morse.v b/thue-morse.v index f7c21df..9425814 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -874,11 +874,108 @@ Proof. Qed. +Lemma count_occ_bool_list : forall (a: list bool), + length a = (count_occ bool_dec a true) + (count_occ bool_dec a false). +Proof. + intro a. + induction a. + - reflexivity. + - destruct a. + + rewrite count_occ_cons_eq. rewrite count_occ_cons_neq. + simpl. rewrite IHa. reflexivity. easy. reflexivity. + + rewrite count_occ_cons_neq. rewrite count_occ_cons_eq. + simpl. rewrite Nat.add_succ_r. rewrite IHa. reflexivity. reflexivity. easy. +Qed. + + +Lemma count_occ_bool_list2 : forall (a: list bool), + count_occ bool_dec a false = count_occ bool_dec a true -> even (length a) = true. +Proof. + intro a. intro H. + rewrite count_occ_bool_list. rewrite H. + replace (count_occ bool_dec a true) with (1 * (count_occ bool_dec a true)). + rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r. + replace (2 * count_occ bool_dec a true) with (0 + 2 * count_occ bool_dec a true). + apply Nat.even_add_mul_2. apply Nat.add_0_l. apply Nat.mul_1_l. +Qed. + + Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool), tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true. Proof. + intros n a hd tl. intro H. + assert (Nat.Even (length hd) \/ Nat.Odd (length hd)). apply Nat.Even_or_Odd. + assert (Nat.Even (length a) \/ Nat.Odd (length a)). apply Nat.Even_or_Odd. + destruct H1. + - apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + - destruct H0. + assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false). + assert (Nat.even (length hd) = true). + apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + generalize H2. generalize H. apply tm_step_count_occ. + assert (I := H). replace (hd++a++a++a++tl) with ((hd++a++a)++(a++tl)) in I. + assert (count_occ Bool.bool_dec (hd++a++a) true = count_occ Bool.bool_dec (hd++a++a) false). + assert (even (length (hd++a++a)) = true). + rewrite app_length. rewrite Nat.even_add_even. + apply Nat.EvenT_even. apply Nat.Even_EvenT. assumption. + + rewrite app_length. replace (length a) with (1*(length a)). + rewrite <- Nat.mul_add_distr_r. rewrite Nat.add_1_r. + rewrite <- Nat.add_0_l. apply Nat.EvenT_Even. + apply Nat.even_EvenT. + rewrite Nat.even_add_mul_2. reflexivity. + apply Nat.mul_1_l. + generalize H3. generalize I. apply tm_step_count_occ. + + rewrite count_occ_app in H3. symmetry in H3. + rewrite count_occ_app in H3. rewrite H2 in H3. + rewrite Nat.add_cancel_l in H3. + + rewrite count_occ_app in H3. rewrite count_occ_app in H3. + replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. + replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. + rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. + rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. + assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + + assert (I := H). replace (hd++a++a++a++tl) with ((hd++a)++(a++a++tl)) in I. + assert (count_occ Bool.bool_dec (hd++a) true = count_occ Bool.bool_dec (hd++a) false). + assert (even (length (hd++a)) = true). + rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + generalize H2. generalize I. apply tm_step_count_occ. + + assert (J := H). replace (hd++a++a++a++tl) with ((hd++a++a++a)++tl) in J. + assert (count_occ Bool.bool_dec (hd++a++a++a) true = count_occ Bool.bool_dec (hd++a++a++a) false). + assert (even (length (hd++a++a++a)) = true). + rewrite Nat.EvenT_even. reflexivity. apply Nat.Even_EvenT. + rewrite app_length. rewrite app_length. rewrite Nat.add_assoc. rewrite <- app_length. + apply Nat.Even_Even_add. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + rewrite app_length. apply Nat.Odd_Odd_add; assumption. + generalize H3. generalize J. apply tm_step_count_occ. + + replace (hd++a++a++a) with ((hd++a)++(a++a)) in H3. + rewrite count_occ_app in H3. symmetry in H3. + rewrite count_occ_app in H3. rewrite H2 in H3. + rewrite Nat.add_cancel_l in H3. + + rewrite count_occ_app in H3. rewrite count_occ_app in H3. + replace (count_occ bool_dec a false) with (1*(count_occ bool_dec a false)) in H3. + replace (count_occ bool_dec a true) with (1*(count_occ bool_dec a true)) in H3. + rewrite <- Nat.mul_add_distr_r in H3. rewrite <- Nat.mul_add_distr_r in H3. + rewrite Nat.mul_cancel_l in H3. apply count_occ_bool_list2 in H3. + assumption. easy. apply Nat.mul_1_l. apply Nat.mul_1_l. + rewrite app_assoc_reverse. reflexivity. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. + rewrite app_assoc_reverse. reflexivity. + rewrite app_assoc_reverse. rewrite app_inv_head_iff. reflexivity. +Qed. Prouver l'énoncé du concours général