Update
This commit is contained in:
parent
8b811724d4
commit
cde0ed1453
11
thue-morse.v
11
thue-morse.v
@ -23,16 +23,6 @@ Fixpoint tm_step (n: nat) : list bool :=
|
|||||||
end.
|
end.
|
||||||
|
|
||||||
(* ad hoc more or less general lemmas *)
|
(* 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,
|
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.
|
0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
|
||||||
Proof.
|
Proof.
|
||||||
@ -297,7 +287,6 @@ Proof.
|
|||||||
- reflexivity.
|
- reflexivity.
|
||||||
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
|
- simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
|
||||||
simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
|
simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
|
||||||
rewrite map_app. rewrite negb_double_map.
|
|
||||||
reflexivity.
|
reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user