baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-11-22 07:49:00 +01:00
parent 8e2b9958e5
commit af637eaae3
1 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
thue-morse.v
View File

@ -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.