From af637eaae3086ae44c932daaeba14cce0448d31b Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 22 Nov 2022 07:49:00 +0100 Subject: [PATCH] Update --- thue-morse.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/thue-morse.v b/thue-morse.v index 9bb4721..491ac9e 100644 --- a/thue-morse.v +++ b/thue-morse.v @@ -773,7 +773,7 @@ Proof. reflexivity. Qed. -Theorem tm_size_expo : forall n : nat, length (tm_step n) = 2^n. +Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n. Proof. intros n. induction n. @@ -794,16 +794,8 @@ Proof. simpl. reflexivity. Qed. -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)))). + rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))). Proof. intros n. induction n. - reflexivity. @@ -813,12 +805,19 @@ Proof. rewrite PeanoNat.Nat.even_succ. rewrite PeanoNat.Nat.odd_succ. rewrite Bool.negb_involutive. - reflexivity. - reflexivity. + reflexivity. reflexivity. +Qed. + +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_1 : forall (n : nat), - rev (tm_step n) = (odd n) :: tl (rev (tm_step n)). + rev (tm_step n) = odd n :: tl (rev (tm_step n)). Proof. intros n. destruct n. @@ -827,3 +826,4 @@ Proof. rewrite PeanoNat.Nat.odd_succ. reflexivity. Qed. +