From c05caff356194748856d099a1b22fbd030e488ab Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 9 Feb 2023 21:13:37 +0100 Subject: [PATCH] Update --- src/thue_morse4.v | 257 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 257 insertions(+) diff --git a/src/thue_morse4.v b/src/thue_morse4.v index 228d54a..ec675e6 100644 --- a/src/thue_morse4.v +++ b/src/thue_morse4.v @@ -160,6 +160,81 @@ Proof. Qed. +(* +Lemma xxx : + forall (n : nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ a ++ tl + -> 0 < length a + -> a = rev a \/ a = map negb (rev a). +Proof. + intros n hd a tl. intros H I. + + destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity. + rewrite H in H0 at 2. rewrite app_length in H0. rewrite app_length in H0. + rewrite app_length in H0. rewrite Nat.add_comm in H0. + destruct a. inversion I. rewrite <- Nat.add_assoc in H0. + rewrite <- Nat.add_assoc in H0. simpl in H0. rewrite Nat.add_succ_r in H0. + apply Nat.succ_inj in H0. apply Nat.neq_0_succ in H0. contradiction. + + assert (exists k j, length a = S (Nat.double k) * 2^j). + apply trailing_zeros; assumption. destruct H0. destruct H0. + assert (x = 0 \/ x = 1). generalize H0. generalize H. + apply tm_step_square_size. + + generalize dependent n. generalize dependent hd. generalize dependent a. + generalize dependent tl. generalize dependent x. + induction x0; intros x K tl a J I hd n H. + - destruct K; rewrite H0 in I; destruct a. + inversion J. destruct a. left. reflexivity. inversion I. + inversion I. destruct a. inversion I. destruct a. inversion I. + destruct a. + assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. + rewrite e. left. reflexivity. + assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1. + rewrite e in H. + replace (hd ++ [b; b1; b1] ++ [b; b1; b1] ++ tl) + with ((hd ++ [b]) ++ [b1;b1] ++ [b] ++ [b1;b1] ++ tl) in H. + apply tm_step_consecutive_identical' in H. inversion H. + rewrite <- app_assoc. reflexivity. + assert (b = b0). destruct b; destruct b0; destruct b1; + reflexivity || contradiction n0 || contradiction n1; reflexivity. + rewrite H1 in H. + replace (hd ++ [b0; b0; b1] ++ [b0; b0; b1] ++ tl) + with (hd ++ [b0;b0] ++ [b1] ++ [b0;b0] ++ ([b1] ++ tl)) in H. + apply tm_step_consecutive_identical' in H. inversion H. reflexivity. + inversion I. + - assert (even (length a) = true). + rewrite Nat.mul_comm in I. rewrite Nat.pow_succ_r in I. rewrite I. + rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. + apply Nat.le_0_l. + assert (even (length (hd ++ a)) = true). + generalize J. generalize H. apply tm_step_square_pos. + assert (even (length hd) = true). + rewrite app_length in H1. rewrite Nat.even_add in H1. + rewrite H0 in H1. destruct (Nat.even (length hd)). reflexivity. + inversion H1. + + + + (se débarrasser du S x0 en I) + generalize H. generalize n. generalize hd. generalize I. generalize J. + apply IHx0. + + +Lemma tm_step_morphism4 : + forall (n : nat) (hd a b tl : list bool), + tm_step (S n) = hd ++ a ++ b ++ tl + -> even (length hd) = true + -> even (length a) = true + -> even (length b) = true + -> tm_step (S n) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step n) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step n)) ++ + firstn (Nat.div2 (length b)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step n)) ++ + skipn (Nat.div2 (length (hd ++ a ++ b))) (tm_step n)). + *) Lemma xxx : forall (j n : nat) (hd a tl : list bool), @@ -192,13 +267,195 @@ Proof. rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. rewrite Nat.even_mul. rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. + assert (0 < length a). destruct I; rewrite H1. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. apply Nat.mul_pos_pos. lia. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. + assert (even (length (hd ++ a)) = true). generalize H1. generalize H. apply tm_step_square_pos. + assert (even (length hd) = true). rewrite app_length in H2. + rewrite Nat.even_add in H2. rewrite H0 in H2. + destruct (even (length hd)). reflexivity. inversion H2. + + assert (2 <= n). + assert (length (tm_step n) = length (tm_step n)). reflexivity. + rewrite H in H4 at 2. rewrite app_length in H4. rewrite Nat.add_comm in H4. + rewrite app_length in H4. destruct I; rewrite H5 in H4; + rewrite tm_size_power2 in H4; rewrite Nat.double_S in H4; + symmetry in H4; apply Nat.eq_le_incl in H4. + assert (2^(S (S (Nat.double j))) <= 2^n). + assert (2^(S (S (Nat.double j))) + <= 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). + rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. + generalize H6. apply Nat.le_trans. rewrite <- Nat.pow_le_mono_r_iff in H6. + assert (2 <= S (S (Nat.double j))). lia. generalize H6. generalize H7. + apply Nat.le_trans. apply Nat.lt_1_2. + assert (3 * 2^(S (S (Nat.double j))) <= 2^n). + assert (3 * 2^(S (S (Nat.double j))) + <= 3 * 2 ^ (S (S (Nat.double j))) + length (a ++ tl) + length hd). + rewrite <- Nat.add_assoc. apply Nat.le_add_r. generalize H4. + generalize H6. apply Nat.le_trans. + assert (2^(S (S (Nat.double j))) <= 3 * 2^(S (S (Nat.double j)))). + rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_pos_r. + rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy. lia. + assert (2^(S (S (Nat.double j))) <= 2^n). + generalize H6. generalize H7. apply Nat.le_trans. + rewrite <- Nat.pow_le_mono_r_iff in H8. + assert (2 <= S (S (Nat.double j))). lia. generalize H8. generalize H9. + apply Nat.le_trans. apply Nat.lt_1_2. + destruct n. inversion H4. destruct n. inversion H4. inversion H6. + + assert( + tm_step (S (S n)) = tm_morphism + (firstn (Nat.div2 (length hd)) (tm_step (S n)) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step (S n))) ++ + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))) ++ + skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n)))). + generalize H0. generalize H0. generalize H3. generalize H. + apply tm_step_morphism4. + + pose (hd' := firstn (Nat.div2 (length hd)) (tm_step (S n))). + pose (a' := firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length hd)) (tm_step (S n)))). + pose (tl' := skipn (Nat.div2 (length (hd ++ a ++ a))) (tm_step (S n))). + fold hd' in H5. fold a' in H5. fold tl' in H5. + + assert (length hd' = Nat.div2 (length hd)). unfold hd'. + rewrite firstn_length_le. reflexivity. + rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. + rewrite tm_size_power2. rewrite <- Nat.pow_succ_r. + rewrite <- tm_size_power2. rewrite <- Nat.Even_double. + rewrite H. rewrite app_length. lia. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. lia. lia. + + assert (length hd = length (tm_morphism hd')). + rewrite tm_morphism_length. rewrite H6. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. reflexivity. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + + assert (length a' = Nat.div2 (length a)). unfold a'. + rewrite firstn_length_le. reflexivity. rewrite skipn_length. + rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. + rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. + rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. + rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. + rewrite H. rewrite app_length. rewrite app_length. lia. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + lia. lia. + + assert (length a = length (tm_morphism a')). + rewrite tm_morphism_length. rewrite H8. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. reflexivity. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + + rewrite H in H5. rewrite tm_morphism_app in H5. + + assert (hd = tm_morphism hd'). generalize H7. generalize H5. + apply app_eq_length_head. rewrite <- H10 in H5. + apply app_inv_head in H5. rewrite tm_morphism_app in H5. + + assert (a = tm_morphism a'). generalize H9. generalize H5. + apply app_eq_length_head. rewrite <- H11 in H5. + apply app_inv_head in H5. rewrite tm_morphism_app in H5. + + assert (length a = length (tm_morphism ( + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n)))))). + rewrite tm_morphism_length. rewrite firstn_length_le. + rewrite <- Nat.double_twice. rewrite <- Nat.Even_double. + reflexivity. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + rewrite skipn_length. + rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. + rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. + rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. + rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. + rewrite H. rewrite app_assoc. + rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. + rewrite app_length. lia. apply Nat.le_refl. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + lia. lia. + + assert (a = tm_morphism ( + firstn (Nat.div2 (length a)) + (skipn (Nat.div2 (length (hd ++ a))) (tm_step (S n))))). + generalize H12. generalize H5. apply app_eq_length_head. + rewrite <- H13 in H5. apply app_inv_head in H5. + + assert (H' := H). + rewrite H10 in H'. rewrite H11 in H'. rewrite H5 in H'. + rewrite <- tm_morphism_app in H'. + rewrite <- tm_morphism_app in H'. + rewrite <- tm_morphism_app in H'. + rewrite <- tm_step_lemma in H'. rewrite <- tm_morphism_eq in H'. + + assert (even (length a') = true). unfold a'. + rewrite firstn_length_le. + destruct I; rewrite H14; rewrite Nat.double_S. + rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. + rewrite Nat.div2_double. + rewrite Nat.even_mul. reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. + rewrite Nat.mul_comm. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r. + rewrite <- Nat.mul_assoc. + rewrite Nat.div2_double. + rewrite Nat.even_mul. rewrite Nat.even_mul. + reflexivity. apply Nat.le_0_l. apply Nat.le_0_l. + rewrite skipn_length. + rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. + rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. + rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. + rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. + rewrite H. rewrite app_length. rewrite app_length. lia. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + lia. lia. + + assert (0 < length a'). unfold a'. rewrite firstn_length_le. + destruct (length a). destruct I. inversion H1. inversion H1. + destruct n0. inversion H0. replace (S (S n0)) with (n0 + 1*2). + rewrite Nat.div2_div. rewrite Nat.div_add. rewrite Nat.add_1_r. lia. + easy. lia. + rewrite skipn_length. + rewrite Nat.mul_le_mono_pos_l with (p := 2). rewrite <- Nat.double_twice. + rewrite tm_size_power2. rewrite Nat.mul_sub_distr_l. + rewrite <- Nat.pow_succ_r. rewrite <- tm_size_power2. + rewrite <- Nat.Even_double. rewrite <- Nat.double_twice. + rewrite <- Nat.Even_double. + rewrite H. rewrite app_length. rewrite app_length. lia. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption. + lia. lia. + + assert (even (length (hd' ++ a')) = true). generalize H15. + generalize H'. apply tm_step_square_pos. + + assert (even (length hd') = true). rewrite app_length in H16. + rewrite Nat.even_add in H16. rewrite H14 in H16. + destruct (even (length hd')). reflexivity. inversion H16. + + assert ( + tm_step (S n) = tm_morphism + (firstn (Nat.div2 (length hd')) (tm_step n) ++ + firstn (Nat.div2 (length a')) + (skipn (Nat.div2 (length hd')) (tm_step n)) ++ + firstn (Nat.div2 (length a')) + (skipn (Nat.div2 (length (hd' ++ a'))) (tm_step n)) ++ + skipn (Nat.div2 (length (hd' ++ a' ++ a'))) (tm_step n))). + generalize H14. generalize H14. generalize H17. generalize H'. + apply tm_step_morphism4. + + +