From 8e2b9958e5c23d317e9201764322bb79f4d7894c Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 22 Nov 2022 06:44:35 +0100 Subject: [PATCH] Update --- thue-morse.v | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 52cee49..9bb4721 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -783,8 +783,7 @@ Proof. simpl. rewrite <- plus_n_O. reflexivity. Qed. -Lemma tm_step_head : - forall (n : nat), +Lemma tm_step_head_2 : forall (n : nat), tm_step (S n) = false :: true :: tl (tl (tm_step (S n))). Proof. intros n. @@ -795,8 +794,15 @@ Proof. simpl. reflexivity. Qed. -Lemma tm_step_end : - forall (n : nat), +Lemma tm_step_head_1 : forall (n : nat), + tm_step n = false :: tl (tm_step n). +Proof. + intros n. destruct n. + - reflexivity. + - rewrite tm_step_head_2. reflexivity. +Qed. + +Lemma tm_step_end_2 : forall (n : nat), rev (tm_step (S n)) = (even n) :: (odd n) :: tl (tl (rev (tm_step (S n)))). Proof. intros n. induction n. @@ -804,10 +810,20 @@ Proof. - simpl tm_step. rewrite tm_morphism_rev. replace (tm_morphism (tm_step n)) with (tm_step (S n)). rewrite IHn. simpl tm_morphism. simpl tl. - replace (negb (negb (even n))) with (odd (S n)). - replace (negb (even n)) with (even (S n)). + rewrite PeanoNat.Nat.even_succ. + rewrite PeanoNat.Nat.odd_succ. + rewrite Bool.negb_involutive. reflexivity. - rewrite PeanoNat.Nat.even_succ. reflexivity. - rewrite PeanoNat.Nat.odd_succ. rewrite Bool.negb_involutive. reflexivity. + reflexivity. +Qed. + +Lemma tm_step_end_1 : forall (n : nat), + rev (tm_step n) = (odd n) :: tl (rev (tm_step n)). +Proof. + intros n. + destruct n. + - reflexivity. + - rewrite tm_step_end_2. simpl. + rewrite PeanoNat.Nat.odd_succ. reflexivity. Qed.