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 06:44:35 +01:00
parent 3dad13243b
commit 8e2b9958e5
1 changed files with 24 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
thue-morse.v
View File

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