From 4f74ecf87015c3e421511e991ef3b57324ac9e82 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 3 Jan 2023 18:44:28 +0100 Subject: [PATCH] Update --- thue-morse.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 6ad0b7d..eb98929 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -151,15 +151,6 @@ Proof. + simpl. apply eq_S. assumption. Qed. -Lemma tm_morphism_app : forall (l1 l2 : list bool), - tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2. -Proof. - intros l1 l2. - induction l1. - - reflexivity. - - simpl. rewrite IHl1. reflexivity. -Qed. - Lemma tm_morphism_eq : forall (l1 l2 : list bool), l1 = l2 <-> tm_morphism l1 = tm_morphism l2. Proof. @@ -184,6 +175,15 @@ Proof. simpl. rewrite Nat.add_0_r. reflexivity. Qed. +Lemma tm_morphism_app : forall (l1 l2 : list bool), + tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2. +Proof. + intros l1 l2. + induction l1. + - reflexivity. + - simpl. rewrite IHl1. reflexivity. +Qed. + Lemma tm_morphism_app2 : forall (l hd tl : list bool), tm_morphism l = hd ++ tl -> even (length hd) = true