From cde0ed14537033178bc79c451919b545284686b9 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 3 Jan 2023 18:34:44 +0100 Subject: [PATCH] Update --- thue-morse.v | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 446c38a..6ad0b7d 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -23,16 +23,6 @@ Fixpoint tm_step (n: nat) : list bool := end. (* ad hoc more or less general lemmas *) -Lemma negb_double_map : forall (l : list bool), - map negb (map negb l) = l. -Proof. - intro l. - induction l. - - reflexivity. - - simpl. rewrite IHl. replace (negb (negb a)) with (a). - reflexivity. rewrite negb_involutive. reflexivity. -Qed. - Lemma lt_split_bits : forall n m k j, 0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n. Proof. @@ -297,7 +287,6 @@ Proof. - reflexivity. - simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat. simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn. - rewrite map_app. rewrite negb_double_map. reflexivity. Qed.