From 161172e767501b7a8abf3a0d9065500b1a54d019 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 18 Jan 2023 12:24:21 +0100 Subject: [PATCH] Update --- src/thue_morse3.v | 50 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/src/thue_morse3.v b/src/thue_morse3.v index c98a4ea..7ab0722 100644 --- a/src/thue_morse3.v +++ b/src/thue_morse3.v @@ -228,8 +228,58 @@ Proof. reflexivity. Qed. +Lemma tm_step_palindromic_even_center' : + forall (n k m: nat) (hd a tl : list bool), + tm_step n = hd ++ a ++ (rev a) ++ tl + -> 0 < length a + -> length (hd ++ a) = S (2 * k) * 2^m + -> odd m = true. +Proof. + intros n k m hd a tl. intros H I J. + assert (Z := H). + assert (K: {a=nil} + {~ a=nil}). apply list_eq_dec. apply bool_dec. + destruct K. rewrite e in I. inversion I. + assert (L: a = removelast a ++ [ last a false ]). + apply app_removelast_last. assumption. + rewrite L in H. rewrite rev_app_distr in H. + assert (nth_error (tm_step n) (length (hd++a)) + = nth_error (tm_step n) (pred (length (hd++a)))). + rewrite H. + rewrite app_assoc. rewrite nth_error_app2. + symmetry. rewrite <- app_assoc. rewrite <- app_assoc. + rewrite app_assoc. rewrite nth_error_app2. + rewrite <- app_removelast_last. rewrite Nat.sub_diag. + replace (hd++a) with ((hd ++ removelast a) ++ [last a false]). + rewrite app_length. rewrite Nat.add_1_r. rewrite <- pred_Sn. + rewrite Nat.sub_diag. reflexivity. rewrite L at 3. + rewrite <- app_assoc. reflexivity. assumption. + + rewrite L at 2. rewrite app_assoc. + replace (length ((hd ++ removelast a) ++ [last a false])) + with (length (hd ++ removelast a) + length [last a false]). + rewrite Nat.add_1_r. rewrite <- pred_Sn. apply Nat.le_refl. + + symmetry. rewrite app_length. reflexivity. + rewrite <- app_removelast_last. apply Nat.le_refl. + assumption. + + generalize H0. rewrite J. apply tm_step_pred. + + rewrite <- J. rewrite <- tm_size_power2. rewrite Z. + rewrite app_length. rewrite app_length. + apply Nat.add_lt_mono_l. rewrite app_length. + rewrite <- Nat.add_0_r at 1. + apply Nat.add_lt_mono_l. rewrite app_length. rewrite rev_length. + assert (0 <= length tl). apply le_0_n. rewrite <- Nat.add_0_r at 1. + apply Nat.add_lt_le_mono; assumption. +Qed. + + + + + (* TODO: voir si une preuve du lemme précédent est plus rapide comme ceci *) (*