Last problem on morecoq.v

[sven--]

This looks quite simple logically but I cannot reduce it. Help!

[jeehoonkang]

Not sure where you have troubles with. So I paste my solution here:

Fixpoint forallb (A:Type) (P: forall (a:A), bool) (l: list A): bool :=
match l with
| nil => true
| a::l => andb (P a) (forallb _ P l)
end.

Fixpoint existsb (A:Type) (P: forall (a:A), bool) (l: list A): bool :=
match l with
| nil => false
| a::l => orb (P a) (existsb _ P l)
end.

Definition existsb' (A:Type) (P:forall (a:A), bool) (l: list A) :=
negb (forallb _ (fun a => negb (P a)) l).

Lemma negb_andb a b:
negb (andb a b) = orb (negb a) (negb b).
Proof.
destruct a, b; auto.
Qed.

Lemma existsb_existsb' (A:Type) (P: forall (a:A), bool) (l: list A):
existsb _ P l = existsb' _ P l.
Proof.
induction l; simpl in *; auto.
unfold existsb'. simpl.
rewrite negb_andb. rewrite negb_involutive.
unfold existsb' in IHl. rewrite <- IHl.
auto.
Qed.